awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse
have 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
Tactic: rcases hf with ⟨M, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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 : M →L[R] M).inverse
have 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)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
have pos : ∀ (h₁ : f.IsInvertible), f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
Tactic: by_cases h₁ : f.IsInvertible
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
have neg : ∀ (h₁ : ¬f.IsInvertible), f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
Tactic: by_cases h₁ : f.IsInvertible
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
have 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)
Tactic: obtain ⟨e', he'⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
have 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)
Tactic: rw [← he']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ (↑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)
have pos : (↑e' : M →L[R] M₂).inverse = (↑(e'.trans e.symm) : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ (↑e' : M →L[R] M₂).inverse = (↑(e'.trans e.symm) : M →L[R] M)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ f.inverse = ((↑e.symm : M₂ →L[R] M) ∘SL f)⁻¹ʳ ∘SL (↑e.symm : M₂ →L[R] M)
have neg : ¬IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)
Tactic: suffices ¬IsUnit ((e.symm : M₂ →L[R] M).comp f) by simp [this, h₁]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ ¬IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)
have neg : ∀ (h₁ : IsUnit ((↑e.symm : M₂ →L[R] M) ∘SL f)), f.IsInvertible
Tactic: contrapose h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
⊢ f.IsInvertible
have neg : ∀ (F : (M →L[R] M)ˣ) (hF : (↑F : M →L[R] M) = (↑e.symm : M₂ →L[R] M) ∘SL f), f.IsInvertible
Tactic: rcases h₁ with ⟨F, hF⟩
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ f.IsInvertible
have h : (↑(ContinuousLinearEquiv.trans ((ContinuousLinearEquiv.unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) F) e) :
    M →L[R] M₂) =
  f
Tactic: use (ContinuousLinearEquiv.unitsEquiv _ _ F).trans e
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ (↑(ContinuousLinearEquiv.trans ((ContinuousLinearEquiv.unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) F) e) :
      M →L[R] M₂) =
    f
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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₂)
    (((↑(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₂)
have 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₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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₂) (((↑F : M →L[R] M) : (a : M) → M) x : M) : M₂) ((f : (a : M) → M₂) x : M₂)
have 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₂)
Tactic: rw [hF]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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.{u_2 + 1} (α := (M →L[R] M) → M →L[R] M) Ring.inverse inverse
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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) (inverse (ContinuousLinearMap.id R M)) (ContinuousLinearMap.id R M)
have rw : Eq (α := M →L[R] M) (ContinuousLinearMap.id R M)⁻¹ʳ (ContinuousLinearMap.id R M)
Tactic: rw [← ringInverse_eq_inverse]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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 ∘SL f.inverse = ContinuousLinearMap.id R M₂
have rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂) ∘SL (↑e : M →L[R] M₂).inverse = ContinuousLinearMap.id R M₂
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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₂
⊢ (f : (a : M) → M₂) ((f.inverse : (a : M₂) → M) y : M) = y
have 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
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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 ∘SL f = ContinuousLinearMap.id R M
have rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂).inverse ∘SL (↑e : M →L[R] M₂) = ContinuousLinearMap.id R M
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ (f.inverse : (a : M₂) → M) ((f : (a : M) → M₂) y : M₂) = y
have 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
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
have rcases : ∀ (e : M ≃L[R] M₂), Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑(↑e : M →L[R] M₂) : (a : M) → M₂)
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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.IsInvertible
have rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂).inverse.IsInvertible
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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.inverse = f
have rcases : ∀ (e : M ≃L[R] M₂), (↑e : M →L[R] M₂).inverse.inverse = (↑e : M →L[R] M₂)
Tactic: rcases hf with ⟨e, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ f.IsInvertible
have by_contra : ∀ (H : ¬f.IsInvertible), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
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
⊢ False
have left : Subsingleton M₂
Tactic: obtain ⟨_, _⟩ : Subsingleton M₂ ∧ Subsingleton M := by simpa [inverse, H] using hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
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₂
⊢ False
have right : Subsingleton M
Tactic: obtain ⟨_, _⟩ : Subsingleton M₂ ∧ Subsingleton M := by simpa [inverse, H] using hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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
⊢ f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃) = g.coprod f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
⊢ f.coprod g ∘SL (↑(ContinuousLinearEquiv.prodComm R M₃ M₂) : M₃ × M₂ →L[R] M₂ × M₃) = g.coprod f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (↑(LinearEquiv.ofEq p q h) : ↥p →ₗ[R] ↥q).toFun
have h' : 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (LinearEquiv.ofEq p q h).invFun
have h' : 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddCommMonoid G
inst_13 : Module R G
inst_14 : TopologicalSpace G
inst_15 : Module S G
inst_16 : ContinuousConstSMul S G
inst_17 : SMulCommClass R S W
inst_18 : SMul S R
inst_19 : IsScalarTower S R V
inst_20 : IsScalarTower S R W
inst_21 : SMulCommClass R S V
inst_22 : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ (α • e).trans f = HSMul.hSMul (β := G ≃L[R] W) α (e.trans f)
have h : ∀ (x : G),
  Eq.{u_4 + 1} (α := W) (((α • e).trans f : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃L[R] W) α (e.trans f) : (a : G) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : Module S V
inst_6 : ContinuousConstSMul S V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : Module S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddCommMonoid G
inst_13 : Module R G
inst_14 : TopologicalSpace G
inst_15 : Module S G
inst_16 : ContinuousConstSMul S G
inst_17 : SMulCommClass R S W
inst_18 : SMul S R
inst_19 : IsScalarTower S R V
inst_20 : IsScalarTower S R W
inst_21 : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ e.trans (α • f) = HSMul.hSMul (β := G ≃L[R] W) α (e.trans f)
have h : ∀ (x : G),
  Eq.{u_4 + 1} (α := W) ((e.trans (α • f) : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃L[R] W) α (e.trans f) : (a : G) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ t = UniformSpace.toTopologicalSpace
have refine_1 : LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
Tactic: refine IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
refine_1 : LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
⊢ t = UniformSpace.toTopologicalSpace
have refine_2 : LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
Tactic: refine IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ LE.le.{u} (α := Filter 𝕜) (𝓝 0) (𝓝 0)
have refine_1 : ∀ (i' : ℝ), 0 < i' → Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 i')
Tactic: rw [Metric.nhds_basis_closedBall.ge_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)
have refine_1 : ∀ (ξ₀ : 𝕜) (hξ₀ : 0 < ‖ξ₀‖) (hξ₀ε : ‖ξ₀‖ < ε), Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)
Tactic: rcases NormedField.exists_norm_lt 𝕜 hε with ⟨ξ₀, hξ₀, hξ₀ε⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)
have this : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
Tactic: have : {ξ₀}ᶜ ∈ @nhds 𝕜 t 0 := IsOpen.mem_nhds isOpen_compl_singleton <|
      mem_compl_singleton_iff.mpr <| Ne.symm <| norm_ne_zero_iff.mp hξ₀.ne.symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)
have this₁ : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
Tactic: have : balancedCore 𝕜 {ξ₀}ᶜ ∈ @nhds 𝕜 t 0 := balancedCore_mem_nhds_zero this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) {ξ₀}ᶜ
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (balancedCore 𝕜 {ξ₀}ᶜ)
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (Metric.closedBall 0 ε)
have refine_1 : ∀ (ξ : 𝕜) (hξ : Membership.mem (γ := Set 𝕜) (balancedCore 𝕜 {ξ₀}ᶜ) ξ),
  Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ε) ξ
Tactic: refine mem_of_superset this fun ξ hξ => ?_