awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
pos :
  ∀ (h : i ∈ I),
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
          (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
        a
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
have neg : i ∉ I →
  Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a
Tactic: split_ifs <;> [apply continuous_apply; exact continuous_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
M₄ : Type u_7
inst_17 : TopologicalSpace M₄
inst_18 : AddCommMonoid M₄
inst_19 : Module R₁ M₁
inst_20 : Module R₂ M₂
inst_21 : Module R₃ M₃
f g : M₁ ≃SL[σ₁₂] M₂
h₁ : (↑(↑f : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun = (↑(↑g : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun
h₂ : (↑f : M₁ ≃ₛₗ[σ₁₂] M₂).invFun = (↑g : M₁ ≃ₛₗ[σ₁₂] M₂).invFun
⊢ f = g
have obtain : ∀ (f' : M₁ ≃ₛₗ[σ₁₂] M₂) (continuous_toFun : Continuous[inst_11, inst_13] (↑f' : M₁ →ₛₗ[σ₁₂] M₂).toFun)
  (continuous_invFun : Continuous[inst_13, inst_11] f'.invFun)
  (h₁ :
    (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                  M₁ ≃SL[σ₁₂] M₂ } :
              M₁ ≃ₛₗ[σ₁₂] M₂) :
          M₁ →ₛₗ[σ₁₂] M₂).toFun =
      (↑(↑g : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun)
  (h₂ :
    (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
              M₁ ≃SL[σ₁₂] M₂ } :
          M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
      (↑g : M₁ ≃ₛₗ[σ₁₂] M₂).invFun),
  { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
      M₁ ≃SL[σ₁₂] M₂ } =
    g
Tactic: obtain ⟨f', _⟩ := f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
M₄ : Type u_7
inst_17 : TopologicalSpace M₄
inst_18 : AddCommMonoid M₄
inst_19 : Module R₁ M₁
inst_20 : Module R₂ M₂
inst_21 : Module R₃ M₃
g : M₁ ≃SL[σ₁₂] M₂
f' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun : Continuous[inst_11, inst_13] (↑f' : M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun : Continuous[inst_13, inst_11] f'.invFun
h₁ :
  (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂) :
        M₁ →ₛₗ[σ₁₂] M₂).toFun =
    (↑(↑g : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun
h₂ :
  (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            M₁ ≃SL[σ₁₂] M₂ } :
        M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
    (↑g : M₁ ≃ₛₗ[σ₁₂] M₂).invFun
⊢ { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
      M₁ ≃SL[σ₁₂] M₂ } =
    g
have obtain : ∀ (g' : M₁ ≃ₛₗ[σ₁₂] M₂) (continuous_toFun_1 : Continuous[inst_11, inst_13] (↑g' : M₁ →ₛₗ[σ₁₂] M₂).toFun)
  (continuous_invFun_1 : Continuous[inst_13, inst_11] g'.invFun)
  (h₁ :
    (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                  M₁ ≃SL[σ₁₂] M₂ } :
              M₁ ≃ₛₗ[σ₁₂] M₂) :
          M₁ →ₛₗ[σ₁₂] M₂).toFun =
      (↑(↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
                  M₁ ≃SL[σ₁₂] M₂ } :
              M₁ ≃ₛₗ[σ₁₂] M₂) :
          M₁ →ₛₗ[σ₁₂] M₂).toFun)
  (h₂ :
    (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
              M₁ ≃SL[σ₁₂] M₂ } :
          M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
      (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
              M₁ ≃SL[σ₁₂] M₂ } :
          M₁ ≃ₛₗ[σ₁₂] M₂).invFun),
  { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
      M₁ ≃SL[σ₁₂] M₂ } =
    { toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
Tactic: obtain ⟨g', _⟩ := g
Cleared hypotheses: g, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) 1 : M₁) ((g : (a : R₁) → M₁) 1 : M₁)
x : R₁
⊢ Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (x * 1) : M₁) ((g : (a : R₁) → M₁) (x * 1) : M₁)
have rw : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
  ((g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
Tactic: rw [← smul_eq_mul, map_smul, h, map_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) 1 : M₁) ((g : (a : R₁) → M₁) 1 : M₁)
x : R₁
rw :
  Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
    ((g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
⊢ Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (x * 1) : M₁) ((g : (a : R₁) → M₁) (x * 1) : M₁)
have rw₁ : HSMul.hSMul (β := M₁) x ((f : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
Tactic: rw [← smul_eq_mul, map_smul, h, map_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) 1 : M₁) ((g : (a : R₁) → M₁) 1 : M₁)
x : R₁
rw :
  Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
    ((g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
rw₁ : HSMul.hSMul (β := M₁) x ((f : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
⊢ Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (x * 1) : M₁) ((g : (a : R₁) → M₁) (x * 1) : M₁)
have rw₂ : HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
Tactic: rw [← smul_eq_mul, map_smul, h, map_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) 1 : M₁) ((g : (a : R₁) → M₁) 1 : M₁)
x : R₁
rw :
  Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
    ((g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
rw₁ : HSMul.hSMul (β := M₁) x ((f : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
rw₂ : HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
⊢ Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (x * 1) : M₁) ((g : (a : R₁) → M₁) (x * 1) : M₁)
have rw₃ : HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁) = HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁)
Tactic: rw [← smul_eq_mul, map_smul, h, map_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
inst_17 : Module R₁ M₁
inst_18 : Module R₂ M₂
inst_19 : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
⊢ Eq (α := M₁ ≃ₛₗ[σ₁₃] M₃) (↑(e₁.trans e₂) : M₁ ≃ₛₗ[σ₁₃] M₃) ((↑e₁ : M₁ ≃ₛₗ[σ₁₂] M₂).trans (↑e₂ : M₂ ≃ₛₗ[σ₂₃] M₃))
have h : ∀ (x : M₁),
  Eq.{u_6 + 1} (α := M₃) (((↑(e₁.trans e₂) : M₁ ≃ₛₗ[σ₁₃] M₃) : (a : M₁) → M₃) x : M₃)
    (((↑e₁ : M₁ ≃ₛₗ[σ₁₂] M₂).trans (↑e₂ : 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
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ Eq.{u_4 + 1} (α := M₁ → M₁)
    (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := M₂) (⇑e.symm : (a : M₂) → M₁) (⇑e : (a : M₁) → M₂)) id
have h : ∀ (x : M₁), Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := M₂) (⇑e.symm : (a : M₂) → M₁) (⇑e : (a : M₁) → M₂) x = id x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ Eq.{u_5 + 1} (α := M₂ → M₂)
    (Function.comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M₁) (⇑e : (a : M₁) → M₂) (⇑e.symm : (a : M₂) → M₁)) id
have h : ∀ (x : M₂), Function.comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M₁) (⇑e : (a : M₁) → M₂) (⇑e.symm : (a : M₂) → M₁) x = id x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ Eq.{u_4 + 1} (α := Set M₁) ((⇑e.symm : (a : M₂) → M₁) '' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
have rw : Eq.{u_4 + 1} (α := Set M₁) ((⇑e.symm.symm : (a : M₁) → M₂) ⁻¹' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
Tactic: rw [e.symm.image_eq_preimage_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
rw : Eq.{u_4 + 1} (α := Set M₁) ((⇑e.symm.symm : (a : M₁) → M₂) ⁻¹' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
⊢ Eq.{u_4 + 1} (α := Set M₁) ((⇑e.symm : (a : M₂) → M₁) '' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
have rw₁ : Eq.{u_4 + 1} (α := Set M₁) ((⇑e : (a : M₁) → M₂) ⁻¹' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
Tactic: rw [e.symm.image_eq_preimage_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ (f.inv * (↑f : M →L[R] M) : (a : M) → M) x = x
have rw : (1 : (a : M) → M) x = x
Tactic: rw [f.inv_val]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ ((↑f : M →L[R] M) * f.inv : (a : M) → M) x = x
have rw : (1 : (a : M) → M) x = x
Tactic: rw [f.val_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : M ≃L[R] M
⊢ (↑f : M →L[R] M) * (↑f.symm : M →L[R] M) = 1
have h : ∀ (x : M), Eq (α := M) (((↑f : M →L[R] M) * (↑f.symm : M →L[R] M) : (a : M) → M) x : M) ((1 : (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
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : M ≃L[R] M
⊢ (↑f.symm : M →L[R] M) * (↑f : M →L[R] M) = 1
have h : ∀ (x : M), Eq (α := M) (((↑f.symm : M →L[R] M) * (↑f : M →L[R] M) : (a : M) → M) x : M) ((1 : (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
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
x y : (M →L[R] M)ˣ
⊢ ofUnit (x * y) = ofUnit x * ofUnit y
have h : ∀ (x_1 : M), Eq (α := M) ((ofUnit (x * y) : (a : M) → M) x_1 : M) ((ofUnit x * ofUnit y : (a : M) → M) x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
⊢ HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
have rw : HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
⊢ HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
have rw₁ : Eq (α := R) ((e.symm : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) 1) : R) (1 : R)
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e.symm : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) 1) : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
have rw₂ : Eq (α := R) ((e.symm : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e.symm : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) 1) : R) (1 : R)
rw₂ : Eq (α := R) ((e.symm : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
have rw₃ : Eq (α := R) ((e.symm : (a : R) → R) ((e : (a : R) → R) 1 : R) : R) (1 : R)
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e.symm : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) 1) : R) (1 : R)
rw₂ : Eq (α := R) ((e.symm : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
rw₃ : Eq (α := R) ((e.symm : (a : R) → R) ((e : (a : R) → R) 1 : R) : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
have rw₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
⊢ HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
have rw : HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
⊢ HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
have rw₁ : Eq (α := R) ((e : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) 1) : R) (1 : R)
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) 1) : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
have rw₂ : Eq (α := R) ((e : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) 1) : R) (1 : R)
rw₂ : Eq (α := R) ((e : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
have rw₃ : Eq (α := R) ((e : (a : R) → R) ((e.symm : (a : R) → R) 1 : R) : R) (1 : R)
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) 1) : R) (1 : R)
rw₂ : Eq (α := R) ((e : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
rw₃ : Eq (α := R) ((e : (a : R) → R) ((e.symm : (a : R) → R) 1 : R) : R) (1 : R)
⊢ HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
have rw₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]
-- 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₂
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0 ↔ Subsingleton M ∧ Subsingleton M₂
have 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₂
Tactic: refine ⟨fun ⟨e, 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₂
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₂
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0 ↔ Subsingleton M ∧ Subsingleton M₂
have refine_2 : Subsingleton M ∧ Subsingleton M₂ → IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
Tactic: refine ⟨fun ⟨e, 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₂
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
have refine : ∀ (x y : M), Eq.{u_3 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) y : M₂)
Tactic: refine ⟨fun x y ↦ e.injective ?_⟩
-- 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₂
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 ∧ Subsingleton M₂
have A : Subsingleton M
Tactic: have A : Subsingleton M := by
      refine ⟨fun x y ↦ e.injective ?_⟩
      simp [he, ← ContinuousLinearEquiv.coe_coe]