Theorem: PowerSeries.isExponential_map (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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ ((map φ) f).IsExponential
Tactic:
rw [isExponential_iff]
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1 ∧
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)

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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1 ∧
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Tactic:
constructor
State after:
case left
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1

case right
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)

State before:
case left
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1
Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_map,
  coeff_zero_eq_constantCoeff, hf.constantCoeff, map_one]
State after:
no goals

State before:
case right
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Tactic:
intro p q
State after:
case right
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)

State before:
case right
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Tactic:
simp only [coeff_map, ← map_mul, ← ((isExponential_iff f).mp hf).2 p q]
State after:
case right
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * φ ((coeff R (p + q)) f) = φ (↑((p + q).choose p) * (coeff R (p + q)) f)

State before:
case right
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
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * φ ((coeff R (p + q)) f) = φ (↑((p + q).choose p) * (coeff R (p + q)) f)
Tactic:
simp only [map_mul, map_natCast]
State after:
no goals