awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
      (((↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f : (a : M) → M₂) x : M₂)
⊢ f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
x : M
⊢ Eq.{u_3 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
    (((↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f : (a : M) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
⊢ f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f

Tactic:
have : f = e.symm ∘L ((e : M₂ →L[R] M₃) ∘L f) := by ext; simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
this : f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f
mp : ((↑e.symm : M₃ →L[R] M₂) ∘SL (↑A : M →L[R] M₃)).IsInvertible
⊢ f.IsInvertible

Tactic:
rw [this, ← hA]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
this : f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f
⊢ ((↑e.symm : M₃ →L[R] M₂) ∘SL (↑A : M →L[R] M₃)).IsInvertible

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M_1 : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M_1
inst_5 : Module R M_1
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
M : M_1 ≃L[R] M₂
⊢ ((↑e : M₂ →L[R] M₃) ∘SL (↑M : M_1 →L[R] M₂)).IsInvertible

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
mp : (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible → f.IsInvertible
mpr : f.IsInvertible → (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible
⊢ (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible ↔ f.IsInvertible

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
      (((f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃) : (a : M) → M₂) x : M₂)
⊢ f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
x : M
⊢ Eq.{u_3 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
    (((f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃) : (a : M) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
⊢ f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)

Tactic:
have : f = (f ∘L (e : M₃ →L[R] M)) ∘L e.symm := by ext; simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
this : f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)
mp : ((↑A : M₃ →L[R] M₂) ∘SL (↑e.symm : M →L[R] M₃)).IsInvertible
⊢ f.IsInvertible

Tactic:
rw [this, ← hA]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
this : f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)
⊢ ((↑A : M₃ →L[R] M₂) ∘SL (↑e.symm : M →L[R] M₃)).IsInvertible

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M_1 : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M_1
inst_5 : Module R M_1
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M_1
M : M_1 ≃L[R] M₂
⊢ ((↑M : M_1 →L[R] M₂) ∘SL (↑e : M₃ →L[R] M_1)).IsInvertible

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
pos : ∀ (hf : f.IsInvertible), ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
neg : ∀ (hf : ¬f.IsInvertible), ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)

Tactic:
by_cases hf : f.IsInvertible

Premises used: ContinuousLinearMap.IsInvertible
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
pos :
  ∀ (A : M ≃L[R] M₂),
    ((↑e : M₂ →L[R] M₃) ∘SL (↑A : M →L[R] M₂)).inverse = (↑A : M →L[R] M₂).inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)

Tactic:
rcases hf with ⟨A, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
A : M ≃L[R] M₂
pos : Eq (α := M₃ ≃L[R] M) (ContinuousLinearEquiv.symm (A.trans e)) (e.symm.trans A.symm)
⊢ ((↑e : M₂ →L[R] M₃) ∘SL (↑A : M →L[R] M₂)).inverse = (↑A : M →L[R] M₂).inverse ∘SL (↑e.symm : M₃ →L[R] M₂)

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

Premises used: ContinuousLinearMap.inverse_equiv, ContinuousLinearEquiv.coe_inj, ContinuousLinearEquiv.comp_coe
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
A : M ≃L[R] M₂
⊢ Eq (α := M₃ ≃L[R] M) (ContinuousLinearEquiv.symm (A.trans e)) (e.symm.trans A.symm)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ ¬((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
neg : 0 = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
neg₁ : Eq (α := M₃ →L[R] M) 0 (comp (σ₂₃ := RingHom.id R) 0 (↑e.symm : M₃ →L[R] M₂))
neg₂ neg₃ : Eq (α := M₃ →L[R] M) 0 0
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)

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

Premises used: ContinuousLinearMap.zero_comp, ContinuousLinearMap.inverse_of_not_isInvertible
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
pos : ∀ (hf : f.IsInvertible), (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
neg : ∀ (hf : ¬f.IsInvertible), (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse

Tactic:
by_cases hf : f.IsInvertible

Premises used: ContinuousLinearMap.IsInvertible
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : f.IsInvertible
pos :
  ∀ (A : M ≃L[R] M₂),
    ((↑A : M →L[R] M₂) ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL (↑A : M →L[R] M₂).inverse
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse

Tactic:
rcases hf with ⟨A, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
pos : Eq (α := M₂ ≃L[R] M₃) (ContinuousLinearEquiv.symm (e.trans A)) (A.symm.trans e.symm)
⊢ ((↑A : M →L[R] M₂) ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL (↑A : M →L[R] M₂).inverse

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

Premises used: ContinuousLinearMap.inverse_equiv, ContinuousLinearEquiv.coe_inj, ContinuousLinearEquiv.comp_coe
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ Eq (α := M₂ ≃L[R] M₃) (ContinuousLinearEquiv.symm (e.trans A)) (A.symm.trans e.symm)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ ¬(f ∘SL (↑e : M₃ →L[R] M)).IsInvertible

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
neg : 0 = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
neg₁ : Eq (α := M₂ →L[R] M₃) 0 ((↑e.symm : M →L[R] M₃).comp (σ₁₂ := RingHom.id R) 0)
neg₂ neg₃ : Eq (α := M₂ →L[R] M₃) 0 0
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse

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

Premises used: ContinuousLinearMap.comp_zero, ContinuousLinearMap.inverse_of_not_isInvertible
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
rcases : ∀ (N : M₂ ≃L[R] M₃), ((↑N : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑N : M₂ →L[R] M₃).inverse
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
rcases hg with ⟨N, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M →L[R] M₂
N : M₂ ≃L[R] M₃
⊢ ((↑N : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑N : M₂ →L[R] M₃).inverse

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
v : M₃
hg : g.IsInvertible
⊢ Eq.{u_2 + 1} (α := M) (((g ∘SL f).inverse : (a : M₃) → M) v : M)
    ((f.inverse : (a : M₂) → M) ((g.inverse : (a : M₃) → M₂) v : M₂) : M)

Tactic:
simp only [hg.inverse_comp_of_left, coe_comp', Function.comp_apply]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.IsInvertible.inverse_comp_of_left, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
rcases : ∀ (M_1 : M ≃L[R] M₂), (g ∘SL (↑M_1 : M →L[R] M₂)).inverse = (↑M_1 : M →L[R] M₂).inverse ∘SL g.inverse
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
rcases hf with ⟨M, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M_1 : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M_1
inst_5 : Module R M_1
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
M : M_1 ≃L[R] M₂
⊢ (g ∘SL (↑M : M_1 →L[R] M₂)).inverse = (↑M : M_1 →L[R] M₂).inverse ∘SL g.inverse

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
v : M₃
hf : f.IsInvertible
⊢ Eq.{u_2 + 1} (α := M) (((g ∘SL f).inverse : (a : M₃) → M) v : M)
    ((f.inverse : (a : M₂) → M) ((g.inverse : (a : M₃) → M₂) v : M₂) : M)

Tactic:
simp only [hf.inverse_comp_of_right, coe_comp', Function.comp_apply]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.IsInvertible.inverse_comp_of_right, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace M
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
e : M ≃L[R] M
this :
  (↑((MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M) : (a : M ≃L[R] M) → (M →L[R] M)ˣ) e) : M →L[R] M)⁻¹ʳ =
    (↑e : M →L[R] M).inverse
⊢ (↑((MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M) : (a : M ≃L[R] M) → (M →L[R] M)ˣ) e) : M →L[R] M)⁻¹ʳ =
    (↑e : M →L[R] M).inverse

Tactic:
this
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace M
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
e : M ≃L[R] M
this :
  (↑((MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M) : (a : M ≃L[R] M) → (M →L[R] M)ˣ) e) : M →L[R] M)⁻¹ʳ =
    (↑e : M →L[R] M).inverse
⊢ (↑e : M →L[R] M)⁻¹ʳ = (↑e : M →L[R] M).inverse

Tactic:
convert! this
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace M
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
e : M ≃L[R] M
simp :
  (↑((MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M) : (a : M ≃L[R] M) → (M →L[R] M)ˣ) e)⁻¹ : M →L[R] M) =
    (↑e.symm : M →L[R] M)
⊢ (↑((MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M) : (a : M ≃L[R] M) → (M →L[R] M)ˣ) e) : M →L[R] M)⁻¹ʳ =
    (↑e : M →L[R] M).inverse

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace M
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
e : M ≃L[R] M
⊢ (↑((MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M) : (a : M ≃L[R] M) → (M →L[R] M)ˣ) e)⁻¹ : M →L[R] M) =
    (↑e.symm : M →L[R] M)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
pos : ∀ (h₁ : f.IsInvertible), f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
neg : ∀ (h₁ : ¬f.IsInvertible), f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
by_cases h₁ : f.IsInvertible

Premises used: ContinuousLinearMap.IsInvertible
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : f.IsInvertible
pos :
  ∀ (e' : M ≃L[R] M₂) (he' : (↑e' : M →L[R] M₂) = f),
    f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
obtain ⟨e', he'⟩ := h₁
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : (↑e' : M →L[R] M₂) = f
pos : (↑e' : M →L[R] M₂).inverse = ((↑e.symm : M₂ →L[R] M) ∘SL (↑e' : M →L[R] M₂))⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
rw [← he']
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : (↑e' : M →L[R] M₂) = f
pos : (↑e' : M →L[R] M₂).inverse = (↑(e'.trans e.symm) : M →L[R] M)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
⊢ (↑e' : M →L[R] M₂).inverse = ((↑e.symm : M₂ →L[R] M) ∘SL (↑e' : M →L[R] M₂))⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
change _ = (e'.trans e.symm : M →L[R] M)⁻¹ʳ ∘L (e.symm : M₂ →L[R] M)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.trans, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : (↑e' : M →L[R] M₂) = f
pos :
  ∀ (x : M₂),
    Eq.{u_2 + 1} (α := M) (((↑e' : M →L[R] M₂).inverse : (a : M₂) → M) x : M)
      (((↑(e'.trans e.symm) : M →L[R] M)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M) : (a : M₂) → M) x : M)
⊢ (↑e' : M →L[R] M₂).inverse = (↑(e'.trans e.symm) : M →L[R] M)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
ext