awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₅ : 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₆ : 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₇ : 2 * (a * (2 * b) + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₅ : 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₆ : 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₇ : 2 * (a * (2 * b) + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₈ : 2 * (a * 2 * b + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₅ : 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₆ : 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₇ : 2 * (a * (2 * b) + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
rw₈ : 2 * (a * 2 * b + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₉ : (↑2 : α) * (a * (↑2 : α) * b + b + a) + 1 = (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
rw : (2 * a + 1) * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₁ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1
rw₂ : 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
rw₃ : 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₄ : 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₅ : 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₆ : 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
rw₇ : 2 * (a * (2 * b) + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
rw₈ : 2 * (a * 2 * b + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
rw₉ : (↑2 : α) * (a * (↑2 : α) * b + b + a) + 1 = (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
have rw₁₀ : (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1 = (↑2 : α) * ((↑2 : α) * a * b + b + a) + 1
Tactic: rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ (n + 1))
have succ : Odd (a ^ n * a)
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a : α
n : ℕ
ha : Odd a
⊢ Odd (a ^ n)
have zero : Odd (HPow.hPow (β := ℕ) a 0)
Tactic: induction n with
  | zero => simp [pow_zero]
  | succ n hrec => rw [pow_succ]; exact hrec.mul ha
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a : α
n : ℕ
ha : Odd a
zero : Odd (HPow.hPow (β := ℕ) a 0)
⊢ Odd (a ^ n)
have succ : ∀ (n : ℕ) (hrec : Odd (a ^ n)), Odd (a ^ (n + 1))
Tactic: induction n with
  | zero => simp [pow_zero]
  | succ n hrec => rw [pow_succ]; exact hrec.mul ha
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
n : ℕ
inst_1 : IsCancelAdd α
hn : Odd n
hab : a + b = 0
⊢ a ^ n + b ^ n = 0
have obtain : ∀ (k : ℕ), a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
⊢ a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
have succ : ∀ (k : ℕ) (ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0), a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
Tactic: induction k with | zero => simpa | succ k ih => ?_
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ HPow.hPow (β := ℕ) a 2 + a * b = 0
have rw : a * a + a * b = 0
Tactic: rw [sq, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : a * a + a * b = 0
⊢ HPow.hPow (β := ℕ) a 2 + a * b = 0
have rw₁ : a * (a + b) = 0
Tactic: rw [sq, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : a * a + a * b = 0
rw₁ : a * (a + b) = 0
⊢ HPow.hPow (β := ℕ) a 2 + a * b = 0
have rw₂ : a * 0 = 0
Tactic: rw [sq, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : a * a + a * b = 0
rw₁ : a * (a + b) = 0
rw₂ : a * 0 = 0
⊢ HPow.hPow (β := ℕ) a 2 + a * b = 0
have rw₃ : Eq.{u_2 + 1} (α := α) 0 0
Tactic: rw [sq, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = HPow.hPow (β := ℕ) b 2 + a * b
have rw : 0 = b * b + a * b
Tactic: rw [sq, ← add_mul, add_comm, hab, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : 0 = b * b + a * b
⊢ 0 = HPow.hPow (β := ℕ) b 2 + a * b
have rw₁ : 0 = (b + a) * b
Tactic: rw [sq, ← add_mul, add_comm, hab, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : 0 = b * b + a * b
rw₁ : 0 = (b + a) * b
⊢ 0 = HPow.hPow (β := ℕ) b 2 + a * b
have rw₂ : 0 = (a + b) * b
Tactic: rw [sq, ← add_mul, add_comm, hab, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : 0 = b * b + a * b
rw₁ : 0 = (b + a) * b
rw₂ : 0 = (a + b) * b
⊢ 0 = HPow.hPow (β := ℕ) b 2 + a * b
have rw₃ : 0 = 0 * b
Tactic: rw [sq, ← add_mul, add_comm, hab, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
rw : 0 = b * b + a * b
rw₁ : 0 = (b + a) * b
rw₂ : 0 = (a + b) * b
rw₃ : 0 = 0 * b
⊢ 0 = HPow.hPow (β := ℕ) b 2 + a * b
have rw₄ : Eq.{u_2 + 1} (α := α) 0 0
Tactic: rw [sq, ← add_mul, add_comm, hab, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (hypothesis)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : 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
have this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
have succ : a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 =
  0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
Tactic: refine add_right_cancel (b := b ^ (2 * k + 1) * a ^ 2) ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3)
have rw : a ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * (k + 1) + 1) =
  a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3)
Tactic: rw [add_mul, ← pow_add, add_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have rw : 0 * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
Tactic: rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
rw : 0 * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have rw₁ : 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
Tactic: rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
rw : 0 * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₁ : 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have rw₂ : b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
Tactic: rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
rw : 0 * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₁ : 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₂ : b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have rw₃ : b ^ (2 * k + 3) = b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
Tactic: rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
rw : 0 * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₁ : 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₂ : b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₃ : b ^ (2 * k + 3) = b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have rw₄ : b ^ (2 * k + 3) = b ^ (2 * k + 1) * HPow.hPow (β := ℕ) b 2
Tactic: rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
rw : 0 * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₁ : 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₂ : b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₃ : b ^ (2 * k + 3) = b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
rw₄ : b ^ (2 * k + 3) = b ^ (2 * k + 1) * HPow.hPow (β := ℕ) b 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have rw₅ : b ^ (2 * k + 3) = b ^ (2 * k + 1 + 2)
Tactic: rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have _ : a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 =
  (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3)
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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
_ :
  a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3)
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2 =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 2
have _₁ : (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
  0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
h : IsUnit.{u_2} (M := α) 2
a : α
u : αˣ
hu : (↑u : α) = 2
⊢ a = (↑u⁻¹ : α) * a + (↑u⁻¹ : α) * a
have rw : a = (↑u⁻¹ : α) * (a + a)
Tactic: rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
h : IsUnit.{u_2} (M := α) 2
a : α
u : αˣ
hu : (↑u : α) = 2
rw : a = (↑u⁻¹ : α) * (a + a)
⊢ a = (↑u⁻¹ : α) * a + (↑u⁻¹ : α) * a
have rw₁ : a = (↑u⁻¹ : α) * (2 * a)
Tactic: rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
h : IsUnit.{u_2} (M := α) 2
a : α
u : αˣ
hu : (↑u : α) = 2
rw : a = (↑u⁻¹ : α) * (a + a)
rw₁ : a = (↑u⁻¹ : α) * (2 * a)
⊢ a = (↑u⁻¹ : α) * a + (↑u⁻¹ : α) * a
have rw₂ : a = (↑u⁻¹ : α) * ((↑u : α) * a)
Tactic: rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
h : IsUnit.{u_2} (M := α) 2
a : α
u : αˣ
hu : (↑u : α) = 2
rw : a = (↑u⁻¹ : α) * (a + a)
rw₁ : a = (↑u⁻¹ : α) * (2 * a)
rw₂ : a = (↑u⁻¹ : α) * ((↑u : α) * a)
⊢ a = (↑u⁻¹ : α) * a + (↑u⁻¹ : α) * a
have rw₃ : a = a
Tactic: rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
⊢ IsUnit.{u_2} (M := α) 2 ↔ ∀ (a : α), Even a
have refine : ∀ (h : ∀ (a : α), Even a), IsUnit.{u_2} (M := α) 2
Tactic: refine ⟨Even.of_isUnit_two, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Semiring α
h : ∀ (a : α), Even a
⊢ IsUnit.{u_2} (M := α) 2
have obtain : ∀ (a : α) (ha : 1 = a + a), IsUnit.{u_2} (M := α) 2
Tactic: obtain ⟨a, ha⟩ := h 1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (hypothesis)
Goal:
α : Type u_2
inst : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = a + a
⊢ IsUnit.{u_2} (M := α) 2
have ha₁ : 2 * a = 1
Tactic: rw [← two_mul, eq_comm] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
h : IsUnit.{u_2} (M := α) 2
a : α
⊢ Odd a
have rw : Odd (a - 1 + 1)
Tactic: rw [← sub_add_cancel a 1]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
have simp_rw : (-a) ^ (2 * c) * HPow.hPow (β := ℕ) (-a) 1 = -(a ^ (2 * c) * HPow.hPow (β := ℕ) a 1)
Tactic: simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
simp_rw : (-a) ^ (2 * c) * HPow.hPow (β := ℕ) (-a) 1 = -(a ^ (2 * c) * HPow.hPow (β := ℕ) a 1)
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
have simp_rw₁ : HPow.hPow (β := ℕ) (-a) 2 ^ c * HPow.hPow (β := ℕ) (-a) 1 = -(HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) a 1)
Tactic: simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
simp_rw : (-a) ^ (2 * c) * HPow.hPow (β := ℕ) (-a) 1 = -(a ^ (2 * c) * HPow.hPow (β := ℕ) a 1)
simp_rw₁ :
  HPow.hPow (β := ℕ) (-a) 2 ^ c * HPow.hPow (β := ℕ) (-a) 1 = -(HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) a 1)
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
have simp_rw₂ : HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) (-a) 1 = -(HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) a 1)
Tactic: simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
c : ℕ
a : α
simp_rw : (-a) ^ (2 * c) * HPow.hPow (β := ℕ) (-a) 1 = -(a ^ (2 * c) * HPow.hPow (β := ℕ) a 1)
simp_rw₁ :
  HPow.hPow (β := ℕ) (-a) 2 ^ c * HPow.hPow (β := ℕ) (-a) 1 = -(HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) a 1)
simp_rw₂ :
  HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) (-a) 1 = -(HPow.hPow (β := ℕ) a 2 ^ c * HPow.hPow (β := ℕ) a 1)
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
have simp_rw₃ : HPow.hPow (β := ℕ) a 2 ^ c * -a = -(HPow.hPow (β := ℕ) a 2 ^ c * a)
Tactic: simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
n : ℕ
h : Odd n
⊢ HPow.hPow (α := α) (-1) n = -1
have rw : -HPow.hPow (α := α) 1 n = -1
Tactic: rw [h.neg_pow, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
n : ℕ
h : Odd n
rw : -HPow.hPow (α := α) 1 n = -1
⊢ HPow.hPow (α := α) (-1) n = -1
have rw₁ : Eq.{u_2 + 1} (α := α) (-1) (-1)
Tactic: rw [h.neg_pow, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
hp : Odd a
⊢ Odd (-a)
have obtain : ∀ (k : α) (hk : a = 2 * k + 1), Odd (-a)
Tactic: obtain ⟨k, hk⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
⊢ Odd (-a)
have h : -a = 2 * -(k + 1) + 1
Tactic: use -(k + 1)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1
have h : -a = -(2 * (k + 1)) + 1
Tactic: rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
h : -a = -(2 * (k + 1)) + 1
⊢ -a = 2 * -(k + 1) + 1
have h₁ : -a = -(2 * k + HMul.hMul (α := α) 2 1) + 1
Tactic: rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
h : -a = -(2 * (k + 1)) + 1
h₁ : -a = -(2 * k + HMul.hMul (α := α) 2 1) + 1
⊢ -a = 2 * -(k + 1) + 1
have h₂ : -a = -(2 * k) + -HMul.hMul (α := α) 2 1 + 1
Tactic: rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
h : -a = -(2 * (k + 1)) + 1
h₁ : -a = -(2 * k + HMul.hMul (α := α) 2 1) + 1
h₂ : -a = -(2 * k) + -HMul.hMul (α := α) 2 1 + 1
⊢ -a = 2 * -(k + 1) + 1
have h₃ : -a = -(2 * k) + (-HMul.hMul (α := α) 2 1 + 1)
Tactic: rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
h : -a = -(2 * (k + 1)) + 1
h₁ : -a = -(2 * k + HMul.hMul (α := α) 2 1) + 1
h₂ : -a = -(2 * k) + -HMul.hMul (α := α) 2 1 + 1
h₃ : -a = -(2 * k) + (-HMul.hMul (α := α) 2 1 + 1)
⊢ -a = 2 * -(k + 1) + 1
have h₄ : -a = -(2 * k) + (-HAdd.hAdd (α := α) 1 1 + 1)
Tactic: rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
h : -a = -(2 * (k + 1)) + 1
h₁ : -a = -(2 * k + HMul.hMul (α := α) 2 1) + 1
h₂ : -a = -(2 * k) + -HMul.hMul (α := α) 2 1 + 1
h₃ : -a = -(2 * k) + (-HMul.hMul (α := α) 2 1 + 1)
h₄ : -a = -(2 * k) + (-HAdd.hAdd (α := α) 1 1 + 1)
⊢ -a = 2 * -(k + 1) + 1
have h₅ : -a = -(2 * k) + (HAdd.hAdd (α := α) (-1) (-1) + 1)
Tactic: rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]