awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
rw : ((↑T⁻¹ : M₁ →L[R₁] M₁) * (↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
rw₁ : (1 : (a : M₁) → M₁) x = x
⊢ ((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x
have rw₂ : x = x
Tactic: rw [← mul_apply, Units.inv_mul, one_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x
have rw : ((↑T : M₁ →L[R₁] M₁) * (↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
Tactic: rw [← mul_apply, Units.mul_inv, one_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
rw : ((↑T : M₁ →L[R₁] M₁) * (↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
⊢ ((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x
have rw₁ : (1 : (a : M₁) → M₁) x = x
Tactic: rw [← mul_apply, Units.mul_inv, one_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
rw : ((↑T : M₁ →L[R₁] M₁) * (↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
rw₁ : (1 : (a : M₁) → M₁) x = x
⊢ ((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x
have rw₂ : x = x
Tactic: rw [← mul_apply, Units.mul_inv, one_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₁
T : M₁ →L[R₁] M₁
hT : IsUnit T
⊢ IsHomeomorph (X := M₁) (Y := M₁) (⇑T : (a : M₁) → M₁)
have obtain : ∀ (T : (M₁ →L[R₁] M₁)ˣ), IsHomeomorph (X := M₁) (Y := M₁) (⇑(↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁)
Tactic: obtain ⟨T, rfl⟩ := hT
Cleared hypotheses: T, hT
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
f : M₁ →L[R] S
⊢ Eq (α := M₁ →L[R] M₂) (f.smulRight 0) 0
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f.smulRight 0 : (a : M₁) → M₂) x : M₂) ((0 : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
x : M₂
⊢ Eq (α := M₁ →L[R] M₂) (smulRight.{u_4, u_6, u_9, u_10} (S := S) 0 x) 0
have h : ∀ (x_1 : M₁),
  Eq.{u_6 + 1} (α := M₂) ((smulRight.{u_4, u_6, u_9, u_10} (S := S) 0 x : (a : M₁) → M₂) x_1 : M₂)
    ((0 : (a : M₁) → M₂) x_1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
M₂ : Type u_6
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₁ M₁
inst_6 : Module R₁ M₂
inst_7 : TopologicalSpace R₁
inst_8 : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst_9 : AddCommMonoid M₃
inst_10 : Module R₁ M₃
inst_11 : TopologicalSpace M₃
inst_12 : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
⊢ Eq (α := M₁ →L[R₁] M₂) (f.smulRight x ∘SL g.smulRight y)
    (g.smulRight (HSMul.hSMul.{u_1, u_6, u_6} (α := R₁) ((f : (a : M₃) → R₁) y : R₁) x))
have h : ∀ (x_1 : M₁),
  Eq.{u_6 + 1} (α := M₂) ((f.smulRight x ∘SL g.smulRight y : (a : M₁) → M₂) x_1 : M₂)
    ((g.smulRight (HSMul.hSMul.{u_1, u_6, u_6} (α := R₁) ((f : (a : M₃) → R₁) y : R₁) x) : (a : M₁) → M₂) x_1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₁
inst_5 : ContinuousSMul R₁ M₁
⊢ Eq (α := R₁ →L[R₁] M₁) (toSpanSingleton R₁ 0) 0
have h : Eq.{u_4 + 1} (α := M₁) ((toSpanSingleton R₁ 0 : (a : R₁) → M₁) 1 : M₁) ((0 : (a : R₁) → M₁) 1 : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₂ : Type u_6
inst_1 : TopologicalSpace M₂
inst_2 : AddCommMonoid M₂
inst_3 : Module R₁ M₂
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ toSpanSingleton R₁ ((c : (a : R₁) → M₂) 1) = c
have h : Eq.{u_6 + 1} (α := M₂) (((toSpanSingleton R₁ ((c : (a : R₁) → M₂) 1) : R₁ →L[R₁] M₂) : (a : R₁) → M₂) 1 : M₂)
  ((c : (a : R₁) → M₂) 1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
M₄ : Type u_7
inst_9 : TopologicalSpace M₄
inst_10 : AddCommGroup M₄
inst_11 : Module R M
inst_12 : Module R₂ M₂
inst_13 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_14 : IsTopologicalAddGroup M₂
x x_1 : M →SL[σ₁₂] M₂
⊢ x - x_1 = x + -x_1
have h : ∀ (x_2 : M), Eq.{u_5 + 1} (α := M₂) ((x - x_1 : (a : M) → M₂) x_2 : M₂) ((x + -x_1 : (a : M) → M₂) x_2 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
M₄ : Type u_7
inst_9 : TopologicalSpace M₄
inst_10 : AddCommGroup M₄
inst_11 : Module R M
inst_12 : Module R₂ M₂
inst_13 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_14 : IsTopologicalAddGroup M₂
f : M →SL[σ₁₂] M₂
⊢ HSMul.hSMul (α := ℤ) 0 f = 0
have h : ∀ (x : M), Eq.{u_5 + 1} (α := M₂) ((HSMul.hSMul (α := ℤ) 0 f : (a : M) → M₂) x : M₂) ((0 : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
M₄ : Type u_7
inst_9 : TopologicalSpace M₄
inst_10 : AddCommGroup M₄
inst_11 : Module R M
inst_12 : Module R₂ M₂
inst_13 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_14 : IsTopologicalAddGroup M₂
n : ℕ
f : M →SL[σ₁₂] M₂
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f = HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f
have h : ∀ (x : M),
  Eq.{u_5 + 1} (α := M₂) ((HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f : (a : M) → M₂) x : M₂)
    ((HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
M₄ : Type u_7
inst_9 : TopologicalSpace M₄
inst_10 : AddCommGroup M₄
inst_11 : Module R M
inst_12 : Module R₂ M₂
inst_13 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_14 : IsTopologicalAddGroup M₂
n : ℕ
f : M →SL[σ₁₂] M₂
⊢ Int.negSucc n • f = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f
have h : ∀ (x : M),
  Eq.{u_5 + 1} (α := M₂) ((Int.negSucc n • f : (a : M) → M₂) x : M₂)
    ((-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
M₄ : Type u_7
inst_9 : TopologicalSpace M₄
inst_10 : AddCommGroup M₄
inst_11 : Module R M
inst_12 : Module R₂ M₂
inst_13 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_14 : IsTopologicalAddGroup M₂
x : M →SL[σ₁₂] M₂
⊢ -x + x = 0
have h : ∀ (x_1 : M), Eq.{u_5 + 1} (α := M₂) ((-x + x : (a : M) → M₂) x_1 : M₂) ((0 : (a : M) → M₂) x_1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
inst_9 : Module R M
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : IsTopologicalAddGroup M₂
inst_14 : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ g ∘SL (-f) = -g ∘SL f
have h : ∀ (x : M), Eq.{u_6 + 1} (α := M₃) ((g ∘SL (-f) : (a : M) → M₃) x : M₃) ((-g ∘SL f : (a : M) → M₃) x : M₃)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
inst_9 : Module R M
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (-g) ∘SL f = -g ∘SL f
have h : ∀ (x : M), Eq.{u_6 + 1} (α := M₃) (((-g) ∘SL f : (a : M) → M₃) x : M₃) ((-g ∘SL f : (a : M) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
inst_9 : Module R M
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : IsTopologicalAddGroup M₂
inst_14 : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
⊢ g ∘SL (f₁ - f₂) = g ∘SL f₁ - g ∘SL f₂
have h : ∀ (x : M),
  Eq.{u_6 + 1} (α := M₃) ((g ∘SL (f₁ - f₂) : (a : M) → M₃) x : M₃) ((g ∘SL f₁ - g ∘SL f₂ : (a : M) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
R₃ : Type u_3
inst_2 : Ring R₃
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup M
M₂ : Type u_5
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
M₃ : Type u_6
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
inst_9 : Module R M
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (g₁ - g₂) ∘SL f = g₁ ∘SL f - g₂ ∘SL f
have h : ∀ (x : M),
  Eq.{u_6 + 1} (α := M₃) (((g₁ - g₂) ∘SL f : (a : M) → M₃) x : M₃) ((g₁ ∘SL f - g₂ ∘SL f : (a : M) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
⊢ HPow.hPow (α := R →L[R] R) (β := ℕ) (toSpanSingleton R c) 0 = toSpanSingleton R (HPow.hPow (β := ℕ) c 0)
have zero : Eq (α := R) ((HPow.hPow (α := R →L[R] R) (β := ℕ) (toSpanSingleton R c) 0 : (a : R) → R) 1 : R)
  ((toSpanSingleton R (HPow.hPow (β := ℕ) c 0) : (a : R) → R) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
have succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
Tactic: rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
have succ₁ : HMul.hMul (α := R →L[R] R) (toSpanSingleton R (c ^ n)) (toSpanSingleton R c) = toSpanSingleton R (c ^ (n + 1))
Tactic: rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
succ₁ : HMul.hMul (α := R →L[R] R) (toSpanSingleton R (c ^ n)) (toSpanSingleton R c) = toSpanSingleton R (c ^ (n + 1))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
have succ₂ : Eq (α := R →L[R] R) (toSpanSingleton R (c ^ n) ∘SL toSpanSingleton R c) (toSpanSingleton R (c ^ (n + 1)))
Tactic: rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
succ₁ : HMul.hMul (α := R →L[R] R) (toSpanSingleton R (c ^ n)) (toSpanSingleton R c) = toSpanSingleton R (c ^ (n + 1))
succ₂ : Eq (α := R →L[R] R) (toSpanSingleton R (c ^ n) ∘SL toSpanSingleton R c) (toSpanSingleton R (c ^ (n + 1)))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
have succ₃ : Eq (α := R →L[R] R) (toSpanSingleton R (c • c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
Tactic: rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
succ₁ : HMul.hMul (α := R →L[R] R) (toSpanSingleton R (c ^ n)) (toSpanSingleton R c) = toSpanSingleton R (c ^ (n + 1))
succ₂ : Eq (α := R →L[R] R) (toSpanSingleton R (c ^ n) ∘SL toSpanSingleton R c) (toSpanSingleton R (c ^ (n + 1)))
succ₃ : Eq (α := R →L[R] R) (toSpanSingleton R (c • c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
have succ₄ : Eq (α := R →L[R] R) (toSpanSingleton R (c * c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
Tactic: rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
succ₁ : HMul.hMul (α := R →L[R] R) (toSpanSingleton R (c ^ n)) (toSpanSingleton R c) = toSpanSingleton R (c ^ (n + 1))
succ₂ : Eq (α := R →L[R] R) (toSpanSingleton R (c ^ n) ∘SL toSpanSingleton R c) (toSpanSingleton R (c ^ (n + 1)))
succ₃ : Eq (α := R →L[R] R) (toSpanSingleton R (c • c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
succ₄ : Eq (α := R →L[R] R) (toSpanSingleton R (c * c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
have succ₅ : Eq (α := R →L[R] R) (toSpanSingleton R (c * c ^ n)) (toSpanSingleton R (c * c ^ n))
Tactic: rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
have zero : HPow.hPow (α := R →L[R] R) (β := ℕ) (toSpanSingleton R c) 0 = toSpanSingleton R (HPow.hPow (β := ℕ) c 0)
Tactic: induction n with
  | zero => ext; simp
  | succ n ihn =>
    rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
zero : HPow.hPow (α := R →L[R] R) (β := ℕ) (toSpanSingleton R c) 0 = toSpanSingleton R (HPow.hPow (β := ℕ) c 0)
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
have succ : ∀ (n : ℕ) (ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)),
  HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
Tactic: induction n with
  | zero => ext; simp
  | succ n ihn =>
    rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
S : Type u_4
inst : Semiring R
inst_1 : Monoid S
M : Type u_6
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
N₂ : Type u_9
inst_5 : TopologicalSpace N₂
inst_6 : AddCommMonoid N₂
inst_7 : Module R N₂
N₃ : Type u_10
inst_8 : TopologicalSpace N₃
inst_9 : AddCommMonoid N₃
inst_10 : Module R N₃
inst_11 : DistribMulAction S N₃
inst_12 : SMulCommClass R S N₃
inst_13 : ContinuousConstSMul S N₃
inst_14 : DistribMulAction S N₂
inst_15 : ContinuousConstSMul S N₂
inst_16 : SMulCommClass R S N₂
inst_17 : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
⊢ hₗ ∘SL (c • fₗ) = c • hₗ ∘SL fₗ
have h : ∀ (x : M), Eq.{u_10 + 1} (α := N₃) ((hₗ ∘SL (c • fₗ) : (a : M) → N₃) x : N₃) ((c • hₗ ∘SL fₗ : (a : M) → N₃) x : N₃)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (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₃
M : Type u_6
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
M₂ : Type u_7
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
M₃ : Type u_8
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : SMulCommClass R₂ R₂ M₂
inst_14 : SMulCommClass R₃ R₃ M₃
inst_15 : ContinuousConstSMul R₂ M₂
inst_16 : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
⊢ h ∘SL (c • f) = HSMul.hSMul (α := R₃) ((σ₂₃ : (a : R₂) → R₃) c : R₃) (h ∘SL f)
have h₁ : ∀ (x : M),
  Eq.{u_8 + 1} (α := M₃) ((h ∘SL (c • f) : (a : M) → M₃) x : M₃)
    ((HSMul.hSMul (α := R₃) ((σ₂₃ : (a : R₂) → R₃) c : R₃) (h ∘SL f) : (a : M) → M₃) x : M₃)
Tactic: ext x