awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
nil :
  ∀
    (this :
      length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
        length.{u} (α := List α) (rotate (cyclicPermutations []) k))
    (hn : n < length.{u} (α := List α) (cyclicPermutations (rotate [] k)))
    (hn' : n < length.{u} (α := List α) (rotate (cyclicPermutations []) k)),
    Eq.{u + 1} (α := List α)
      (rotate []
        (((↑(⟨n, hn⟩ : Fin (length.{u} (α := List α) (cyclicPermutations (rotate [] k)))) : ℕ) + k) %
          length.{u} (α := α) []))
      (get (cyclicPermutations [])
        ⟨((↑(⟨n, hn'⟩ : Fin (length.{u} (α := List α) (rotate (cyclicPermutations []) k))) : ℕ) + k) %
            length.{u} (α := List α) (cyclicPermutations []),
          ⋯⟩)
⊢ l.rotate (((↑(⟨n, hn⟩ : Fin (l.rotate k).cyclicPermutations.length) : ℕ) + k) % l.length) =
    l.cyclicPermutations.get
      ⟨((↑(⟨n, hn'⟩ : Fin (l.cyclicPermutations.rotate k).length) : ℕ) + k) % l.cyclicPermutations.length, ⋯⟩
have cons : ∀ (head : α) (tail : List α)
  (this : ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length)
  (hn : n < ((head :: tail).rotate k).cyclicPermutations.length)
  (hn' : n < ((head :: tail).cyclicPermutations.rotate k).length),
  (head :: tail).rotate
      (((↑(⟨n, hn⟩ : Fin ((head :: tail).rotate k).cyclicPermutations.length) : ℕ) + k) % (head :: tail).length) =
    (head :: tail).cyclicPermutations.get
      ⟨((↑(⟨n, hn'⟩ : Fin ((head :: tail).cyclicPermutations.rotate k).length) : ℕ) + k) %
          (head :: tail).cyclicPermutations.length,
        sorry⟩
Tactic: cases l
Cleared hypotheses: l, this, hn, hn'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations ↔ l ~r l'
have mp : l ∈ l'.cyclicPermutations → l ~r l'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
mp : l ∈ l'.cyclicPermutations → l ~r l'
⊢ l ∈ l'.cyclicPermutations ↔ l ~r l'
have mpr : l ~r l' → l ∈ l'.cyclicPermutations
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'
have mp : (∃ (n : Fin l'.cyclicPermutations.length), l'.rotate (↑n : ℕ) = l) → l ~r l'
Tactic: simp_rw [mem_iff_get, get_cyclicPermutations]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
k : ℕ
⊢ l ∈ (l.rotate k).cyclicPermutations
have mpr : l ∈ l.cyclicPermutations
Tactic: rw [cyclicPermutations_rotate, mem_rotate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hn : l.Nodup
⊢ l.cyclicPermutations.Nodup
have inl : ∀ (hn : Nodup.{u} (α := α) []), Nodup.{u} (α := List α) (cyclicPermutations [])
Tactic: rcases eq_or_ne l [] with rfl | hl
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hn : l.Nodup
inl : ∀ (hn : Nodup.{u} (α := α) []), Nodup.{u} (α := List α) (cyclicPermutations [])
⊢ l.cyclicPermutations.Nodup
have inr : ∀ (hl : l ≠ []), l.cyclicPermutations.Nodup
Tactic: rcases eq_or_ne l [] with rfl | hl
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup
have inr : Injective l.cyclicPermutations.get
Tactic: rw [nodup_iff_injective_get]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h :
  l.cyclicPermutations.get (⟨i, hi⟩ : Fin l.cyclicPermutations.length) =
    l.cyclicPermutations.get (⟨j, hj⟩ : Fin l.cyclicPermutations.length)
⊢ (⟨i, hi⟩ : Fin l.cyclicPermutations.length) = ⟨j, hj⟩
have hi₁ : i < l.length
Tactic: simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h :
  l.cyclicPermutations.get (⟨i, hi⟩ : Fin l.cyclicPermutations.length) =
    l.cyclicPermutations.get (⟨j, hj⟩ : Fin l.cyclicPermutations.length)
hi₁ : i < l.length
⊢ (⟨i, hi⟩ : Fin l.cyclicPermutations.length) = ⟨j, hj⟩
have hj₁ : j < l.length
Tactic: simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
h : l ~r l'
⊢ l.cyclicPermutations ~r l'.cyclicPermutations
have obtain : ∀ (k : ℕ), l.cyclicPermutations ~r (l.rotate k).cyclicPermutations
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
r n : ℕ
⊢ (2 * n).choose (2 * n / 2) = (2 * n).choose n
have rw : (2 * n).choose n = (2 * n).choose n
Tactic: rw [Nat.mul_div_cancel_left n zero_lt_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw : n.centralBinom ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ n
Tactic: grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
grw : n.centralBinom ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ n
⊢ n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw₁ : n.centralBinom ≤ HPow.hPow (α := ℕ) 2 (2 * n)
Tactic: grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
grw : n.centralBinom ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ n
grw₁ : n.centralBinom ≤ HPow.hPow (α := ℕ) 2 (2 * n)
⊢ n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw₂ : (2 * n).choose n ≤ HPow.hPow (α := ℕ) 2 (2 * n)
Tactic: grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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)
⊢ n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw₃ : HPow.hPow (α := ℕ) 2 (2 * n) ≤ HPow.hPow (α := ℕ) 2 (2 * n)
Tactic: grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ n.centralBinom < HPow.hPow (α := ℕ) 4 n
have rw : n.centralBinom < HPow.hPow (α := ℕ) 2 (2 * n)
Tactic: rw [show 4 = 2 ^ 2 by rfl, ← pow_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ n.centralBinom < HPow.hPow (α := ℕ) 2 (2 * n)
have p : 0 < 2 * n
Tactic: apply choose_lt_two_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ (2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)
have rw : (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1).choose n * (2 * n + 2)
Tactic: rw [choose_succ_right_eq, choose_mul_succ_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
rw : (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1).choose n * (2 * n + 2)
⊢ (2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)
have rw₁ : (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1 + 1).choose n * (2 * n + 1 + 1 - n)
Tactic: rw [choose_succ_right_eq, choose_mul_succ_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
have rw : 2 * ((n + n + 1).choose n * (n + 1)) = 2 * ((n + n + 1).choose n * (n + n + 1 - n))
Tactic: rw [two_mul n, add_assoc,
                                                               Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
rw : 2 * ((n + n + 1).choose n * (n + 1)) = 2 * ((n + n + 1).choose n * (n + n + 1 - n))
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
have rw₁ : 2 * ((n + (n + 1)).choose n * (n + 1)) = 2 * ((n + (n + 1)).choose n * (n + (n + 1) - n))
Tactic: rw [two_mul n, add_assoc,
                                                               Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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))
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
have rw₂ : 2 * ((n + (n + 1)).choose n * (n + 1)) = 2 * ((n + (n + 1)).choose n * (n + 1))
Tactic: rw [two_mul n, add_assoc,
                                                               Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n).choose n * (2 * n + 1))
have rw : 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
Tactic: rw [choose_mul_succ_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n
have rw : 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
rw : 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n + 1) * (2 * n).choose n)
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n
have rw₁ : 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n).choose n * (2 * n + 1))
Tactic: rw [mul_assoc, mul_comm (2 * n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
n_big : 4 ≤ n
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
have 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
Tactic: induction n using Nat.strong_induction_on with | _ n IH
Cleared hypotheses: n, n_big
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
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
have h : ∀ (hn : n < 4), HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
Tactic: rcases lt_trichotomy n 4 with (hn | rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
have 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
Tactic: rcases lt_trichotomy n 4 with (hn | rfl | hn)
Cleared hypotheses: n, IH, n_big
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
have h₂ : ∀ (hn : 4 < n), HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
Tactic: rcases lt_trichotomy n 4 with (hn | rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
IH : ∀ m < n, ∀ (n_big : 4 ≤ m), HPow.hPow (α := ℕ) 4 m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
have 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
Tactic: obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)
Cleared hypotheses: n, IH, n_big, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
have rw : 4 * HPow.hPow (α := ℕ) 4 n = 4 * HPow.hPow (α := ℕ) 4 n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ 4 * HPow.hPow (α := ℕ) 4 n < 4 * (n * n.centralBinom)
have hbc : HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom
have rw : 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
have linarith₁ : 2 * (2 * n + 1) * n.centralBinom < 4 * n * n.centralBinom → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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) < (n + 1) * (n + 1).centralBinom
have _ : HPow.hPow (α := ℕ) 4 (n + 1) = 4 * HPow.hPow (α := ℕ) 4 n
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
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ HPow.hPow (α := ℕ) 4 (n + 1) < (n + 1) * (n + 1).centralBinom
have _₁ : 4 * HPow.hPow (α := ℕ) 4 n < 4 * (n * n.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
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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)
⊢ HPow.hPow (α := ℕ) 4 (n + 1) < (n + 1) * (n + 1).centralBinom
have _₂ : 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.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
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom
have rw : (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ 2 ∣ (n + 1).centralBinom
have h : (n + 1).centralBinom = 2 * (n + 1 + n).choose n
Tactic: use (n + 1 + n).choose n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
have h : (2 * (n + 1)).choose (n + 1) = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h : (2 * (n + 1)).choose (n + 1) = 2 * (n + 1 + n).choose n
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
have h₁ : (n + 1 + (n + 1)).choose (n + 1) = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
have h₂ : (n + 1 + n + 1).choose (n + 1) = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
have h₃ : (n + 1 + n).choose n + (n + 1 + n).choose (n + 1) = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
have h₄ : (n + 1 + n).choose n + (n + 1 + n).choose n = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
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
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
have h₅ : 2 * (n + 1 + n).choose n = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.centralBinom
have rw : 2 ∣ n.pred.succ.centralBinom
Tactic: rw [← Nat.succ_pred_eq_of_pos h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
⊢ (n + 1).Coprime (2 * n + 1)
have rw : Coprime 1 n
Tactic: rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (hypothesis)
Goal:
n : ℕ
⊢ n + 1 ∣ n.centralBinom
have h_s : (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
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ n.centralBinom
have apply : n + 1 ∣ (2 * n + 1) * n.centralBinom
Tactic: apply h_s.dvd_of_dvd_mul_left
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * n.centralBinom
have apply : 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)
Tactic: apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Central (goal)
Goal:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)
have rw : (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom
Tactic: rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
⊢ primeFactorsList 0 = []
have rw : Eq (α := List ℕ) [] []
Tactic: rw [primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
⊢ primeFactorsList 1 = []
have rw : Eq (α := List ℕ) [] []
Tactic: rw [primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
⊢ Prime p
have this : (k + 2) / m < k + 2
Tactic: have : (k + 2) / m < (k + 2) := factors_lemma
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList
have 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
Tactic: rwa [primeFactorsList] at h
Cleared hypotheses: h, m, this
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ Prime p
have h₁ : 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)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
k : ℕ
h_1 : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ False
have this₁ : k + 2 = 0 * m
Tactic: have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
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
⊢ False
have this₁ : k + 2 = 0
Tactic: rw [zero_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2
have h₁ : (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
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).primeFactorsList.prod = k + 2
have rw : ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2
Tactic: rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]