Theorem: DividedPowers.add_dpowExp (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ hI.dpowExp (a + b) = hI.dpowExp a * hI.dpowExp b
Tactic:
ext n
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
a b : A
ha : a ∈ I
hb : b ∈ I
n : ℕ
⊢ (PowerSeries.coeff A n) (hI.dpowExp (a + b)) = (PowerSeries.coeff A n) (hI.dpowExp a * hI.dpowExp b)

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
a b : A
ha : a ∈ I
hb : b ∈ I
n : ℕ
⊢ (PowerSeries.coeff A n) (hI.dpowExp (a + b)) = (PowerSeries.coeff A n) (hI.dpowExp a * hI.dpowExp b)
Tactic:
simp only [dpowExp, PowerSeries.coeff_mk, PowerSeries.coeff_mul, hI.dpow_add n ha hb,
  Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
State after:
no goals