awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((HSMul.hSMul (α := ℕ) 0 f : (a : M₁) → M₂) x : M₂) ((0 : (a : M₁) → M₂) x : M₂)
⊢ HSMul.hSMul (α := ℕ) 0 f = 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((HSMul.hSMul (α := ℕ) 0 f : (a : M₁) → M₂) x : M₂) ((0 : (a : M₁) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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 : ContinuousAdd M₂
n : ℕ
f : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) (((n + 1) • f : (a : M₁) → M₂) x : M₂) ((n • f + f : (a : M₁) → M₂) x : M₂)
⊢ (n + 1) • f = n • f + f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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 : ContinuousAdd M₂
n : ℕ
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) (((n + 1) • f : (a : M₁) → M₂) x : M₂) ((n • f + f : (a : M₁) → M₂) x : M₂)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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 : ContinuousAdd M₂
a b : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((a + b : (a : M₁) → M₂) x : M₂) ((b + a : (a : M₁) → M₂) x : M₂)
⊢ a + b = b + a

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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 : ContinuousAdd M₂
a b : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((a + b : (a : M₁) → M₂) x : M₂) ((b + a : (a : M₁) → M₂) x : M₂)

Tactic:
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]

Premises used: add_assoc, zero_add, add_comm, neg_add_cancel, add_zero
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
ι : Type u_9
t : Finset ι
f : ι → M₁ →SL[σ₁₂] M₂
⊢ Eq (α := M₁ →ₛₗ[σ₁₂] M₂) (↑(∑ d ∈ t, f d) : M₁ →ₛₗ[σ₁₂] M₂) (∑ d ∈ t, (↑(f d) : M₁ →ₛₗ[σ₁₂] M₂))

Tactic:
map_sum (AddMonoidHom.mk ⟨((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂), rfl⟩ fun _ _ => rfl) _ _

Premises used: AddMonoidHom.mk, ContinuousLinearMap.toLinearMap, map_sum, ZeroHom.mk, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
ι : Type u_9
t : Finset ι
f : ι → M₁ →SL[σ₁₂] M₂
⊢ Eq (α := (a : M₁) → M₂) (⇑(∑ d ∈ t, f d) : (a : M₁) → M₂) (∑ d ∈ t, (⇑(f d) : (a : M₁) → M₂))

Tactic:
simp only [← coe_coe, coe_sum, LinearMap.coe_sum]

Premises used: ContinuousLinearMap.coe_coe, LinearMap.coe_sum, ContinuousLinearMap.coe_sum
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
ι : Type u_9
t : Finset ι
f : ι → M₁ →SL[σ₁₂] M₂
b : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((∑ d ∈ t, f d : (a : M₁) → M₂) b : M₂) (∑ d ∈ t, (f d : (a : M₁) → M₂) b : M₂)

Tactic:
simp only [coe_sum', Finset.sum_apply]

Premises used: Finset.sum_apply, ContinuousLinearMap.coe_sum'
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
h : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (↑(h ∘SL f) : M₁ →ₛₗ[σ₁₃] M₃) = (↑h : M₂ →ₛₗ[σ₂₃] M₃) ∘ₛₗ (↑f : M₁ →ₛₗ[σ₁₂] M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
h : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := (a : M₁) → M₃) (⇑(h ∘SL f) : (a : M₁) → M₃)
    (Function.comp.{u_4 + 1, u_6 + 1, u_7 + 1} (β := M₂) (⇑h : (a : M₂) → M₃) (⇑f : (a : M₁) → M₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
h : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := M₁ →ₜ+ M₃) (↑(h ∘SL f) : M₁ →ₜ+ M₃) (ContinuousAddMonoidHom.comp (↑h : M₂ →ₜ+ M₃) (↑f : M₁ →ₜ+ M₂))

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) ((g ∘SL f : (a : M₁) → M₃) x : M₃) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x : M₂) : M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ f ∘SL ContinuousLinearMap.id R₁ M₁ = f

Tactic:
ext fun _x => rfl

Premises used: ContinuousLinearMap.ext, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ ContinuousLinearMap.id R₂ M₂ ∘SL f = f

Tactic:
ext fun _x => rfl

Premises used: ContinuousLinearMap.ext, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_9
E : Type u_10
F : Type u_11
inst : Semiring R
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
g : F →L[R] E
hinv : g ∘SL f = ContinuousLinearMap.id R E
⊢ Function.LeftInverse.{u_10 + 1, u_11 + 1} (α := E) (β := F) (⇑g : (a : F) → E) (⇑f : (a : E) → F)

Tactic:
simpa [← Function.rightInverse_iff_comp] using congr(⇑$hinv)

Premises used: Function.rightInverse_iff_comp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_9
E : Type u_10
F : Type u_11
inst : Semiring R
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
g : F →L[R] E
hinv : f ∘SL g = ContinuousLinearMap.id R F
⊢ Function.RightInverse.{u_10 + 1, u_11 + 1} (α := E) (β := F) (⇑g : (a : F) → E) (⇑f : (a : E) → F)

Tactic:
leftInverse_of_comp hinv

Premises used: ContinuousLinearMap.leftInverse_of_comp, Function.RightInverse
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
h : ∀ (x : M₁), Eq.{u_7 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M₁) → M₃) x : M₃) ((0 : (a : M₁) → M₃) x : M₃)
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (g.comp (σ₁₂ := σ₁₂) 0) 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M₁) → M₃) x : M₃) ((0 : (a : M₁) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_7 + 1} (α := M₃) ((comp (σ₂₃ := σ₂₃) 0 f : (a : M₁) → M₃) x : M₃) ((0 : (a : M₁) → M₃) x : M₃)
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (comp (σ₂₃ := σ₂₃) 0 f) 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) ((comp (σ₂₃ := σ₂₃) 0 f : (a : M₁) → M₃) x : M₃) ((0 : (a : M₁) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : ContinuousAdd M₂
inst_14 : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
h :
  ∀ (x : M₁),
    Eq.{u_7 + 1} (α := M₃) ((g ∘SL (f₁ + f₂) : (a : M₁) → M₃) x : M₃) ((g ∘SL f₁ + g ∘SL f₂ : (a : M₁) → M₃) x : M₃)
⊢ g ∘SL (f₁ + f₂) = g ∘SL f₁ + g ∘SL f₂

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : ContinuousAdd M₂
inst_14 : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) ((g ∘SL (f₁ + f₂) : (a : M₁) → M₃) x : M₃) ((g ∘SL f₁ + g ∘SL f₂ : (a : M₁) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
h :
  ∀ (x : M₁),
    Eq.{u_7 + 1} (α := M₃) (((g₁ + g₂) ∘SL f : (a : M₁) → M₃) x : M₃) ((g₁ ∘SL f + g₂ ∘SL f : (a : M₁) → M₃) x : M₃)
⊢ (g₁ + g₂) ∘SL f = g₁ ∘SL f + g₂ ∘SL f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) (((g₁ + g₂) ∘SL f : (a : M₁) → M₃) x : M₃) ((g₁ ∘SL f + g₂ ∘SL f : (a : M₁) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst_13 : ContinuousAdd M₂
inst_14 : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
h :
  ∀ (x : M₁),
    Eq.{u_7 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) (∑ i ∈ s, f i) : (a : M₁) → M₃) x : M₃)
      ((∑ i ∈ s, g ∘SL f i : (a : M₁) → M₃) x : M₃)
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (g.comp (σ₁₂ := σ₁₂) (∑ i ∈ s, f i)) (∑ i ∈ s, g ∘SL f i)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst_13 : ContinuousAdd M₂
inst_14 : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) (∑ i ∈ s, f i) : (a : M₁) → M₃) x : M₃)
    ((∑ i ∈ s, g ∘SL f i : (a : M₁) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst_13 : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
h :
  ∀ (x : M₁),
    Eq.{u_7 + 1} (α := M₃) ((comp (σ₂₃ := σ₂₃) (∑ i ∈ s, g i) f : (a : M₁) → M₃) x : M₃)
      ((∑ i ∈ s, g i ∘SL f : (a : M₁) → M₃) x : M₃)
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (comp (σ₂₃ := σ₂₃) (∑ i ∈ s, g i) f) (∑ i ∈ s, g i ∘SL f)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst_13 : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_7 + 1} (α := M₃) ((comp (σ₂₃ := σ₂₃) (∑ i ∈ s, g i) f : (a : M₁) → M₃) x : M₃)
    ((∑ i ∈ s, g i ∘SL f : (a : M₁) → M₃) x : M₃)

Tactic:
simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply]

Premises used: ContinuousLinearMap.coe_comp', Finset.sum_apply, ContinuousLinearMap.coe_sum', Function.comp_apply
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
M₄ : Type u_8
inst_9 : TopologicalSpace M₄
inst_10 : AddCommMonoid M₄
inst_11 : Module R₁ M₁
inst_12 : Module R₂ M₂
inst_13 : Module R₃ M₃
inst_14 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
R₄ : Type u_9
inst_15 : Semiring R₄
inst_16 : Module R₄ M₄
σ₁₄ : R₁ →+* R₄
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
inst_17 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_18 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_19 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
h : M₃ →SL[σ₃₄] M₄
g : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (h ∘SL g) ∘SL f = h ∘SL g ∘SL f

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑g : (a : M₂) → M₃)
h : g ∘SL f₁ = g ∘SL f₂
h₁ : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f₁ : (a : M₁) → M₂) x : M₂) ((f₂ : (a : M₁) → M₂) x : M₂)
⊢ f₁ = f₂

Tactic:
ext x