Theorem: MvPowerSeries.substDomain_add (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
s : σ
⊢ IsNilpotent ((constantCoeff τ S) ((a + b) s))
Tactic:
simp only [Pi.add_apply, map_add]
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (a s) + (constantCoeff τ S) (b s))

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (a s) + (constantCoeff τ S) (b s))
Tactic:
exact IsNilpotent.add (ha.const_coeff s) (hb.const_coeff s)
State after:
no goals

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
⊢ Filter.Tendsto (a + b) Filter.cofinite (nhds 0)
Tactic:
letI : UniformSpace S := ⊥
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ Filter.Tendsto (a + b) Filter.cofinite (nhds 0)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ Filter.Tendsto (a + b) Filter.cofinite (nhds 0)
Tactic:
convert Filter.Tendsto.add (ha.tendsto_zero) (hb.tendsto_zero)
State after:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ 0 = 0 + 0

State before:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ 0 = 0 + 0
Tactic:
rw [add_zero]
State after:
no goals