Theorem: PowerSeries.substDomain_smul_X (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
A : Type u_1
inst✝⁷ : CommRing A
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_3
inst✝⁴ : DecidableEq τ
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : A
⊢ (MvPowerSeries.constantCoeff Unit R) (a • X) = 0
Tactic:
change constantCoeff R (a • X) = 0
State after:
A : Type u_1
inst✝⁷ : CommRing A
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_3
inst✝⁴ : DecidableEq τ
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : A
⊢ (constantCoeff R) (a • X) = 0

State before:
A : Type u_1
inst✝⁷ : CommRing A
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_3
inst✝⁴ : DecidableEq τ
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : A
⊢ (constantCoeff R) (a • X) = 0
Tactic:
rw [← coeff_zero_eq_constantCoeff]
State after:
A : Type u_1
inst✝⁷ : CommRing A
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_3
inst✝⁴ : DecidableEq τ
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : A
⊢ (coeff R 0) (a • X) = 0

State before:
A : Type u_1
inst✝⁷ : CommRing A
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_3
inst✝⁴ : DecidableEq τ
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : A
⊢ (coeff R 0) (a • X) = 0
Tactic:
simp only [LinearMap.map_smul_of_tower, coeff_zero_X, smul_zero]
State after:
no goals