Theorem: DividedPowers.isExponential_dpowExp (DividedPowers/Exponential.lean)

State before:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (hI.dpowExp a).IsExponential
Tactic:
rw [isExponential_iff]
State after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)

State before:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Tactic:
constructor
State after:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1

case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)

State before:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1
Tactic:
simp only [dpowExp, ← coeff_zero_eq_constantCoeff_apply, coeff_mk, dpow_zero _ ha]
State after:
no goals

State before:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Tactic:
intro p q
State after:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)

State before:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Tactic:
simp only [dpowExp, coeff_mk, hI.dpow_mul p q ha]
State after:
no goals