Theorem: PowerSeries.isExponential_one (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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) 1 = subst (MvPowerSeries.X 0) 1 * subst (MvPowerSeries.X 1) 1
Tactic:
rw [← Polynomial.coe_one]
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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) ↑1 = subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1

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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) ↑1 = subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1
Tactic:
rw [subst_coe (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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1

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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1
Tactic:
rw [subst_coe (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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * subst (MvPowerSeries.X 1) ↑1

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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * subst (MvPowerSeries.X 1) ↑1
Tactic:
rw [subst_coe (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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * (Polynomial.aeval (MvPowerSeries.X 1)) 1

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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * (Polynomial.aeval (MvPowerSeries.X 1)) 1
Tactic:
simp only [map_one, mul_one]
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
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0 + 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
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0) = 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
⊢ (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
⊢ (constantCoeff R) 1 = 1
Tactic:
simp only [map_one]
State after:
no goals