-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.pow_add_pow_eq_zero [IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) :
    a ^ n + b ^ n = 0

Proof state:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = b ^ 2 + a * b

Tactic:
rw [sq, ← add_mul, add_comm, hab, zero_mul]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
rw [add_mul, ← pow_add, add_right_comm]

Result:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * (k + 1) + 1) =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)

Proof state:
case intro.zero
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
⊢ a ^ (2 * 0 + 1) + b ^ (2 * 0 + 1) = 0

Tactic:
simpa

Result:
no goals

Proof state:
case intro.succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

Tactic:
have : a ^ 2 = b ^ 2 := add_right_cancel <|
  calc
    a ^ 2 + a * b = 0 := by rw [sq, ← mul_add, hab, mul_zero]
    _ = b ^ 2 + a * b := by rw [sq, ← add_mul, add_comm, hab, zero_mul]

Result:
case intro.succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

Proof state:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * (k + 1) + 1) =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Semiring α
a b : α
n : ℕ
inst✝ : IsCancelAdd α
hn : Odd n
hab : a + b = 0
⊢ a ^ n + b ^ n = 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
⊢ a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0

Proof state:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ 2 + a * b = 0

Tactic:
rw [sq, ← mul_add, hab, mul_zero]

Result:
no goals

Proof state:
case intro.succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

Tactic:
refine add_right_cancel (b := b ^ (2 * k + 1) * a ^ 2) ?_

Result:
case intro.succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 = 0 + b ^ (2 * k + 1) * a ^ 2

Proof state:
case intro
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
⊢ a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0

Tactic:
induction' k with k ih

Result:
case intro.zero
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
⊢ a ^ (2 * 0 + 1) + b ^ (2 * 0 + 1) = 0

case intro.succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

Proof state:
case intro.succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
calc
  _ = (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) := by
    rw [add_mul, ← pow_add, add_right_comm]; rfl
  _ = _ := by rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]

Result:
no goals