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
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
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)

Tactic:
simp
-- 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
this : ¬IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
simp [this, 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₂
h₁ : ¬f.IsInvertible
neg : ¬IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)

Tactic:
suffices ¬IsUnit ((e.symm : M₂ →L[R] M).comp f) by simp [this, 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₂
h₁ : ¬f.IsInvertible
neg : ∀ (h₁ : IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)), f.IsInvertible
⊢ ¬IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)

Tactic:
contrapose 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₂
h₁ : IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)
neg : ∀ (F : (M →L[R] M)ˣ) (hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f), f.IsInvertible
⊢ f.IsInvertible

Tactic:
rcases h₁ with ⟨F, hF⟩
-- 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₂
F : (M →L[R] M)ˣ
hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f
h :
  (↑(ContinuousLinearEquiv.trans ((ContinuousLinearEquiv.unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) F) e) :
      M →L[R] M₂) =
    f
⊢ f.IsInvertible

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

Premises used: ContinuousLinearEquiv.trans, ContinuousLinearEquiv.unitsEquiv, DFunLike.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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := M₂)
      (((↑(ContinuousLinearEquiv.trans ((ContinuousLinearEquiv.unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) F) e) :
              M →L[R] M₂) :
            (a : M) → M₂)
          x :
        M₂)
      ((f : (a : M) → M₂) x : M₂)
⊢ (↑(ContinuousLinearEquiv.trans ((ContinuousLinearEquiv.unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) F) e) :
      M →L[R] M₂) =
    f

Tactic:
ext
-- 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₂
F : (M →L[R] M)ˣ
hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f
x : M
h :
  Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) (((↑F : M →L[R] M) : (a : M) → M) x : M) : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_3 + 1} (α := M₂)
    (((↑(ContinuousLinearEquiv.trans ((ContinuousLinearEquiv.unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) F) e) :
            M →L[R] M₂) :
          (a : M) → M₂)
        x :
      M₂)
    ((f : (a : M) → M₂) x : M₂)

Tactic:
dsimp
-- 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₂
F : (M →L[R] M)ˣ
hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f
x : M
h :
  Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) (((↑e.symm : M₂ →L[R] M) ∘SL f : (a : M) → M) x : M) : M₂)
    ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) (((↑F : M →L[R] M) : (a : M) → M) x : M) : M₂) ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [hF]
-- 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₂
F : (M →L[R] M)ˣ
hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f
x : M
⊢ Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) (((↑e.symm : M₂ →L[R] M) ∘SL f : (a : M) → M) x : M) : M₂)
    ((f : (a : M) → M₂) x : M₂)

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
h : ∀ (x : M →L[R] M) (x_1 : M), Eq (α := M) ((x⁻¹ʳ : (a : M) → M) x_1 : M) ((x.inverse : (a : M) → M) x_1 : M)
⊢ Eq.{u_2 + 1} (α := (M →L[R] M) → M →L[R] M) Ring.inverse inverse

Tactic:
ext
-- 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
x : M →L[R] M
x_1 : M
⊢ Eq (α := M) ((x⁻¹ʳ : (a : M) → M) x_1 : M) ((x.inverse : (a : M) → M) x_1 : M)

Tactic:
simp [inverse_eq_ringInverse (ContinuousLinearEquiv.refl R M)]

Premises used: ContinuousLinearEquiv.refl, ContinuousLinearMap.inverse_eq_ringInverse
-- 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
rw : Eq (α := M →L[R] M) (ContinuousLinearMap.id R M)⁻¹ʳ (ContinuousLinearMap.id R M)
⊢ Eq (α := M →L[R] M) (inverse (ContinuousLinearMap.id R M)) (ContinuousLinearMap.id R M)

Tactic:
rw [← ringInverse_eq_inverse]

Premises used: ContinuousLinearMap.ringInverse_eq_inverse
-- 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
⊢ Eq (α := M →L[R] M) (ContinuousLinearMap.id R M)⁻¹ʳ (ContinuousLinearMap.id R M)

Tactic:
Ring.inverse_one _

Premises used: Ring.inverse_one
-- 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
⊢ Eq (α := M →L[R] M) (ContinuousLinearMap.id R M)⁻¹ʳ (ContinuousLinearMap.id R M)

Tactic:
exact Ring.inverse_one _

Premises used: Ring.inverse_one
-- 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
rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂) ∘SL (↑e : M →L[R] M₂).inverse = ContinuousLinearMap.id R M₂
⊢ f ∘SL f.inverse = ContinuousLinearMap.id R M₂

Tactic:
rcases hf with ⟨e, 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₂
e : M ≃L[R] M₂
⊢ (↑e : M →L[R] M₂) ∘SL (↑e : M →L[R] M₂).inverse = ContinuousLinearMap.id R M₂

Tactic:
simp
-- 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
y : M₂
rcases : ∀ (e : M ≃L[R] M₂), ((↑e : M →L[R] M₂) : (a : M) → M₂) (((↑e : M →L[R] M₂).inverse : (a : M₂) → M) y : M) = y
⊢ (f : (a : M) → M₂) ((f.inverse : (a : M₂) → M) y : M) = y

Tactic:
rcases hf with ⟨e, 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₂
y : M₂
e : M ≃L[R] M₂
⊢ ((↑e : M →L[R] M₂) : (a : M) → M₂) (((↑e : M →L[R] M₂).inverse : (a : M₂) → M) y : M) = y

Tactic:
simp
-- 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
rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂).inverse ∘SL (↑e : M →L[R] M₂) = ContinuousLinearMap.id R M
⊢ f.inverse ∘SL f = ContinuousLinearMap.id R M

Tactic:
rcases hf with ⟨e, 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₂
e : M ≃L[R] M₂
⊢ (↑e : M →L[R] M₂).inverse ∘SL (↑e : M →L[R] M₂) = ContinuousLinearMap.id R M

Tactic:
simp
-- 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
y : M
rcases : ∀ (e : M ≃L[R] M₂), ((↑e : M →L[R] M₂).inverse : (a : M₂) → M) (((↑e : M →L[R] M₂) : (a : M) → M₂) y : M₂) = y
⊢ (f.inverse : (a : M₂) → M) ((f : (a : M) → M₂) y : M₂) = y

Tactic:
rcases hf with ⟨e, 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₂
y : M
e : M ≃L[R] M₂
⊢ ((↑e : M →L[R] M₂).inverse : (a : M₂) → M) (((↑e : M →L[R] M₂) : (a : M) → M₂) y : M₂) = y

Tactic:
simp
-- 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
rcases :
  ∀ (e : M ≃L[R] M₂), Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑(↑e : M →L[R] M₂) : (a : M) → M₂)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)

Tactic:
rcases hf with ⟨e, 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₂
e : M ≃L[R] M₂
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑(↑e : M →L[R] M₂) : (a : M) → M₂)

Tactic:
simp [ContinuousLinearEquiv.bijective]

Premises used: ContinuousLinearEquiv.bijective
-- 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
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)

Tactic:
hf.bijective.injective

Premises used: ContinuousLinearMap.IsInvertible.bijective, Function.Bijective.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₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)

Tactic:
hf.bijective.surjective

Premises used: ContinuousLinearMap.IsInvertible.bijective, Function.Bijective.surjective
-- 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
rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂).inverse.IsInvertible
⊢ f.inverse.IsInvertible

Tactic:
rcases hf with ⟨e, 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₂
e : M ≃L[R] M₂
⊢ (↑e : M →L[R] M₂).inverse.IsInvertible

Tactic:
simp
-- 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
rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂).inverse.inverse = (↑e : M →L[R] M₂)
⊢ f.inverse.inverse = f

Tactic:
rcases hf with ⟨e, 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₂
e : M ≃L[R] M₂
⊢ (↑e : M →L[R] M₂).inverse.inverse = (↑e : M →L[R] M₂)

Tactic:
simp
-- 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.inverse.IsInvertible
by_contra : ∀ (H : ¬f.IsInvertible), False
⊢ f.IsInvertible

Tactic:
by_contra 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₂
f : M →L[R] M₂
hf : f.inverse.IsInvertible
H : ¬f.IsInvertible
⊢ Subsingleton M₂ ∧ Subsingleton M

Tactic:
simpa [inverse, H] using hf

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.inverse.IsInvertible
H : ¬f.IsInvertible
⊢ Subsingleton M₂

Tactic:
obtain ⟨_, _⟩ : Subsingleton M₂ ∧ Subsingleton M := by simpa [inverse, H] using hf

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

Tactic:
obtain ⟨_, _⟩ : Subsingleton M₂ ∧ Subsingleton M := by simpa [inverse, H] using hf

Premises used: 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₂
f : M →L[R] M₂
hf : f.inverse.IsInvertible
H : ¬f.IsInvertible
left : Subsingleton M₂
right : Subsingleton M
⊢ False

Tactic:
simp_all [Subsingleton.elim f 0]

Premises used: Subsingleton.elim, 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₂
f : M →L[R] M₂
⊢ f.inverse.IsInvertible ↔ f.IsInvertible

Tactic:
⟨.of_isInvertible_inverse, .inverse⟩

Premises used: ContinuousLinearMap.IsInvertible.inverse, ContinuousLinearMap.IsInvertible.of_isInvertible_inverse, Iff.intro
-- 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₃
inst_10 : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
hl :
  ∀ (x : M₃),
    Eq.{u_2 + 1} (α := M)
      (((f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃)) ∘SL inl R M₃ M₂ :
            (a : M₃) → M)
          x :
        M)
      ((g.coprod f ∘SL inl R M₃ M₂ : (a : M₃) → M) x : M)
hr :
  ∀ (x : M₂),
    Eq.{u_2 + 1} (α := M)
      (((f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃)) ∘SL inr R M₃ M₂ :
            (a : M₂) → M)
          x :
        M)
      ((g.coprod f ∘SL inr R M₃ M₂ : (a : M₂) → M) x : M)
⊢ f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃) = g.coprod 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₃
inst_10 : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x : M₃
⊢ Eq.{u_2 + 1} (α := M)
    (((f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃)) ∘SL inl R M₃ M₂ :
          (a : M₃) → M)
        x :
      M)
    ((g.coprod f ∘SL inl R M₃ 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₃
inst_10 : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x : M₂
⊢ Eq.{u_2 + 1} (α := M)
    (((f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃)) ∘SL inr R M₃ M₂ :
          (a : M₂) → M)
        x :
      M)
    ((g.coprod f ∘SL inr R M₃ M₂ : (a : M₂) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
⊢ Eq.{u_3 + 1} (α := (x : M) → Prop) (fun (x : M) ↦ x ∈ p) fun (x : M) ↦ x ∈ q

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
⊢ Eq.{u_3 + 1} (α := (x : M) → Prop) (fun (x : M) ↦ x ∈ p) fun (x : M) ↦ x ∈ q

Tactic:
have h' : (fun x ↦ x ∈ p) = (fun x ↦ x ∈ q) := by simp [h]
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
h' : Eq.{u_3 + 1} (α := (x : M) → Prop) (fun (x : M) ↦ x ∈ p) fun (x : M) ↦ x ∈ q
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (↑(LinearEquiv.ofEq p q h) : ↥p →ₗ[R] ↥q).toFun

Tactic:
(Homeomorph.ofEqSubtypes h').continuous

Premises used: Homeomorph.continuous, Homeomorph.ofEqSubtypes
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
h' : Eq.{u_3 + 1} (α := (x : M) → Prop) (fun (x : M) ↦ x ∈ p) fun (x : M) ↦ x ∈ q
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (↑(LinearEquiv.ofEq p q h) : ↥p →ₗ[R] ↥q).toFun

Tactic:
exact (Homeomorph.ofEqSubtypes h').continuous

Premises used: Homeomorph.continuous, Homeomorph.ofEqSubtypes
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
h' : Eq.{u_3 + 1} (α := (x : M) → Prop) (fun (x : M) ↦ x ∈ p) fun (x : M) ↦ x ∈ q
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (LinearEquiv.ofEq p q h).invFun

Tactic:
(Homeomorph.ofEqSubtypes h').symm.continuous

Premises used: Homeomorph.continuous, Homeomorph.symm, Homeomorph.ofEqSubtypes
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M₂
inst_5 : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
h' : Eq.{u_3 + 1} (α := (x : M) → Prop) (fun (x : M) ↦ x ∈ p) fun (x : M) ↦ x ∈ q
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (LinearEquiv.ofEq p q h).invFun

Tactic:
exact (Homeomorph.ofEqSubtypes h').symm.continuous

Premises used: Homeomorph.continuous, Homeomorph.symm, Homeomorph.ofEqSubtypes