awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
⊢ a ^ (HMul.hMul (α := ℕ) 2 0 + 1) + b ^ (HMul.hMul (α := ℕ) 2 0 + 1) = 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.Parity
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

Tactic:
?_
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
a b : α
inst_1 : IsCancelAdd α
hab : a + b = 0
k : ℕ
succ : ∀ (k : ℕ) (ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0), a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
⊢ a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0

Tactic:
induction k with | zero => simpa | succ k ih => ?_
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := α) 0 0
⊢ HPow.hPow (β := ℕ) a 2 + a * b = 0

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

Premises used: sq, MulZeroClass.mul_zero, mul_add
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₄ rw₅ : Eq.{u_2 + 1} (α := α) 0 0
⊢ 0 = HPow.hPow (β := ℕ) b 2 + a * b

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

Premises used: add_mul, MulZeroClass.zero_mul, sq, add_comm
-- Module: Mathlib.Algebra.Ring.Parity
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 = 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]
-- Module: Mathlib.Algebra.Ring.Parity
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

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

Premises used: add_right_cancel
-- Module: Mathlib.Algebra.Ring.Parity
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
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
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

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

Premises used: add_right_cancel
-- Module: Mathlib.Algebra.Ring.Parity
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 :
  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)
⊢ 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:
rw [add_mul, ← pow_add, add_right_comm]

Premises used: add_mul, pow_add, add_right_comm
-- Module: Mathlib.Algebra.Ring.Parity
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) * 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:
rfl
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₅ rw₆ : b ^ (2 * k + 3) = b ^ (2 * k + 1 + 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

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

Premises used: MulZeroClass.zero_mul, pow_add, zero_add
-- Module: Mathlib.Algebra.Ring.Parity
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) + b ^ (2 * k + 1)) * HPow.hPow (β := ℕ) a 2 + b ^ (2 * k + 3) =
    0 + b ^ (2 * k + 1) * HPow.hPow (β := ℕ) a 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

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]

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
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)
rw₃ rw₄ : a = a
⊢ a = (↑u⁻¹ : α) * a + (↑u⁻¹ : α) * a

Tactic:
rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]

Premises used: two_mul, mul_add, Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
⊢ IsUnit.{u_2} (M := α) 2 ↔ ∀ (a : α), Even a

Tactic:
⟨Even.of_isUnit_two, fun h => ?_⟩

Premises used: Iff.intro, Even.of_isUnit_two
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
refine : ∀ (h : ∀ (a : α), Even a), IsUnit.{u_2} (M := α) 2
⊢ IsUnit.{u_2} (M := α) 2 ↔ ∀ (a : α), Even a

Tactic:
refine ⟨Even.of_isUnit_two, fun h => ?_⟩
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
h : ∀ (a : α), Even a
obtain : ∀ (a : α) (ha : 1 = a + a), IsUnit.{u_2} (M := α) 2
⊢ IsUnit.{u_2} (M := α) 2

Tactic:
obtain ⟨a, ha⟩ := h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = a + a
⊢ 2 * a = 1

Tactic:
rw [← two_mul, eq_comm] at ha

Premises used: two_mul, eq_comm
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 2 * a = 1
⊢ IsUnit.{u_2} (M := α) 2

Tactic:
⟨⟨2, a, ha, .trans (Commute.ofNat_right _ _).eq ha⟩, rfl⟩

Premises used: IsUnit, Units.mk, Exists.intro, Commute.ofNat_right, OfNat.ofNat, Commute.eq, rfl, Eq.trans
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 2 * a = 1
⊢ IsUnit.{u_2} (M := α) 2

Tactic:
exact ⟨⟨2, a, ha, .trans (Commute.ofNat_right _ _).eq ha⟩, rfl⟩
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
h : IsUnit.{u_2} (M := α) 2
a : α
rw : Odd (a - 1 + 1)
⊢ Odd a

Tactic:
rw [← sub_add_cancel a 1]

Premises used: OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
h : IsUnit.{u_2} (M := α) 2
a : α
⊢ Odd (a - 1 + 1)

Tactic:
(Even.of_isUnit_two h _).add_one

Premises used: Even.add_one, Even.of_isUnit_two
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
h : IsUnit.{u_2} (M := α) 2
a : α
⊢ Odd (a - 1 + 1)

Tactic:
exact (Even.of_isUnit_two h _).add_one

Premises used: Even.add_one, Even.of_isUnit_two
-- Module: Mathlib.Algebra.Ring.Parity
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)
simp_rw₃ : HPow.hPow (β := ℕ) a 2 ^ c * -a = -(HPow.hPow (β := ℕ) a 2 ^ c * a)
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)

Tactic:
simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

Premises used: pow_add, neg_sq, pow_mul, pow_one, mul_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Monoid α
inst_1 : HasDistribNeg α
n : ℕ
h : Odd n
rw : -HPow.hPow (α := α) 1 n = -1
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) (-1) (-1)
⊢ HPow.hPow (α := α) (-1) n = -1

Tactic:
rw [h.neg_pow, one_pow]

Premises used: one_pow, Odd.neg_pow
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
⊢ Even.{u_2} (α := α) (-2)

Tactic:
simp only [even_neg, even_two]

Premises used: even_two, even_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a : α
hp : Odd a
obtain : ∀ (k : α) (hk : a = 2 * k + 1), Odd (-a)
⊢ Odd (-a)

Tactic:
obtain ⟨k, hk⟩ := hp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a k : α
hk : a = 2 * k + 1
h : -a = 2 * -(k + 1) + 1
⊢ Odd (-a)

Tactic:
use -(k + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
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)
h₈ h₉ : -(2 * k + 1) = -(2 * k + 1)
⊢ -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]

Premises used: add_assoc, two_mul, neg_add, neg_add_cancel_right, mul_add, OfNat.ofNat, mul_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a : α
⊢ Odd (-a) ↔ Odd a

Tactic:
⟨fun h ↦ neg_neg a ▸ h.neg, Odd.neg⟩

Premises used: Odd.neg, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
⊢ Odd.{u_2} (α := α) (-1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Even b
rw : Odd (a + -b)
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)

Tactic:
ha.add_even hb.neg

Premises used: Odd.add_even, Even.neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)

Tactic:
exact ha.add_even hb.neg

Premises used: Odd.add_even, Even.neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Even a
hb : Odd b
rw : Odd (a + -b)
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)

Tactic:
ha.add_odd hb.neg

Premises used: Odd.neg, Even.add_odd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)

Tactic:
exact ha.add_odd hb.neg

Premises used: Odd.neg, Even.add_odd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Odd b
rw : Even (a + -b)
⊢ Even (a - b)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)

Tactic:
ha.add_odd hb.neg

Premises used: Odd.neg, Odd.add_odd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)

Tactic:
exact ha.add_odd hb.neg

Premises used: Odd.neg, Odd.add_odd
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₃ rw₄ : Odd a ↔ Odd a
⊢ Odd (a + 2) ↔ Odd a

Tactic:
rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]

Premises used: add_assoc, one_add_one_eq_two, even_add_one, odd_add_one
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₃ rw₄ : Odd a ↔ Odd a
⊢ Odd (a - 2) ↔ Odd a

Tactic:
rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]

Premises used: sub_self, odd_add_two, add_comm_sub, add_zero
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
h : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
h : n % 2 = 1
⊢ n = 2 * (n / 2) + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ ¬Odd n ↔ Even n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ ¬Even n ↔ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
⊢ ¬Odd (α := ℕ) 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
h : Odd n
⊢ ¬2 ∣ n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ Xor (Even n) (Odd n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ Even n ∨ Odd n

Tactic:
(even_xor_odd n).or

Premises used: Nat.even_xor_odd, Xor.or
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ ∃ (k : ℕ), n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa only [← two_mul, exists_or, Odd, Even] using even_or_odd n

Premises used: exists_or, Odd, two_mul, Even, Nat.even_or_odd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
inl : ∀ (k : ℕ), ∃ (k_1 : ℕ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
inr : ∀ (k : ℕ), ∃ (k_1 : ℕ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
⊢ ∃ (k : ℕ), Xor (n = 2 * k) (n = 2 * k + 1)

Tactic:
obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n

Premises used: Nat.even_or_odd, rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
h : Xor (k + k = 2 * k) (k + k = 2 * k + 1)
⊢ ∃ (k_1 : ℕ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
use k
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
⊢ Xor (k + k = 2 * k) (k + k = 2 * k + 1)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
h : Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
⊢ ∃ (k_1 : ℕ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
use k
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
⊢ Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ Odd (n + 1) ↔ ¬Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
hn : Odd n
⊢ m % 2 + (m + n) % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m : ℕ
⊢ m % 2 + (m + 1) % 2 = 1

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m : ℕ
⊢ (m + 1) % 2 + m % 2 = 1

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ ¬Even (2 * n + 1)

Tactic:
simp [parity_simps]
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
⊢ ¬Even (2 * n + 1)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ Even (m - n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : Odd (m * n)
⊢ Odd m

Tactic:
(odd_mul.mp h).1

Premises used: Nat.odd_mul, And.left, Iff.mp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : Odd (m * n)
⊢ Odd n

Tactic:
(odd_mul.mp h).2

Premises used: Nat.odd_mul, And.right, Iff.mp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n e : ℕ
he : e ≠ 0
⊢ Odd (n ^ e) ↔ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₃ rw₄ : m % (2 * n) / n = 0 ↔ m % (2 * n) / n = 0
⊢ Even (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]

Premises used: Nat.dvd_iff_mod_eq_zero, mul_comm, even_iff_two_dvd, Nat.mod_mul_right_div_self
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : n ≤ m
hm : Odd m
hn : Even n
⊢ Odd (m - n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
m n : ℕ
h : n ≤ m
hm : Even m
hn : Odd n
⊢ Odd (m - n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
h : Odd n
⊢ 2 * (n / 2) + 1 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
h : Odd n
⊢ n / 2 * 2 + 1 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
n : ℕ
h : Odd n
⊢ 1 + n / 2 * 2 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
⊢ 2 ∣ k * (k + 1)

Tactic:
even_iff_two_dvd.mp (even_mul_succ_self k)

Premises used: Nat.even_mul_succ_self, Iff.mp, even_iff_two_dvd
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
zero : 2 ∣ 0 * HSub.hSub (α := ℕ) 0 1
succ : ∀ (k : ℕ), 2 ∣ (k + 1) * (k + 1 - 1)
⊢ 2 ∣ k * (k - 1)

Tactic:
rcases k with rfl | k

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
⊢ 2 ∣ 0 * HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)

Tactic:
simpa [mul_comm (k + 1)] using k.two_dvd_mul_add_one

Premises used: HAdd.hAdd, mul_comm, Nat.two_dvd_mul_add_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
m_1 n_1 m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (HPow.hPow (β := ℕ) m 2 + m + n)

Tactic:
simp [*, parity_simps]
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
m n : ℕ
⊢ ¬Even (α := ℕ) 25394535

Tactic:
decide
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
rw : f^[2]^[n] = id
rw₁ : Eq.{u_4 + 1} (α := α → α) id^[n] id
rw₂ rw₃ : Eq.{u_4 + 1} (α := α → α) id id
⊢ f^[2 * n] = id

Tactic:
rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]

Premises used: Function.iterate_id, Function.involutive_iff_iter_2_eq_id, Function.iterate_mul, Iff.mp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
rw : f^[2 * n] ∘ f = f
rw₁ : id ∘ f = f
rw₂ rw₃ : f = f
⊢ f^[2 * n + 1] = f

Tactic:
rw [iterate_succ, hf.iterate_two_mul, id_comp]

Premises used: Function.iterate_succ, Function.Involutive.iterate_two_mul, Function.id_comp
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
obtain : ∀ (m : ℕ), f^[m + m] = id
⊢ f^[n] = id

Tactic:
obtain ⟨m, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
rw : f^[2 * m] = id
rw₁ rw₂ : Eq.{u_4 + 1} (α := α → α) id id
⊢ f^[m + m] = id

Tactic:
rw [← two_mul, hf.iterate_two_mul]

Premises used: two_mul, Function.Involutive.iterate_two_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
obtain : ∀ (m : ℕ), f^[2 * m + 1] = f
⊢ f^[n] = f

Tactic:
obtain ⟨m, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Parity
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
rw₃ rw₄ : f = f
⊢ f^[2 * m + 1] = f

Tactic:
rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]

Premises used: Function.Involutive.iterate_two_mul, Function.iterate_add, Function.iterate_one, Function.id_comp
-- Module: Mathlib.Algebra.Ring.Parity
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : f = id) (hn : Even n), f = id
⊢ f = id

Tactic:
rwa [hf.iterate_even hn, eq_comm] at H

Premises used: Function.Involutive.iterate_even, eq_comm
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
rwa rwa₁ rwa₂ rwa₃ : ∀ (H : f = id) (hn : Odd n), f = id
⊢ f = id

Tactic:
rwa [hf.iterate_odd hn] at H

Premises used: Function.Involutive.iterate_odd
-- Module: Mathlib.Algebra.Ring.Parity
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)
inl₁ inl₂ : Eq.{u_4 + 1} (α := R) 1 1
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1

Tactic:
rw [h.neg_one_pow, if_pos h]

Premises used: Even.neg_one_pow, if_pos
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Odd n
⊢ ¬Even n

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Ring.Parity
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)
inr₁ inr₂ : Eq.{u_4 + 1} (α := R) (-1) (-1)
⊢ HPow.hPow (α := R) (-1) n = if Even n then 1 else -1

Tactic:
rw [h.neg_one_pow, if_neg (by simpa using h)]

Premises used: if_neg, Odd.neg_one_pow
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
⊢ 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)]

Premises used: Nat.even_or_odd, if_neg
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
m n : ℕ
h : Even m ↔ Even n
⊢ HPow.hPow (α := R) (-1) m = HPow.hPow (α := R) (-1) n

Tactic:
simp [h, neg_one_pow_eq_ite]

Premises used: neg_one_pow_eq_ite
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Ne.{u_4 + 1} (α := R) (-1) 1
⊢ HPow.hPow (α := R) (-1) n = 1 ↔ Even n

Tactic:
simp [neg_one_pow_eq_ite, h]

Premises used: neg_one_pow_eq_ite
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
R : Type u_4
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : Ne.{u_4 + 1} (α := R) (-1) 1
⊢ HPow.hPow (α := R) (-1) n = -1 ↔ Odd n

Tactic:
simp [neg_one_pow_eq_ite, h.symm]

Premises used: neg_one_pow_eq_ite, Ne.symm
-- Module: Mathlib.Algebra.Ring.Parity
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
simp_rw₂ : (-a * -a) ^ c = (a * a) ^ c
⊢ (-a) ^ (c + c) = a ^ (c + c)

Tactic:
simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]

Premises used: zpow_mul, neg_mul_neg, zpow_two, Int.two_mul
-- Module: Mathlib.Algebra.Ring.Parity
Goal:
α : Type u_2
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Even n
rw : HPow.hPow (α := α) 1 n = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) 1 1
⊢ HPow.hPow (α := α) (-1) n = 1

Tactic:
rw [h.neg_zpow, one_zpow]

Premises used: one_zpow, Even.neg_zpow