feat(Topology/Algebra/Module/Equiv): add 2 lemmas (leanprover-community#33510)

Author: urkud

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -1199,11 +1199,21 @@ theorem self_comp_inverse (hf : f.IsInvertible) : f ∘L f.inverse = .id _ _ :=
   rcases hf with ⟨e, rfl⟩
   simp
 
+@[simp]
+theorem self_apply_inverse (hf : f.IsInvertible) (y : M₂) : f (f.inverse y) = y := by
+  rcases hf with ⟨e, rfl⟩
+  simp
+
 @[simp]
 theorem inverse_comp_self (hf : f.IsInvertible) : f.inverse ∘L f = .id _ _ := by
   rcases hf with ⟨e, rfl⟩
   simp
 
+@[simp]
+theorem inverse_apply_self (hf : f.IsInvertible) (y : M) : f.inverse (f y) = y := by
+  rcases hf with ⟨e, rfl⟩
+  simp
+
 protected theorem bijective (hf : f.IsInvertible) : Function.Bijective f := by
   rcases hf with ⟨e, rfl⟩
   simp [ContinuousLinearEquiv.bijective]