awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h₅ : -a = -(2 * k) + (HAdd.hAdd (α := α) (-1) (-1) + 1)
⊢ -a = 2 * -(k + 1) + 1
have h₆ : -a = -(2 * k) + -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)
h₅ : -a = -(2 * k) + (HAdd.hAdd (α := α) (-1) (-1) + 1)
h₆ : -a = -(2 * k) + -1
⊢ -a = 2 * -(k + 1) + 1
have h₇ : -a = -(2 * k + 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)
h₅ : -a = -(2 * k) + (HAdd.hAdd (α := α) (-1) (-1) + 1)
h₆ : -a = -(2 * k) + -1
h₇ : -a = -(2 * k + 1)
⊢ -a = 2 * -(k + 1) + 1
have h₈ : -(2 * k + 1) = -(2 * k + 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 b : α
ha : Odd a
hb : Even b
⊢ Odd (a - b)
have rw : Odd (a + -b)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a - b)
have rw : Odd (a + -b)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a - b)
have rw : Even (a + -b)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
⊢ Odd (a + 2) ↔ Odd a
have rw : Odd (a + HAdd.hAdd (α := α) 1 1) ↔ Odd a
Tactic: rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
rw : Odd (a + HAdd.hAdd (α := α) 1 1) ↔ Odd a
⊢ Odd (a + 2) ↔ Odd a
have rw₁ : Odd (a + 1 + 1) ↔ Odd a
Tactic: rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
rw : Odd (a + HAdd.hAdd (α := α) 1 1) ↔ Odd a
rw₁ : Odd (a + 1 + 1) ↔ Odd a
⊢ Odd (a + 2) ↔ Odd a
have rw₂ : Even (a + 1) ↔ Odd a
Tactic: rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
rw : Odd (a + HAdd.hAdd (α := α) 1 1) ↔ Odd a
rw₁ : Odd (a + 1 + 1) ↔ Odd a
rw₂ : Even (a + 1) ↔ Odd a
⊢ Odd (a + 2) ↔ Odd a
have rw₃ : Odd a ↔ Odd a
Tactic: rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
⊢ Odd (a - 2) ↔ Odd a
have rw : Odd (a - 2 + 2) ↔ Odd a
Tactic: rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
rw : Odd (a - 2 + 2) ↔ Odd a
⊢ Odd (a - 2) ↔ Odd a
have rw₁ : Odd (a + HSub.hSub (α := α) 2 2) ↔ Odd a
Tactic: rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
rw : Odd (a - 2 + 2) ↔ Odd a
rw₁ : Odd (a + HSub.hSub (α := α) 2 2) ↔ Odd a
⊢ Odd (a - 2) ↔ Odd a
have rw₂ : Odd (a + 0) ↔ Odd a
Tactic: rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : Ring α
a : α
rw : Odd (a - 2 + 2) ↔ Odd a
rw₁ : Odd (a + HSub.hSub (α := α) 2 2) ↔ Odd a
rw₂ : Odd (a + 0) ↔ Odd a
⊢ Odd (a - 2) ↔ Odd a
have rw₃ : Odd a ↔ Odd a
Tactic: rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
n : ℕ
⊢ ∃ (k : ℕ), Xor (n = 2 * k) (n = 2 * k + 1)
have inl : ∀ (k : ℕ), ∃ (k_1 : ℕ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
Tactic: obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
n : ℕ
inl : ∀ (k : ℕ), ∃ (k_1 : ℕ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
⊢ ∃ (k : ℕ), Xor (n = 2 * k) (n = 2 * k + 1)
have inr : ∀ (k : ℕ), ∃ (k_1 : ℕ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Tactic: obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
k : ℕ
⊢ ∃ (k_1 : ℕ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
have h : Xor (k + k = 2 * k) (k + k = 2 * k + 1)
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
k : ℕ
⊢ ∃ (k_1 : ℕ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
have h : Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
m n : ℕ
⊢ Even (m / n) ↔ m % (2 * n) / n = 0
have rw : 2 ∣ m / n ↔ m % (2 * n) / n = 0
Tactic: rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
m n : ℕ
rw : 2 ∣ m / n ↔ m % (2 * n) / n = 0
⊢ Even (m / n) ↔ m % (2 * n) / n = 0
have rw₁ : m / n % 2 = 0 ↔ m % (2 * n) / n = 0
Tactic: rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
m n : ℕ
rw : 2 ∣ m / n ↔ m % (2 * n) / n = 0
rw₁ : m / n % 2 = 0 ↔ m % (2 * n) / n = 0
⊢ Even (m / n) ↔ m % (2 * n) / n = 0
have rw₂ : m % (n * 2) / n = 0 ↔ m % (2 * n) / n = 0
Tactic: rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
m n : ℕ
rw : 2 ∣ m / n ↔ m % (2 * n) / n = 0
rw₁ : m / n % 2 = 0 ↔ m % (2 * n) / n = 0
rw₂ : m % (n * 2) / n = 0 ↔ m % (2 * n) / n = 0
⊢ Even (m / n) ↔ m % (2 * n) / n = 0
have rw₃ : m % (2 * n) / n = 0 ↔ m % (2 * n) / n = 0
Tactic: rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
k : ℕ
⊢ 2 ∣ k * (k - 1)
have zero : 2 ∣ 0 * HSub.hSub (α := ℕ) 0 1
Tactic: rcases k with rfl | k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
k : ℕ
zero : 2 ∣ 0 * HSub.hSub (α := ℕ) 0 1
⊢ 2 ∣ k * (k - 1)
have succ : ∀ (k : ℕ), 2 ∣ (k + 1) * (k + 1 - 1)
Tactic: rcases k with rfl | k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n] = id
have rw : f^[2]^[n] = id
Tactic: rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
rw : f^[2]^[n] = id
⊢ f^[2 * n] = id
have rw₁ : Eq.{u_4 + 1} (α := α → α) id^[n] id
Tactic: rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
rw : f^[2]^[n] = id
rw₁ : Eq.{u_4 + 1} (α := α → α) id^[n] id
⊢ f^[2 * n] = id
have rw₂ : Eq.{u_4 + 1} (α := α → α) id id
Tactic: rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n + 1] = f
have rw : f^[2 * n] ∘ f = f
Tactic: rw [iterate_succ, hf.iterate_two_mul, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
rw : f^[2 * n] ∘ f = f
⊢ f^[2 * n + 1] = f
have rw₁ : id ∘ f = f
Tactic: rw [iterate_succ, hf.iterate_two_mul, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
rw : f^[2 * n] ∘ f = f
rw₁ : id ∘ f = f
⊢ f^[2 * n + 1] = f
have rw₂ : f = f
Tactic: rw [iterate_succ, hf.iterate_two_mul, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id
have obtain : ∀ (m : ℕ), f^[m + m] = id
Tactic: obtain ⟨m, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id
have rw : f^[2 * m] = id
Tactic: rw [← two_mul, hf.iterate_two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
rw : f^[2 * m] = id
⊢ f^[m + m] = id
have rw₁ : Eq.{u_4 + 1} (α := α → α) id id
Tactic: rw [← two_mul, hf.iterate_two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f
have obtain : ∀ (m : ℕ), f^[2 * m + 1] = f
Tactic: obtain ⟨m, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
have rw : f^[2 * m] ∘ f^[1] = f
Tactic: rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
rw : f^[2 * m] ∘ f^[1] = f
⊢ f^[2 * m + 1] = f
have rw₁ : id ∘ f^[1] = f
Tactic: rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
rw : f^[2 * m] ∘ f^[1] = f
rw₁ : id ∘ f^[1] = f
⊢ f^[2 * m + 1] = f
have rw₂ : f^[1] = f
Tactic: rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
rw : f^[2 * m] ∘ f^[1] = f
rw₁ : id ∘ f^[1] = f
rw₂ : f^[1] = f
⊢ f^[2 * m + 1] = f
have rw₃ : f = f
Tactic: rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
⊢ f = id
have rwa : ∀ (H : id = f) (hn : Even n), f = id
Tactic: rwa [hf.iterate_even hn, eq_comm] at H
Cleared hypotheses: H, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
rwa : ∀ (H : id = f) (hn : Even n), f = id
⊢ f = id
have rwa₁ : ∀ (H : f = id) (hn : Even n), f = id
Tactic: rwa [hf.iterate_even hn, eq_comm] at H
Cleared hypotheses: H, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
⊢ f = id
have rwa : ∀ (H : f = id) (hn : Odd n), f = id
Tactic: rwa [hf.iterate_odd hn] at H
Cleared hypotheses: H, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Even n
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1
have inl : Eq.{u_4 + 1} (α := R) 1 (if Even n then 1 else -1)
Tactic: rw [h.neg_one_pow, if_pos h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Even n
inl : Eq.{u_4 + 1} (α := R) 1 (if Even n then 1 else -1)
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1
have inl₁ : Eq.{u_4 + 1} (α := R) 1 1
Tactic: rw [h.neg_one_pow, if_pos h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Odd n
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1
have inr : Eq.{u_4 + 1} (α := R) (-1) (if Even n then 1 else -1)
Tactic: rw [h.neg_one_pow, if_neg (by simpa using h)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Odd n
inr : Eq.{u_4 + 1} (α := R) (-1) (if Even n then 1 else -1)
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1
have inr₁ : Eq.{u_4 + 1} (α := R) (-1) (-1)
Tactic: rw [h.neg_one_pow, if_neg (by simpa using h)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (hypothesis)
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1
have x : Even n ∨ Odd n
Tactic: cases even_or_odd n with
  | inl h => rw [h.neg_one_pow, if_pos h]
  | inr h => rw [h.neg_one_pow, if_neg (by simpa using h)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
have simp_rw : (-a) ^ (2 * c) = a ^ (2 * c)
Tactic: simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
c : ℤ
a : α
simp_rw : (-a) ^ (2 * c) = a ^ (2 * c)
⊢ (-a) ^ (c + c) = a ^ (c + c)
have simp_rw₁ : HPow.hPow (β := ℤ) (-a) 2 ^ c = HPow.hPow (β := ℤ) a 2 ^ c
Tactic: simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
c : ℤ
a : α
simp_rw : (-a) ^ (2 * c) = a ^ (2 * c)
simp_rw₁ : HPow.hPow (β := ℤ) (-a) 2 ^ c = HPow.hPow (β := ℤ) a 2 ^ c
⊢ (-a) ^ (c + c) = a ^ (c + c)
have simp_rw₂ : (-a * -a) ^ c = (a * a) ^ c
Tactic: simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Even n
⊢ HPow.hPow (α := α) (-1) n = 1
have rw : HPow.hPow (α := α) 1 n = 1
Tactic: rw [h.neg_zpow, one_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Even n
rw : HPow.hPow (α := α) 1 n = 1
⊢ HPow.hPow (α := α) (-1) n = 1
have rw₁ : Eq.{u_2 + 1} (α := α) 1 1
Tactic: rw [h.neg_zpow, one_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
⊢ HPow.hPow (α := α) (-1) n = if Even n then 1 else -1
have obtain : ∀ (n_1 : ℕ), n = (↑n_1 : ℤ) ∨ n = -(↑n_1 : ℤ) → HPow.hPow (α := α) (-1) n = if Even n then 1 else -1
Tactic: obtain ⟨n, _⟩ := n.eq_nat_or_neg
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
⊢ (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1)
have zero : (Even (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 0) ∧ (Odd (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 1)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n _ _ => simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
zero : (Even (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 0) ∧ (Odd (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 1)
⊢ (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1)
have one : (Even (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 0) ∧ (Odd (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 1)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n _ _ => simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
zero : (Even (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 0) ∧ (Odd (α := ℕ) 0 → Eq.{u_4 + 1} (α := R) (↑0 : R) 1)
one : (Even (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 0) ∧ (Odd (α := ℕ) 1 → Eq.{u_4 + 1} (α := R) (↑1 : R) 1)
⊢ (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1)
have more : ∀ (n : ℕ),
  (Even n → Eq.{u_4 + 1} (α := R) (↑n : R) 0) ∧ (Odd n → Eq.{u_4 + 1} (α := R) (↑n : R) 1) →
    (Even (n + 1) → Eq.{u_4 + 1} (α := R) (↑(n + 1) : R) 0) ∧ (Odd (n + 1) → Eq.{u_4 + 1} (α := R) (↑(n + 1) : R) 1) →
      (Even (n + 2) → Eq.{u_4 + 1} (α := R) (↑(n + 2) : R) 0) ∧ (Odd (n + 2) → Eq.{u_4 + 1} (α := R) (↑(n + 2) : R) 1)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n _ _ => simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
have inl : ∀ (hn : Even n), Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
Tactic: obtain hn | hn := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Parity (goal)
Goal:
R : Type u_4
inst : AddMonoidWithOne R
n : ℕ
h : Eq.{u_4 + 1} (α := R) 2 0
inl : ∀ (hn : Even n), Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
⊢ Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
have inr : ∀ (hn : Odd n), Eq.{u_4 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_4 + 1} (α := R) (↑n : R) 1
Tactic: obtain hn | hn := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
g : α → β
l : List (α → β)
ih : ∀ (hl : ∀ f ∈ l, Periodic f c), Periodic l.prod c
hl : ∀ f ∈ g :: l, Periodic f c
⊢ Periodic (g :: l).prod c
have hl₁ : Periodic g c ∧ ∀ x ∈ l, Periodic x c
Tactic: rw [List.forall_mem_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
l : List (α → β)
hl : ∀ f ∈ l, Periodic f c
⊢ Periodic l.prod c
have nil : ∀ (hl : ∀ (f : α → β), Membership.mem (γ := List (α → β)) [] f → Periodic f c),
  Periodic.{u_1, u_2} (β := β) (List.prod []) c
Tactic: induction l with
  | nil => simp
  | cons g l ih =>
    rw [List.forall_mem_cons] at hl
    simpa only [List.prod_cons] using hl.1.mul (ih hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
c : α
inst : Add α
inst_1 : MulOneClass β
l : List (α → β)
hl : ∀ f ∈ l, Periodic f c
nil :
  ∀ (hl : ∀ (f : α → β), Membership.mem (γ := List (α → β)) [] f → Periodic f c),
    Periodic.{u_1, u_2} (β := β) (List.prod []) c
⊢ Periodic l.prod c
have cons : ∀ (g : α → β) (l : List (α → β)) (ih : ∀ (hl : ∀ f ∈ l, Periodic f c), Periodic l.prod c)
  (hl : ∀ f ∈ g :: l, Periodic f c), Periodic (g :: l).prod c
Tactic: induction l with
  | nil => simp
  | cons g l ih =>
    rw [List.forall_mem_cons] at hl
    simpa only [List.prod_cons] using hl.1.mul (ih hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x
have rw : f (x + (c₁ + -c₂)) = f x
Tactic: rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
rw : f (x + (c₁ + -c₂)) = f x
⊢ f (x + (c₁ - c₂)) = f x
have rw₁ : f (x + c₁ + -c₂) = f x
Tactic: rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
rw : f (x + (c₁ + -c₂)) = f x
rw₁ : f (x + c₁ + -c₂) = f x
⊢ f (x + (c₁ - c₂)) = f x
have rw₂ : f (x + c₁) = f x
Tactic: rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
rw : f (x + (c₁ + -c₂)) = f x
rw₁ : f (x + c₁ + -c₂) = f x
rw₂ : f (x + c₁) = f x
⊢ f (x + (c₁ - c₂)) = f x
have rw₃ : f x = f x
Tactic: rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)
have zero : Periodic f (HSMul.hSMul (α := ℕ) 0 c)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddMonoid α
h : Periodic f c
n : ℕ
zero : Periodic f (HSMul.hSMul (α := ℕ) 0 c)
⊢ Periodic f (n • c)
have succ : ∀ (n : ℕ), Periodic f (n • c) → Periodic f ((n + 1) • c)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℤ
⊢ Periodic f (n • c)
have ofNat : ∀ (n : ℕ), Periodic f (Int.ofNat n • c)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddGroup α
h : Periodic f c
n : ℤ
ofNat : ∀ (n : ℕ), Periodic f (Int.ofNat n • c)
⊢ Periodic f (n • c)
have negSucc : ∀ (n : ℕ), Periodic f (Int.negSucc n • c)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddZeroClass α
f : α → β
x : α
⊢ f (x + 0) = f x
have rw : f x = f x
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
a : α
⊢ Periodic.{0, u_1} (β := α) (fun (x : ℕ) ↦ f^[x] a) n ↔ IsPeriodicPt f n a
have refine : ∀ (h : IsPeriodicPt f n a) (k : ℕ), Eq.{u_1 + 1} (α := α) ((fun (x : ℕ) ↦ f^[x] a) (k + n)) ((fun (x : ℕ) ↦ f^[x] a) k)
Tactic: refine ⟨fun h ↦ h.eq, fun h k ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
hf : Periodic f c
a : ↥(AddSubgroup.zmultiples c)
x : α
⊢ f (a +ᵥ x) = f x
have rcases : ∀ (m : ℤ),
  f
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples c) x)
          ((fun (x : ℤ) ↦ x • c) m) sorry +ᵥ
        x) =
    f x
Tactic: rcases a with ⟨_, m, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommMonoid α
hf : Periodic f c
a : ↥(AddSubmonoid.multiples c)
x : α
⊢ f (a +ᵥ x) = f x
have rcases : ∀ (m : ℕ),
  f
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubmonoid α) (AddSubmonoid.multiples c) x)
          ((fun (i : ℕ) ↦ i • c) m) sorry +ᵥ
        x) =
    f x
Tactic: rcases a with ⟨_, m, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Periodic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x_1 : α
inst : AddGroup α
h : Periodic f c
x : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples c)
a b : α
h' : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples c) : α → α → Prop) a b
⊢ f a = f b
have h'₁ : Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples c) (-a + b)
Tactic: rw [QuotientAddGroup.leftRel_apply] at h'
Cleared hypotheses: h'