Theorem: PowerSeries.isExponential_mul (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) (f * g) =
    subst (MvPowerSeries.X 0) (f * g) * subst (MvPowerSeries.X 1) (f * g)
Tactic:
repeat
  rw [← coe_substAlgHom (substDomain_of_constantCoeff_zero (by simp))]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * (substAlgHom ⋯) (f * g)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * (substAlgHom ⋯) (f * g)
Tactic:
simp only [map_mul, coe_substAlgHom, hf.add_mul, hg.add_mul]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f *
      (subst (MvPowerSeries.X 0) g * subst (MvPowerSeries.X 1) g) =
    subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 0) g *
      (subst (MvPowerSeries.X 1) f * subst (MvPowerSeries.X 1) g)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f *
      (subst (MvPowerSeries.X 0) g * subst (MvPowerSeries.X 1) g) =
    subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 0) g *
      (subst (MvPowerSeries.X 1) f * subst (MvPowerSeries.X 1) g)
Tactic:
ring
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * subst (MvPowerSeries.X 1) (f * g)
Tactic:
rw [← coe_substAlgHom (substDomain_of_constantCoeff_zero (by simp))]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * (substAlgHom ⋯) (f * g)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 1) = 0
Tactic:
simp
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (constantCoeff R) (f * g) = 1
Tactic:
simp only [map_mul, hf.constantCoeff, hg.constantCoeff, mul_one]
State after:
no goals