Theorem: IsNilpotent.add (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
ha : IsNilpotent a
hb : IsNilpotent b
⊢ IsNilpotent (a + b)
Tactic:
obtain ⟨m, ha⟩ := ha
State after:
case intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
hb : IsNilpotent b
m : ℕ
ha : a ^ m = 0
⊢ IsNilpotent (a + b)

State before:
case intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
hb : IsNilpotent b
m : ℕ
ha : a ^ m = 0
⊢ IsNilpotent (a + b)
Tactic:
obtain ⟨n, hb⟩ := hb
State after:
case intro.intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
m : ℕ
ha : a ^ m = 0
n : ℕ
hb : b ^ n = 0
⊢ IsNilpotent (a + b)

State before:
case intro.intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
m : ℕ
ha : a ^ m = 0
n : ℕ
hb : b ^ n = 0
⊢ IsNilpotent (a + b)
Tactic:
exact ⟨_, add_pow_add_pred_eq_zero_of_pow_eq_zero ha hb⟩
State after:
no goals