-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem to_ring_inverse (e : M ≃L[R] M₂) (f : M →L[R] M₂) :
    inverse f = Ring.inverse ((e.symm : M₂ →L[R] M).comp f) ∘L e.symm

Proof state:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (Ring.inverse ↑(e'.trans e.symm)).comp ↑e.symm

Tactic:
ext

Result:
case pos.intro.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
x✝ : M₂
⊢ (↑e').inverse x✝ = ((Ring.inverse ↑(e'.trans e.symm)).comp ↑e.symm) x✝

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Tactic:
by_cases h₁ : f.IsInvertible

Result:
case pos
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : f.IsInvertible
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬f.IsInvertible
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬f.IsInvertible
this : ¬IsUnit ((↑e.symm).comp f)
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Tactic:
simp [this, h₁]

Result:
no goals

Proof state:
case h.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
x✝ : M
⊢ e (((↑e.symm).comp f) x✝) = f x✝

Tactic:
simp

Result:
no goals

Proof state:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : IsUnit ((↑e.symm).comp f)
⊢ f.IsInvertible

Tactic:
rcases h₁ with ⟨F, hF⟩

Result:
case neg.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
⊢ f.IsInvertible

Proof state:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬f.IsInvertible
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Tactic:
suffices ¬IsUnit ((e.symm : M₂ →L[R] M).comp f) by simp [this, h₁]

Result:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬f.IsInvertible
⊢ ¬IsUnit ((↑e.symm).comp f)

Proof state:
case h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) = f

Tactic:
ext

Result:
case h.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
x✝ : M
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) x✝ = f x✝

Proof state:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Tactic:
rw [← he']

Result:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (Ring.inverse ((↑e.symm).comp ↑e')).comp ↑e.symm

Proof state:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬f.IsInvertible
⊢ ¬IsUnit ((↑e.symm).comp f)

Tactic:
contrapose! h₁

Result:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : IsUnit ((↑e.symm).comp f)
⊢ f.IsInvertible

Proof state:
case pos.intro.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
x✝ : M₂
⊢ (↑e').inverse x✝ = ((Ring.inverse ↑(e'.trans e.symm)).comp ↑e.symm) x✝

Tactic:
simp

Result:
no goals

Proof state:
case neg.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
⊢ f.IsInvertible

Tactic:
use (ContinuousLinearEquiv.unitsEquiv _ _ F).trans e

Result:
case h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) = f