-- Mathlib/Topology/Algebra/Module/Equiv.lean
@[simp] lemma inverse_comp_equiv {e : M₃ ≃L[R] M} {f : M →L[R] M₂} :
    (f ∘L e).inverse = (e.symm : M →L[R] M₃) ∘L f.inverse

Proof state:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ 0 = (↑e.symm).comp 0

Tactic:
simp

Result:
no goals

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

Tactic:
by_cases hf : f.IsInvertible

Result:
case pos
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (f.comp ↑e).inverse = (↑e.symm).comp f.inverse

case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (f.comp ↑e).inverse = (↑e.symm).comp f.inverse

Proof state:
case pos
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (f.comp ↑e).inverse = (↑e.symm).comp f.inverse

Tactic:
rcases hf with ⟨A, rfl⟩

Result:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ ((↑A).comp ↑e).inverse = (↑e.symm).comp (↑A).inverse

Proof state:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ (e.trans A).symm = A.symm.trans e.symm

Tactic:
rfl

Result:
no goals

Proof state:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ ((↑A).comp ↑e).inverse = (↑e.symm).comp (↑A).inverse

Tactic:
simp only [ContinuousLinearEquiv.comp_coe, inverse_equiv, ContinuousLinearEquiv.coe_inj]

Result:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ (e.trans A).symm = A.symm.trans e.symm

Proof state:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (f.comp ↑e).inverse = (↑e.symm).comp f.inverse

Tactic:
rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf]

Result:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ 0 = (↑e.symm).comp 0

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ ¬(f.comp ↑e).IsInvertible

Tactic:
simp [hf]

Result:
no goals