mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 + p.2
⊢ (fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p ↦ p.1 + p.2

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 + p.2
x✝ : A × A
⊢ ((fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ) x✝ = (⇑φ ∘ fun p ↦ p.1 + p.2) x✝
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S✝
inst✝⁹ : Ring R
inst✝⁸ : Ring S✝
A : Type u_3
inst✝⁷ : AddCommGroup A
inst✝⁶ : Module R A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
⊢ IsModuleTopology R (A ⧸ S)

Tactic:
constructor

Goal state after:
R : Type u_1
S✝ : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S✝
inst✝⁹ : Ring R
inst✝⁸ : Ring S✝
A : Type u_3
inst✝⁷ : AddCommGroup A
inst✝⁶ : Module R A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
⊢ IsModuleTopology R (M × N)

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
⊢ instTopologicalSpaceProd = moduleTopology R (M × N)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ (fun ab ↦ (bil ab.1) ab.2) = (fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
x✝ : A × B
⊢ (bil x✝.1) x✝.2 = ((fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe ↔ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

Tactic:
constructor

Goal state after:
case mp
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
⊢ g ∘SL 0 = 0

Tactic:
ext

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x✝ : M₁
⊢ (g ∘SL 0) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
⊢ 0 ∘SL f = 0

Tactic:
ext

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (0 ∘SL f) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
⊢ g ∘SL (f₁ + f₂) = g ∘SL f₁ + g ∘SL f₂

Tactic:
ext

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g ∘SL (f₁ + f₂)) x✝ = (g ∘SL f₁ + g ∘SL f₂) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (g₁ + g₂) ∘SL f = g₁ ∘SL f + g₂ ∘SL f

Tactic:
ext

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((g₁ + g₂) ∘SL f) x✝ = (g₁ ∘SL f + g₂ ∘SL f) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
⊢ g ∘SL ∑ i ∈ s, f i = ∑ i ∈ s, g ∘SL f i

Tactic:
ext

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g ∘SL ∑ i ∈ s, f i) x✝ = (∑ i ∈ s, g ∘SL f i) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝ : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (∑ i ∈ s, g i) ∘SL f = ∑ i ∈ s, g i ∘SL f

Tactic:
ext

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝ : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((∑ i ∈ s, g i) ∘SL f) x✝ = (∑ i ∈ s, g i ∘SL f) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
f : M₁ →L[R] S
⊢ f.smulRight 0 = 0

Tactic:
ext

Goal state after:
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
f : M₁ →L[R] S
x✝ : M₁
⊢ (f.smulRight 0) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
x : M₂
⊢ smulRight 0 x = 0

Tactic:
ext

Goal state after:
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
x : M₂
x✝ : M₁
⊢ (smulRight 0 x) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝¹² : Semiring R₁
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₁ M₁
inst✝⁶ : Module R₁ M₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₃
inst✝¹ : TopologicalSpace M₃
inst✝ : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
⊢ f.smulRight x ∘SL g.smulRight y = g.smulRight (f y • x)

Tactic:
ext

Goal state after:
R₁ : Type u_1
inst✝¹² : Semiring R₁
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₁ M₁
inst✝⁶ : Module R₁ M₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₃
inst✝¹ : TopologicalSpace M₃
inst✝ : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
x✝ : M₁
⊢ (f.smulRight x ∘SL g.smulRight y) x✝ = (g.smulRight (f y • x)) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₁ : Type u_4
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₁
⊢ toSpanSingleton R₁ 0 = 0

Tactic:
ext

Goal state after:
R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₁ : Type u_4
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₁
⊢ (toSpanSingleton R₁ 0) 1 = 0 1
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ toSpanSingleton R₁ (c 1) = c

Tactic:
ext

Goal state after:
R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ (toSpanSingleton R₁ (c 1)) 1 = c 1
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (-g) ∘SL f = -g ∘SL f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((-g) ∘SL f) x✝ = (-g ∘SL f) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
⊢ g ∘SL (f₁ - f₂) = g ∘SL f₁ - g ∘SL f₂

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
x✝ : M
⊢ (g ∘SL (f₁ - f₂)) x✝ = (g ∘SL f₁ - g ∘SL f₂) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (g₁ - g₂) ∘SL f = g₁ ∘SL f - g₂ ∘SL f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((g₁ - g₂) ∘SL f) x✝ = (g₁ ∘SL f - g₂ ∘SL f) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ toSpanSingleton R c ^ 0 = toSpanSingleton R (c ^ 0)

Tactic:
ext

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ (toSpanSingleton R c ^ 0) 1 = (toSpanSingleton R (c ^ 0)) 1
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝¹ x✝ : U →L[R] V
⊢ lcomp W (x✝¹ + x✝) = lcomp W x✝¹ + lcomp W x✝

Tactic:
ext

Goal state after:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝³ x✝² : U →L[R] V
x✝¹ : V →L[R] W
x✝ : U
⊢ ((lcomp W (x✝³ + x✝²)) x✝¹) x✝ = ((lcomp W x✝³ + lcomp W x✝²) x✝¹) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝¹ : R
x✝ : U →L[R] V
⊢ lcomp W (x✝¹ • x✝) = (RingHom.id R) x✝¹ • lcomp W x✝

Tactic:
ext

Goal state after:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝³ : R
x✝² : U →L[R] V
x✝¹ : V →L[R] W
x✝ : U
⊢ ((lcomp W (x✝³ • x✝²)) x✝¹) x✝ = (((RingHom.id R) x✝³ • lcomp W x✝²) x✝¹) x✝