awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₁
x : M₁
⊢ Eq (α := R₁ →ₗ[R₁] M₁) (↑(toSpanSingleton R₁ x) : R₁ →ₗ[R₁] M₁) (LinearMap.toSpanSingleton R₁ M₁ x)

Tactic:
rfl

Premises used: LinearMap.smulRight, LinearMap.toSpanSingleton, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
inst_9 : ContinuousSMul R₁ M₁
f : M₁ →L[R₁] M₂
x : M₁
⊢ Eq (α := R₁ →L[R₁] M₂) (f ∘SL toSpanSingleton R₁ x) (toSpanSingleton R₁ ((f : (a : M₁) → M₂) x))

Tactic:
coe_inj.mp <| LinearMap.comp_toSpanSingleton _ _

Premises used: LinearMap.comp_toSpanSingleton, ContinuousLinearMap.coe_inj, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
f : M₁ →L[R₁] R₁
g : M₂
⊢ Eq (α := M₁ →L[R₁] M₂) (toSpanSingleton R₁ g ∘SL f) (f.smulRight g)

Tactic:
rfl

Premises used: ContinuousLinearMap.smulRight, LinearMap.smulRight, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
f f' : M₂
⊢ Eq (α := R₁ →L[R₁] M₂) (toSpanSingleton R₁ f) (toSpanSingleton R₁ f') ↔ f = f'

Tactic:
simp [ContinuousLinearMap.ext_ring_iff]

Premises used: ContinuousLinearMap.ext_ring_iff
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
inst_6 : ContinuousMul R₁
x : M₂
c : R₁
⊢ Eq (α := R₁ →L[R₁] M₂) (toSpanSingleton R₁ x ∘SL toSpanSingleton R₁ c) (toSpanSingleton R₁ (c • x))

Tactic:
smulRight_comp_smulRight 1 1

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.toSpanSingleton, ContinuousLinearMap.smulRight_comp_smulRight, OfNat.ofNat, LinearMap.toSpanSingleton
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) (-x) : M₂) (-(f : (a : M) → M₂) x : M₂)

Tactic:
map_neg f x

Premises used: map_neg
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) (-x) : M₂) (-(f : (a : M) → M₂) x : M₂)

Tactic:
exact map_neg f x

Premises used: map_neg
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x y : M
⊢ (f : (a : M) → M₂) (x - y) = HSub.hSub (α := M₂) (β := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x y : M
⊢ (f : (a : M) → M₂) (x - y) = HSub.hSub (α := M₂) (β := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)

Tactic:
exact map_sub f x y

Premises used: map_sub
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
f g : M →SL[σ₁₂] M₂
x : M
⊢ ((↑f : M →ₛₗ[σ₁₂] M₂) - (↑g : M →ₛₗ[σ₁₂] M₂) : (a : M) → M₂) x =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f : M →SL[σ₁₂] M₂
x : M
⊢ Eq.{u_5 + 1} (α := M₂) ((-f : (a : M) → M₂) x : M₂) (-(f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f : M →SL[σ₁₂] M₂
⊢ (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -(↑f : M →ₛₗ[σ₁₂] M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f : M →SL[σ₁₂] M₂
⊢ Eq (α := (a : M) → M₂) (⇑(-f) : (a : M) → M₂) (-(⇑f : (a : M) → M₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f : M →SL[σ₁₂] M₂
⊢ Eq (α := M →ₜ+ M₂) (↑(-f) : M →ₜ+ M₂) (-(↑f : M →ₜ+ M₂))

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.toContinuousAddMonoidHom, ContinuousAddMonoidHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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₂)
⊢ x - x_1 = x + -x_1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_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:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
h : ∀ (x : M), Eq.{u_5 + 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
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₂
x : M
⊢ Eq.{u_5 + 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
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₂
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₂)
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f = HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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:
simp [add_smul, add_comm]

Premises used: add_comm, add_smul
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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₂)
⊢ Int.negSucc n • f = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
h : ∀ (x_1 : M), Eq.{u_5 + 1} (α := M₂) ((-x + x : (a : M) → M₂) x_1 : M₂) ((0 : (a : M) → M₂) x_1 : M₂)
⊢ -x + x = 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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_1 : M
⊢ Eq.{u_5 + 1} (α := M₂) ((-x + x : (a : M) → M₂) x_1 : M₂) ((0 : (a : M) → M₂) x_1 : M₂)

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f g : M →SL[σ₁₂] M₂
x : M
⊢ (f - g : (a : M) → M₂) x = HSub.hSub (α := M₂) (β := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f g : M →SL[σ₁₂] M₂
⊢ (↑(f - g) : M →ₛₗ[σ₁₂] M₂) = (↑f : M →ₛₗ[σ₁₂] M₂) - (↑g : M →ₛₗ[σ₁₂] M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f g : M →SL[σ₁₂] M₂
⊢ (⇑(f - g) : (a : M) → M₂) = HSub.hSub (α := (a : M) → M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
M₂ : Type u_5
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_8 : IsTopologicalAddGroup M₂
f g : M →SL[σ₁₂] M₂
⊢ (↑(f - g) : M →ₜ+ M₂) = HSub.hSub (α := M →ₜ+ M₂) (↑f : M →ₜ+ M₂) (↑g : M →ₜ+ M₂)

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.toContinuousAddMonoidHom, ContinuousAddMonoidHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
h : ∀ (x : M), Eq.{u_6 + 1} (α := M₃) ((g ∘SL (-f) : (a : M) → M₃) x : M₃) ((-g ∘SL f : (a : M) → M₃) x : M₃)
⊢ g ∘SL (-f) = -g ∘SL f

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
x : M
⊢ Eq.{u_6 + 1} (α := M₃) ((g ∘SL (-f) : (a : M) → M₃) x : M₃) ((-g ∘SL f : (a : M) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
h : ∀ (x : M), Eq.{u_6 + 1} (α := M₃) (((-g) ∘SL f : (a : M) → M₃) x : M₃) ((-g ∘SL f : (a : M) → M₃) x : M₃)
⊢ (-g) ∘SL f = -g ∘SL f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
x : M
⊢ Eq.{u_6 + 1} (α := M₃) (((-g) ∘SL f : (a : M) → M₃) x : M₃) ((-g ∘SL f : (a : M) → M₃) x : M₃)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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₃)
⊢ g ∘SL (f₁ - f₂) = g ∘SL f₁ - g ∘SL f₂

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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₃)
⊢ (g₁ - g₂) ∘SL f = g₁ ∘SL f - g₂ ∘SL f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
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₂
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:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTopologicalAddGroup M
z : ℤ
m : M
⊢ ((↑z : M →L[R] M) : (a : M) → M) m = z • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
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)
⊢ HPow.hPow (α := R →L[R] R) (β := ℕ) (toSpanSingleton R c) 0 = toSpanSingleton R (HPow.hPow (β := ℕ) c 0)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
⊢ 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:
simp