Theorem: MvPowerSeries.substDomain_mul (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
b a : σ → MvPowerSeries τ S
ha : SubstDomain a
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff τ S) ((b * a) s))
Tactic:
simp only [Pi.mul_apply, map_mul]
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
b a : σ → MvPowerSeries τ S
ha : SubstDomain a
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (b s) * (constantCoeff τ S) (a 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
b a : σ → MvPowerSeries τ S
ha : SubstDomain a
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (b s) * (constantCoeff τ S) (a s))
Tactic:
exact Commute.isNilpotent_mul_right (Commute.all _ _) (ha.const_coeff _)
State after:
no goals