awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_3
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
M₂ : Type u_4
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_8 : RingHomInvPair σ₁₂ σ₂₁
inst_9 : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
x : M
⊢ Eq.{u_4 + 1} (α := M₂) ((e : (a : M) → M₂) (-x) : M₂) (-(e : (a : M) → M₂) x : M₂)

Tactic:
(e : M →SL[σ₁₂] M₂).map_neg x

Premises used: ContinuousLinearMap.map_neg, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_3
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
M₂ : Type u_4
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_8 : RingHomInvPair σ₁₂ σ₂₁
inst_9 : RingHomInvPair σ₂₁ σ₁₂
inst_10 : Module R M₂
inst_11 : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f₂ : (a : M₂) → M) (⇑f₁ : (a : M) → M₂)
x : M
⊢ (f₂.coprod (↑f₁ : M →ₗ[R] M₂).ker.subtypeL : (a : M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker) → M)
      ((f₁.prod (f₁.projKerOfRightInverse f₂ h) : (a : M) → M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker) x :
        Prod.{u_4, u_3} M₂ ↥(↑f₁ : M →ₗ[R] M₂).ker) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_3
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
M₂ : Type u_4
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_8 : RingHomInvPair σ₁₂ σ₂₁
inst_9 : RingHomInvPair σ₂₁ σ₁₂
inst_10 : Module R M₂
inst_11 : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f₂ : (a : M₂) → M) (⇑f₁ : (a : M) → M₂)
x_1 : Prod.{u_4, u_3} M₂ ↥(↑f₁ : M →ₗ[R] M₂).ker
x : M₂
y : ↥(↑f₁ : M →ₗ[R] M₂).ker
⊢ (f₁.prod (f₁.projKerOfRightInverse f₂ h) : (a : M) → M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker)
      ((f₂.coprod (↑f₁ : M →ₗ[R] M₂).ker.subtypeL : (a : M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker) → M) (x, y)) =
    (x, y)

Tactic:
simp [h x]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
M₂ : Type u_4
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f₂ : (a : M₂) → M) (⇑f₁ : (a : M) → M₂)
x : M
⊢ Eq.{u_4 + 1} (α := M₂) (((equivOfRightInverse f₁ f₂ h : (a : M) → M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker) x).1 : M₂)
    ((f₁ : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
M₂ : Type u_4
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f₂ : (a : M₂) → M) (⇑f₁ : (a : M) → M₂)
x : M
⊢ (↑((equivOfRightInverse f₁ f₂ h : (a : M) → M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker) x).2 : M) =
    HSub.hSub (β := M) x ((f₂ : (a : M₂) → M) ((f₁ : (a : M) → M₂) x : M₂) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
M₂ : Type u_4
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f₂ : (a : M₂) → M) (⇑f₁ : (a : M) → M₂)
y : Prod.{u_4, u_3} M₂ ↥(↑f₁ : M →ₗ[R] M₂).ker
⊢ ((equivOfRightInverse f₁ f₂ h).symm : (a : M₂ × ↥(↑f₁ : M →ₗ[R] M₂).ker) → M) y =
    HAdd.hAdd (α := M) ((f₂ : (a : M₂) → M) y.1 : M) (↑y.2 : M)

Tactic:
rfl

Premises used: 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₂
f : M ≃L[R] M₂
⊢ (↑f : M →L[R] M₂).IsInvertible

Tactic:
⟨f, rfl⟩

Premises used: ContinuousLinearMap.IsInvertible, Exists.intro, 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₂
⊢ (↑e : M →L[R] M₂).inverse = (↑e.symm : M₂ →L[R] M)

Tactic:
simp [inverse]

Premises used: ContinuousLinearMap.inverse
-- 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₂
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ f.inverse = 0

Tactic:
dif_neg hf

Premises used: dif_neg, ContinuousLinearMap.inverse
-- 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₂
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0 ↔ Subsingleton M ∧ Subsingleton M₂

Tactic:
⟨fun ⟨e, he⟩ ↦ ?_, ?_⟩

Premises used: _private.0.ContinuousLinearMap.isInvertible_zero_iff.match_1, And, Iff.intro, Subsingleton
-- 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₂
refine_1 :
  IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0 →
    ∀ (e : M ≃L[R] M₂) (he : (↑e : M →L[R] M₂) = 0), Subsingleton M ∧ Subsingleton M₂
refine_2 : Subsingleton M ∧ Subsingleton M₂ → IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0 ↔ Subsingleton M ∧ Subsingleton M₂

Tactic:
refine ⟨fun ⟨e, 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
e : M ≃L[R] M₂
he : (↑e : M →L[R] M₂) = 0
⊢ Subsingleton M

Tactic:
⟨fun x y ↦ e.injective ?_⟩

Premises used: ContinuousLinearEquiv.injective, Subsingleton.intro
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
e : M ≃L[R] M₂
he : (↑e : M →L[R] M₂) = 0
refine : ∀ (x y : M), Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) y : M₂)
⊢ Subsingleton M

Tactic:
refine ⟨fun x y ↦ e.injective ?_⟩
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
e : M ≃L[R] M₂
he : (↑e : M →L[R] M₂) = 0
x y : M
⊢ Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) y : M₂)

Tactic:
simp [he, ← ContinuousLinearEquiv.coe_coe]

Premises used: ContinuousLinearEquiv.coe_coe
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
e : M ≃L[R] M₂
he : (↑e : M →L[R] M₂) = 0
⊢ Subsingleton M

Tactic:
have A : Subsingleton M := by
      refine ⟨fun x y ↦ e.injective ?_⟩
      simp [he, ← ContinuousLinearEquiv.coe_coe]
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
e : M ≃L[R] M₂
he : (↑e : M →L[R] M₂) = 0
A : Subsingleton M
⊢ Subsingleton M ∧ Subsingleton M₂

Tactic:
⟨A, e.toEquiv.symm.subsingleton⟩

Premises used: ContinuousLinearEquiv.toLinearEquiv, And.intro, LinearEquiv.toEquiv, Equiv.symm, Equiv.subsingleton
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
e : M ≃L[R] M₂
he : (↑e : M →L[R] M₂) = 0
A : Subsingleton M
⊢ Subsingleton M ∧ Subsingleton M₂

Tactic:
exact ⟨A, e.toEquiv.symm.subsingleton⟩
-- 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₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0

Tactic:
⟨e, ?_⟩

Premises used: ContinuousLinearMap.IsInvertible, Exists.intro
-- 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₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
refine_2 : (↑e : M →L[R] M₂) = 0
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0

Tactic:
refine ⟨e, ?_⟩
-- 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₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
refine_2 : ∀ (x : M), Eq.{u_3 + 1} (α := M₂) (((↑e : M →L[R] M₂) : (a : M) → M₂) x : M₂) ((0 : (a : M) → M₂) x : M₂)
⊢ (↑e : M →L[R] M₂) = 0

Tactic:
ext x
-- 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₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
x : M
⊢ Eq.{u_3 + 1} (α := M₂) (((↑e : M →L[R] M₂) : (a : M) → M₂) x : M₂) ((0 : (a : M) → M₂) x : M₂)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
x : M
⊢ Eq.{u_3 + 1} (α := M₂) (((↑e : M →L[R] M₂) : (a : M) → M₂) x : M₂) ((0 : (a : M) → M₂) x : M₂)

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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₂
pos : ∀ (h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0), Eq (α := M₂ →L[R] M) (inverse 0) 0
neg : ∀ (h : ¬IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0), Eq (α := M₂ →L[R] M) (inverse 0) 0
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0

Tactic:
by_cases h : IsInvertible (0 : M →L[R] M₂)

Premises used: ContinuousLinearMap.IsInvertible, OfNat.ofNat
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
⊢ Subsingleton M

Tactic:
rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩

Premises used: ContinuousLinearMap.isInvertible_zero_iff, Iff.mp
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
hM : Subsingleton M
⊢ Subsingleton M₂

Tactic:
rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩

Premises used: ContinuousLinearMap.isInvertible_zero_iff, Iff.mp
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
pos : ∀ (x : M₂), Eq.{u_2 + 1} (α := M) ((inverse 0 : (a : M₂) → M) x : M) ((0 : (a : M₂) → M) x : M)
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0

Tactic:
ext x
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
x : M₂
⊢ Eq.{u_2 + 1} (α := M) ((inverse 0 : (a : M₂) → M) x : M) ((0 : (a : M₂) → M) x : M)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
x : M₂
⊢ Eq.{u_2 + 1} (α := M) ((inverse 0 : (a : M₂) → M) x : M) ((0 : (a : M₂) → M) x : M)

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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₂
h : ¬IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0

Tactic:
inverse_of_not_isInvertible h

Premises used: ContinuousLinearMap.inverse_of_not_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₂
h : ¬IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0

Tactic:
exact inverse_of_not_isInvertible h

Premises used: 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
hf : f.IsInvertible
rcases : ∀ (N : M₂ ≃L[R] M₃), ((↑N : M₂ →L[R] M₃) ∘SL f).IsInvertible
⊢ (g ∘SL f).IsInvertible

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₂
hf : f.IsInvertible
N : M₂ ≃L[R] M₃
rcases : ∀ (M_1 : M ≃L[R] M₂), ((↑N : M₂ →L[R] M₃) ∘SL (↑M_1 : M →L[R] M₂)).IsInvertible
⊢ ((↑N : M₂ →L[R] M₃) ∘SL f).IsInvertible

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₃
N : M₂ ≃L[R] M₃
M : M_1 ≃L[R] M₂
⊢ ((↑N : M₂ →L[R] M₃) ∘SL (↑M : M_1 →L[R] M₂)).IsInvertible

Tactic:
⟨M.trans N, rfl⟩

Premises used: ContinuousLinearMap.IsInvertible, ContinuousLinearEquiv.trans, Exists.intro, 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₃
N : M₂ ≃L[R] M₃
M : M_1 ≃L[R] M₂
⊢ ((↑N : M₂ →L[R] M₃) ∘SL (↑M : M_1 →L[R] M₂)).IsInvertible

Tactic:
exact ⟨M.trans N, 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₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
⊢ f.IsInvertible

Tactic:
⟨ContinuousLinearEquiv.equivOfInverse' _ _ hf hg, rfl⟩

Premises used: ContinuousLinearEquiv.equivOfInverse', ContinuousLinearMap.IsInvertible, Exists.intro, 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₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
⊢ f = (↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg) : M →L[R] M₂)

Tactic:
have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := 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₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
this : f = (↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg) : M →L[R] M₂)
rw : (↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.equivOfInverse' f g hf hg)) : M₂ →L[R] M) = g
⊢ f.inverse = g

Tactic:
rw [this, inverse_equiv]

Premises used: ContinuousLinearMap.inverse_equiv
-- 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₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
this : f = (↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg) : M →L[R] M₂)
⊢ (↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.equivOfInverse' f g hf hg)) : M₂ →L[R] M) = g

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₂
f : M →L[R] M₂
x : M
y : M₂
hf : f.IsInvertible
rcases :
  ∀ (M_1 : M ≃L[R] M₂), ((↑M_1 : M →L[R] M₂).inverse : (a : M₂) → M) y = x ↔ y = ((↑M_1 : M →L[R] M₂) : (a : M) → M₂) x
⊢ (f.inverse : (a : M₂) → M) y = x ↔ y = (f : (a : M) → M₂) x

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
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
x : M_1
y : M₂
M : M_1 ≃L[R] M₂
simp : (M.symm : (a : M₂) → M_1) y = x ↔ y = (M : (a : M_1) → M₂) x
⊢ ((↑M : M_1 →L[R] M₂).inverse : (a : M₂) → M_1) y = x ↔ y = ((↑M : M_1 →L[R] M₂) : (a : M_1) → M₂) x

Tactic:
simp only [inverse_equiv, ContinuousLinearEquiv.coe_coe]

Premises used: ContinuousLinearMap.inverse_equiv, ContinuousLinearEquiv.coe_coe
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M_1 : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
x : M_1
y : M₂
M : M_1 ≃L[R] M₂
⊢ (M.symm : (a : M₂) → M_1) y = x ↔ y = (M : (a : M_1) → M₂) x

Tactic:
ContinuousLinearEquiv.symm_apply_eq M

Premises used: ContinuousLinearEquiv.symm_apply_eq
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M_1 : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
x : M_1
y : M₂
M : M_1 ≃L[R] M₂
⊢ (M.symm : (a : M₂) → M_1) y = x ↔ y = (M : (a : M_1) → M₂) x

Tactic:
exact ContinuousLinearEquiv.symm_apply_eq M

Premises used: ContinuousLinearEquiv.symm_apply_eq
-- 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 : ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible → f.IsInvertible
mpr : f.IsInvertible → ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible ↔ f.IsInvertible

Tactic:
constructor