awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi_1 : i < l.cyclicPermutations.length
j : ℕ
hj_1 : j < l.cyclicPermutations.length
h :
  l.cyclicPermutations.get (⟨i, hi_1⟩ : Fin l.cyclicPermutations.length) =
    l.cyclicPermutations.get (⟨j, hj_1⟩ : Fin l.cyclicPermutations.length)
hi : i < l.length
hj : j < l.length
⊢ (⟨i, hi_1⟩ : Fin l.cyclicPermutations.length) = ⟨j, hj_1⟩

Tactic:
simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h

Premises used: List.Nodup.rotate_congr_iff, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
obtain : ∀ (k : ℕ), l.cyclicPermutations ~r (l.rotate k).cyclicPermutations
⊢ l.cyclicPermutations ~r l'.cyclicPermutations

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
⊢ l.cyclicPermutations.rotate k = (l.rotate k).cyclicPermutations

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
⊢ l.cyclicPermutations ~r (l.rotate k).cyclicPermutations

Tactic:
exact ⟨k, by simp⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'

Tactic:
simp only [IsRotated, ← cyclicPermutations_rotate, cyclicPermutations_inj]

Premises used: List.IsRotated, List.cyclicPermutations_rotate, List.cyclicPermutations_inj
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ n.centralBinom = (2 * n).choose n

Tactic:
rfl

Premises used: Nat.centralBinom, rfl
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ 0 < n.centralBinom

Tactic:
choose_pos (Nat.le_mul_of_pos_left _ zero_lt_two)

Premises used: Nat.centralBinom, Nat.choose_pos, Nat.le_mul_of_pos_left, zero_lt_two
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ n.centralBinom ≠ 0

Tactic:
(centralBinom_pos n).ne'

Premises used: Nat.centralBinom_pos, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
⊢ centralBinom 0 = 1

Tactic:
choose_zero_right _

Premises used: Nat.centralBinom, Nat.choose_zero_right
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
r n : ℕ
rw rw₁ : (2 * n).choose n = (2 * n).choose n
⊢ (2 * n).choose (2 * n / 2) = (2 * n).choose n

Tactic:
rw [Nat.mul_div_cancel_left n zero_lt_two]

Premises used: Nat.mul_div_cancel_left, zero_lt_two
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
n_pos : 0 < n
⊢ 2 ≤ n.centralBinom

Tactic:
calc
    2 ≤ 2 * n := Nat.le_mul_of_pos_right _ n_pos
    _ = (2 * n).choose 1 := (choose_one_right (2 * n)).symm
    _ ≤ centralBinom n := choose_le_centralBinom 1 n

Premises used: Trans.trans, HMul.hMul, Nat.le_mul_of_pos_right, Nat.choose_one_right, OfNat.ofNat, Eq.symm, Nat.choose_le_centralBinom
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ 4 = HPow.hPow (α := ℕ) (β := ℕ) 2 2

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
grw : n.centralBinom ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ n
grw₁ : n.centralBinom ≤ HPow.hPow (α := ℕ) 2 (2 * n)
grw₂ : (2 * n).choose n ≤ HPow.hPow (α := ℕ) 2 (2 * n)
grw₃ grw₄ : HPow.hPow (α := ℕ) 2 (2 * n) ≤ HPow.hPow (α := ℕ) 2 (2 * n)
⊢ n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]

Premises used: pow_mul, Nat.centralBinom_eq_two_mul_choose, Nat.choose_le_two_pow
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : n ≠ 0
⊢ 4 = HPow.hPow (α := ℕ) (β := ℕ) 2 2

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : n ≠ 0
rw : n.centralBinom < HPow.hPow (α := ℕ) 2 (2 * n)
⊢ n.centralBinom < HPow.hPow (α := ℕ) 4 n

Tactic:
rw [show 4 = 2 ^ 2 by rfl, ← pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : n ≠ 0
p : 0 < 2 * n
⊢ n.centralBinom < HPow.hPow (α := ℕ) 2 (2 * n)

Tactic:
apply choose_lt_two_pow

Premises used: Nat.choose_lt_two_pow
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : n ≠ 0
⊢ 0 < 2 * n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
rw : (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1).choose n * (2 * n + 2)
rw₁ rw₂ : (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1 + 1).choose n * (2 * n + 1 + 1 - n)
⊢ (2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)

Tactic:
rw [choose_succ_right_eq, choose_mul_succ_eq]

Premises used: Nat.choose_mul_succ_eq, Nat.choose_succ_right_eq
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ (2 * n + 1).choose n * (2 * n + 2) = 2 * ((2 * n + 1).choose n * (n + 1))

Tactic:
ring
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
rw : 2 * ((n + n + 1).choose n * (n + 1)) = 2 * ((n + n + 1).choose n * (n + n + 1 - n))
rw₁ : 2 * ((n + (n + 1)).choose n * (n + 1)) = 2 * ((n + (n + 1)).choose n * (n + (n + 1) - n))
rw₂ rw₃ : 2 * ((n + (n + 1)).choose n * (n + 1)) = 2 * ((n + (n + 1)).choose n * (n + 1))
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))

Tactic:
rw [two_mul n, add_assoc,
                                                               Nat.add_sub_cancel_left]

Premises used: add_assoc, two_mul, Nat.add_sub_cancel_left
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
rw rw₁ : 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
⊢ 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n).choose n * (2 * n + 1))

Tactic:
rw [choose_mul_succ_eq]

Premises used: Nat.choose_mul_succ_eq
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
rw : 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n + 1) * (2 * n).choose n)
rw₁ rw₂ : 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n).choose n * (2 * n + 1))
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n

Tactic:
rw [mul_assoc, mul_comm (2 * n + 1)]

Premises used: HMul.hMul, mul_assoc, HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
n_big : 4 ≤ n
h :
  ∀ (n : ℕ) (IH : ∀ m < n, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom) (n_big : 4 ≤ n),
    HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n
h : ∀ (hn : n < 4), HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
h₁ :
  ∀ (IH : ∀ m < 4, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom) (n_big : LE.le (α := ℕ) 4 4),
    HPow.hPow (α := ℕ) (β := ℕ) 4 4 < 4 * centralBinom 4
h₂ : ∀ (hn : 4 < n), HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
rcases lt_trichotomy n 4 with (hn | rfl | hn)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
False.elim ((not_lt.2 n_big) hn)

Premises used: Iff.mpr, False.elim, not_lt
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
exact False.elim ((not_lt.2 n_big) hn)

Premises used: Iff.mpr, False.elim, not_lt
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
IH : ∀ m < 4, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : LE.le (α := ℕ) 4 4
⊢ HPow.hPow (α := ℕ) (β := ℕ) 4 4 < 4 * centralBinom 4

Tactic:
norm_num [centralBinom, choose]

Premises used: Nat.choose, Nat.centralBinom
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ ∃ (m : ℕ), n = m + 1

Tactic:
Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)

Premises used: Nat.exists_eq_succ_of_ne_zero, Nat.ne_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
h :
  ∀ (n : ℕ) (IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom) (n_big : 4 ≤ n + 1)
    (hn : 4 < n + 1), HPow.hPow (α := ℕ) 4 (n + 1) < (n + 1) * (n + 1).centralBinom
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)

Premises used: Nat.exists_eq_succ_of_ne_zero, Nat.ne_zero_of_lt, rfl
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
rw rw₁ : 4 * HPow.hPow (α := ℕ) 4 n = 4 * HPow.hPow (α := ℕ) 4 n
⊢ HPow.hPow (α := ℕ) 4 (n + 1) = 4 * HPow.hPow (α := ℕ) 4 n

Tactic:
rw [pow_succ']

Premises used: Nat.pow_succ'
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
hbc : HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
⊢ 4 * HPow.hPow (α := ℕ) 4 n < 4 * (n * n.centralBinom)

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
IH n n.lt_succ_self (Nat.le_of_lt_succ hn)

Premises used: Nat.lt_succ_self, Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)

Premises used: Nat.lt_succ_self, Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
rw : 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
⊢ 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
linarith :
  2 * (2 * n + 1) * n.centralBinom < 4 * n * n.centralBinom →
    -1 + 2 * HSub.hSub (α := ℤ) 0 (↑n.centralBinom : ℤ) +
        (2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) * (↑n.centralBinom : ℤ) + 1 -
          HMul.hMul (α := ℤ) 4 (↑n : ℤ) * (↑n.centralBinom : ℤ)) =
      0
linarith₁ : 2 * (2 * n + 1) * n.centralBinom < 4 * n * n.centralBinom → GT.gt (α := ℤ) 2 0
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
linarith
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 2 * (2 * n + 1) * n.centralBinom = (n + 1) * (n + 1).centralBinom

Tactic:
(succ_mul_centralBinom_succ n).symm

Premises used: Eq.symm, Nat.succ_mul_centralBinom_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
IH : ∀ m < n + 1, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
_ : HPow.hPow (α := ℕ) 4 (n + 1) = 4 * HPow.hPow (α := ℕ) 4 n
_₁ : 4 * HPow.hPow (α := ℕ) 4 n < 4 * (n * n.centralBinom)
_₂ : 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom
⊢ HPow.hPow (α := ℕ) 4 (n + 1) < (n + 1) * (n + 1).centralBinom

Tactic:
calc
    4 ^ (n + 1)
    _ = 4 * 4 ^ n := by rw [pow_succ']
    _ < 4 * (n * centralBinom n) := by gcongr; exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)
    _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
    _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm

Premises used: HMul.hMul, Nat.centralBinom, HAdd.hAdd, OfNat.ofNat, Eq.symm, Nat.succ_mul_centralBinom_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
h : LT.lt (α := ℕ) 0 1
⊢ HPow.hPow (α := ℕ) (β := ℕ) 4 1 ≤ HMul.hMul (α := ℕ) 2 1 * centralBinom 1

Tactic:
simp [centralBinom, choose]

Premises used: Nat.choose, Nat.centralBinom
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
h : LT.lt (α := ℕ) 0 2
⊢ HPow.hPow (α := ℕ) (β := ℕ) 4 2 ≤ HMul.hMul (α := ℕ) 2 2 * centralBinom 2

Tactic:
simp [centralBinom, choose]

Premises used: Nat.choose, Nat.centralBinom
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
h : LT.lt (α := ℕ) 0 3
⊢ HPow.hPow (α := ℕ) (β := ℕ) 4 3 ≤ HMul.hMul (α := ℕ) 2 3 * centralBinom 3

Tactic:
simp [centralBinom, choose]

Premises used: Nat.choose, Nat.centralBinom
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : 0 < n + 4
rw : (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)

Tactic:
Nat.le_mul_of_pos_left _ zero_lt_two

Premises used: Nat.le_mul_of_pos_left, zero_lt_two
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)

Tactic:
refine Nat.le_mul_of_pos_left _ zero_lt_two

Premises used: Nat.le_mul_of_pos_left, zero_lt_two
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : (n + 1).centralBinom = 2 * (n + 1 + n).choose n
⊢ 2 ∣ (n + 1).centralBinom

Tactic:
use (n + 1 + n).choose n

Premises used: Nat.choose, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : (2 * (n + 1)).choose (n + 1) = 2 * (n + 1 + n).choose n
h₁ : (n + 1 + (n + 1)).choose (n + 1) = 2 * (n + 1 + n).choose n
h₂ : (n + 1 + n + 1).choose (n + 1) = 2 * (n + 1 + n).choose n
h₃ : (n + 1 + n).choose n + (n + 1 + n).choose (n + 1) = 2 * (n + 1 + n).choose n
h₄ : (n + 1 + n).choose n + (n + 1 + n).choose n = 2 * (n + 1 + n).choose n
h₅ h₆ : 2 * (n + 1 + n).choose n = 2 * (n + 1 + n).choose n
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n

Tactic:
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc,
      choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]

Premises used: add_assoc, two_mul, Nat.choose_symm_add, HAdd.hAdd, Nat.centralBinom_eq_two_mul_choose, Nat.choose_succ_succ', OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : 0 < n
rw : 2 ∣ n.pred.succ.centralBinom
⊢ 2 ∣ n.centralBinom

Tactic:
rw [← Nat.succ_pred_eq_of_pos h]

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom

Tactic:
two_dvd_centralBinom_succ n.pred

Premises used: Nat.pred, Nat.two_dvd_centralBinom_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom

Tactic:
exact two_dvd_centralBinom_succ n.pred

Premises used: Nat.pred, Nat.two_dvd_centralBinom_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
rw : Coprime 1 n
⊢ (n + 1).Coprime (2 * n + 1)

Tactic:
rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]

Premises used: add_assoc, two_mul, Nat.coprime_self_add_left, Nat.coprime_add_self_right
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ Coprime 1 n

Tactic:
coprime_one_left n

Premises used: Nat.coprime_one_left
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ Coprime 1 n

Tactic:
exact coprime_one_left n

Premises used: Nat.coprime_one_left
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
⊢ (n + 1).Coprime (2 * n + 1)

Tactic:
have h_s : (n + 1).Coprime (2 * n + 1) := by
    rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
    exact coprime_one_left n
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
apply : n + 1 ∣ (2 * n + 1) * n.centralBinom
⊢ n + 1 ∣ n.centralBinom

Tactic:
apply h_s.dvd_of_dvd_mul_left

Premises used: Nat.Coprime.dvd_of_dvd_mul_left
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
apply : 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)
⊢ n + 1 ∣ (2 * n + 1) * n.centralBinom

Tactic:
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two

Premises used: zero_lt_two, Nat.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
rw : (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)

Tactic:
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]

Premises used: mul_assoc, mul_comm, Nat.succ_mul_centralBinom_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom

Tactic:
mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)

Premises used: mul_dvd_mul_left, Nat.two_dvd_centralBinom_succ
-- Module: Mathlib.Data.Nat.Choose.Central
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom

Tactic:
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)

Premises used: mul_dvd_mul_left, Nat.two_dvd_centralBinom_succ
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
m : ℕ := (k + 2).minFac
⊢ (k + 2) / (k + 2).minFac < k.succ.succ

Tactic:
factors_lemma

Premises used: Nat.factors_lemma
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
m : ℕ := (k + 2).minFac
⊢ (k + 2) / (k + 2).minFac < k.succ.succ

Tactic:
exact factors_lemma

Premises used: Nat.factors_lemma
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
m : ℕ := (k + 2).minFac
⊢ (k + 2) / (k + 2).minFac < k.succ.succ

Tactic:
decreasing_by exact factors_lemma

Premises used: Nat.factors_lemma
-- Module: Mathlib.Data.Nat.Factors
Goal:
rw rw₁ : Eq (α := List ℕ) [] []
⊢ primeFactorsList 0 = []

Tactic:
rw [primeFactorsList]

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
rw rw₁ : Eq (α := List ℕ) [] []
⊢ primeFactorsList 1 = []

Tactic:
rw [primeFactorsList]

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ primeFactorsList 2 = [2]

Tactic:
simp [primeFactorsList]

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 0 → Prime p

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 1 → Prime p

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
⊢ (k + 2) / m < k + 2

Tactic:
have : (k + 2) / m < (k + 2) := factors_lemma
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : p ∈ (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList),
    let m := (k + 2).minFac;
    ∀ (this : (k + 2) / m < k + 2), p ∈ m :: ((k + 2) / m).primeFactorsList
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList

Tactic:
rwa [primeFactorsList] at h

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p = m ∨ p ∈ ((k + 2) / m).primeFactorsList

Tactic:
have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
        List.mem_cons.1 (by rwa [primeFactorsList] at h)
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
h₂ : p = m
⊢ k + 2 ≠ 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
⊢ Prime p

Tactic:
exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ n.primeFactorsList → Prime p

Tactic:
match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
      intro p h
      let m := minFac (k + 2)
      have : (k + 2) / m < (k + 2) := factors_lemma
      have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
        List.mem_cons.1 (by rwa [primeFactorsList] at h)
      exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
⊢ 0 < p

Tactic:
Prime.pos (prime_of_mem_primeFactorsList h)

Premises used: Nat.prime_of_mem_primeFactorsList, Nat.Prime.pos
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ Ne (α := ℕ) 0 0 → (primeFactorsList 0).prod = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ Ne (α := ℕ) 1 0 → (primeFactorsList 1).prod = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h_1 : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ k + 2 = 0 * m

Tactic:
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h_1 : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this_1 : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ k + 2 = 0

Tactic:
rw [zero_mul] at this

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h_1 : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this_1 : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ k + 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h_1 : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this_1 : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False

Tactic:
exact (show k + 2 ≠ 0 by simp) this
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ (k + 2) / m ≠ 0

Tactic:
have h₁ : (k + 2) / m ≠ 0 := fun h => by
        have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
        rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
rw : ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2
rw₁ : (k + 2).minFac * ((k + 2) / (k + 2).minFac).primeFactorsList.prod = k + 2
rw₂ : (k + 2).minFac * ((k + 2) / m) = k + 2
rw₃ rw₄ : k + 2 = k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2

Tactic:
rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]

Premises used: Nat.minFac_dvd, List.prod_cons, Nat.mul_div_cancel', Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
⊢ p = p - 2 + 2

Tactic:
have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
rw : (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
⊢ p.primeFactorsList = [p]

Tactic:
rw [this, primeFactorsList]

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
simp : p.minFac :: (p / p.minFac).primeFactorsList = [p]
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]

Tactic:
simp only [Eq.symm this]

Premises used: Eq.symm
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.minFac = p

Tactic:
have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
this_1 : p = p - 2 + 2
this : p.minFac = p
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Tactic:
simp only [this, primeFactorsList, Nat.div_self (Nat.Prime.pos hp)]

Premises used: Nat.Prime.pos, Nat.div_self, Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: primeFactorsList 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: primeFactorsList 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
⊢ (k + 2) / m < k + 2

Tactic:
have : (k + 2) / m < (k + 2) := factors_lemma