awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
zero : 1 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
⊢ ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
have zero₁ : 1 = 0! * 1
Tactic: rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
zero : 1 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
zero₁ : 1 = 0! * 1
⊢ ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
have zero₂ : 1 = HMul.hMul (α := ℕ) 1 1
Tactic: rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k n : ℕ
⊢ (n + 1).ascFactorial k = k ! * (n + 1 + k - 1).choose k
have succ : k ! * (n + k).choose k = k ! * (n + 1 + k - 1).choose k
Tactic: rw [ascFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ (n + k).choose k = (n + 1).ascFactorial k / k !
have apply : k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)
Tactic: apply Nat.mul_left_cancel k.factorial_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)
have rw : (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)
Tactic: rw [← ascFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ n.descFactorial k = k ! * n.choose k
have inl : ∀ (h : n < k), n.descFactorial k = k ! * n.choose k
Tactic: obtain h | h := Nat.lt_or_ge n k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
inl : ∀ (h : n < k), n.descFactorial k = k ! * n.choose k
⊢ n.descFactorial k = k ! * n.choose k
have inr : ∀ (h : n ≥ k), n.descFactorial k = k ! * n.choose k
Tactic: obtain h | h := Nat.lt_or_ge n k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n < k
⊢ n.descFactorial k = k ! * n.choose k
have inl : 0 = k ! * n.choose k
Tactic: rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n < k
inl : 0 = k ! * n.choose k
⊢ n.descFactorial k = k ! * n.choose k
have inl₁ : 0 = k ! * 0
Tactic: rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n < k
inl : 0 = k ! * n.choose k
inl₁ : 0 = k ! * 0
⊢ n.descFactorial k = k ! * n.choose k
have inl₂ : Eq (α := ℕ) 0 0
Tactic: rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = k ! * n.choose k
have inr : n.descFactorial k = n.choose k * k !
Tactic: rw [Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !
have inr : n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!
Tactic: apply Nat.mul_right_cancel (n - k).factorial_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!
have inr : n.descFactorial k * (n - k)! = n !
Tactic: rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n ≥ k
inr : n.descFactorial k * (n - k)! = n !
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!
have inr₁ : n.descFactorial k * (n - k)! = (n - k)! * n.descFactorial k
Tactic: rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
h : n ≥ k
inr : n.descFactorial k * (n - k)! = n !
inr₁ : n.descFactorial k * (n - k)! = (n - k)! * n.descFactorial k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!
have inr₂ : (n - k)! * n.descFactorial k = (n - k)! * n.descFactorial k
Tactic: rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)
have refine : n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)
Tactic: refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
h : r < n / 2
⊢ n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)
have rw : n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)
Tactic: rw [← choose_succ_right_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
h : r < n / 2
⊢ n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)
have h₁ : r + 1 ≤ n - r
Tactic: apply Nat.mul_le_mul_left
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r
have h₁ : r * 2 < n
Tactic: rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n r : ℕ
hr : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)
have self : n.choose (n / 2) ≤ n.choose (n / 2)
Tactic: induction hr using decreasingInduction with
  | self => rfl
  | of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n r : ℕ
hr : r ≤ n / 2
self : n.choose (n / 2) ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)
have of_succ : ∀ (k : ℕ) (hk : k < n / 2) (ih : n.choose (k + 1) ≤ n.choose (n / 2)), n.choose k ≤ n.choose (n / 2)
Tactic: induction hr using decreasingInduction with
  | self => rfl
  | of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
⊢ n.choose r ≤ n.choose (n / 2)
have inl : ∀ (b : r ≤ n), n.choose r ≤ n.choose (n / 2)
Tactic: rcases le_or_gt r n with b | b
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
inl : ∀ (b : r ≤ n), n.choose r ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)
have inr : ∀ (b : n < r), n.choose r ≤ n.choose (n / 2)
Tactic: rcases le_or_gt r n with b | b
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
b : r ≤ n
⊢ n.choose r ≤ n.choose (n / 2)
have inl : ∀ (a : r ≤ n / 2), n.choose r ≤ n.choose (n / 2)
Tactic: rcases le_or_gt r (n / 2) with a | h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
b : r ≤ n
inl : ∀ (a : r ≤ n / 2), n.choose r ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)
have inl₁ : ∀ (h : n / 2 < r), n.choose r ≤ n.choose (n / 2)
Tactic: rcases le_or_gt r (n / 2) with a | h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose r ≤ n.choose (n / 2)
have inl : n.choose (n - r) ≤ n.choose (n / 2)
Tactic: rw [← choose_symm b]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose (n - r) ≤ n.choose (n / 2)
have inl : n - r ≤ n / 2
Tactic: apply choose_le_middle_of_le_half_left
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
r n : ℕ
b : n < r
⊢ n.choose r ≤ n.choose (n / 2)
have inr : 0 ≤ n.choose (n / 2)
Tactic: rw [choose_eq_zero_of_lt b]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
a c : ℕ
⊢ a.choose c ≤ a.succ.choose c
have zero : a.choose 0 ≤ a.succ.choose 0
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
a c : ℕ
zero : a.choose 0 ≤ a.succ.choose 0
⊢ a.choose c ≤ a.succ.choose c
have succ : ∀ (n : ℕ), a.choose (n + 1) ≤ a.succ.choose (n + 1)
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
a b c : ℕ
⊢ a.choose c ≤ (a + b).choose c
have zero : a.choose c ≤ (a + 0).choose c
Tactic: induction b with
  | zero => simp
  | succ b_n b_ih => exact b_ih.trans (choose_le_succ (a + b_n) c)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
a b c : ℕ
zero : a.choose c ≤ (a + 0).choose c
⊢ a.choose c ≤ (a + b).choose c
have succ : ∀ (b_n : ℕ) (b_ih : a.choose c ≤ (a + b_n).choose c), a.choose c ≤ (a + (b_n + 1)).choose c
Tactic: induction b with
  | zero => simp
  | succ b_n b_ih => exact b_ih.trans (choose_le_succ (a + b_n) c)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
have inl : ∀ (hk : k < n), n.choose k = 1 ↔ k = 0 ∨ n = k
Tactic: rcases lt_trichotomy k n with hk | rfl | hk
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
inl : ∀ (hk : k < n), n.choose k = 1 ↔ k = 0 ∨ n = k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
have inr : k.choose k = 1 ↔ k = 0 ∨ k = k
Tactic: rcases lt_trichotomy k n with hk | rfl | hk
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
inl : ∀ (hk : k < n), n.choose k = 1 ↔ k = 0 ∨ n = k
inr : k.choose k = 1 ↔ k = 0 ∨ k = k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
have inr₁ : ∀ (hk : n < k), n.choose k = 1 ↔ k = 0 ∨ n = k
Tactic: rcases lt_trichotomy k n with hk | rfl | hk
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n.multichoose 0 = 1
have zero : multichoose 0 0 = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : multichoose 0 0 = 1
⊢ n.multichoose 0 = 1
have succ : ∀ (n : ℕ), (n + 1).multichoose 0 = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
⊢ multichoose 1 k = 1
have zero : multichoose 1 0 = 1
Tactic: induction k with
  | zero => simp
  | succ k IH => simp [multichoose_succ_succ 0 k, IH]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
zero : multichoose 1 0 = 1
⊢ multichoose 1 k = 1
have succ : ∀ (k : ℕ) (IH : multichoose 1 k = 1), multichoose 1 (k + 1) = 1
Tactic: induction k with
  | zero => simp
  | succ k IH => simp [multichoose_succ_succ 0 k, IH]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1
have succ : multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
Tactic: rw [multichoose, IH]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
⊢ multichoose 2 k = k + 1
have zero : multichoose 2 0 = HAdd.hAdd (α := ℕ) 0 1
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [multichoose, IH]; simp [Nat.add_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
zero : multichoose 2 0 = HAdd.hAdd (α := ℕ) 0 1
⊢ multichoose 2 k = k + 1
have succ : ∀ (k : ℕ) (IH : multichoose 2 k = k + 1), multichoose 2 (k + 1) = k + 1 + 1
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [multichoose, IH]; simp [Nat.add_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n.multichoose 1 = n
have zero : multichoose 0 1 = 0
Tactic: induction n with
  | zero => simp
  | succ n IH => simp [multichoose_succ_succ n 0, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : multichoose 0 1 = 0
⊢ n.multichoose 1 = n
have succ : ∀ (n : ℕ) (IH : n.multichoose 1 = n), (n + 1).multichoose 1 = n + 1
Tactic: induction n with
  | zero => simp
  | succ n IH => simp [multichoose_succ_succ n 0, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k : ℕ
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
have this : n + (k + 1) < n + 1 + (k + 1)
Tactic: have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
have this₁ : n + 1 + k < n + 1 + (k + 1)
Tactic: have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
this_1 : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
have rw : (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ
Tactic: rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
      Nat.choose_succ_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r / (↑r ! : α)
have rw : HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r
Tactic: rw [le_div_iff₀']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
rw : HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r
⊢ (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r / (↑r ! : α)
have rw₁ : LT.lt.{u_1} (α := α) 0 (↑r ! : α)
Tactic: rw [le_div_iff₀']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r
have norm_cast : r ! * n.choose r ≤ n ^ r
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ r ! * n.choose r ≤ n ^ r
have rw : n.descFactorial r ≤ n ^ r
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ (↑(n.choose k) : α) < HPow.hPow (α := α) (↑n : α) k / (↑k ! : α)
have rw : HMul.hMul (α := α) (↑k ! : α) (↑(n.choose k) : α) < HPow.hPow (α := α) (↑n : α) k
Tactic: rw [lt_div_iff₀' (mod_cast k.factorial_pos)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ HMul.hMul (α := α) (↑k ! : α) (↑(n.choose k) : α) < HPow.hPow (α := α) (↑n : α) k
have norm_cast : k ! * n.choose k < n ^ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ k ! * n.choose k < n ^ k
have rw : n.descFactorial k < n ^ k
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
⊢ n.choose k ≤ n.descFactorial k
have rw : n.descFactorial k / k ! ≤ n.descFactorial k
Tactic: rw [choose_eq_descFactorial_div_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.choose k < n.descFactorial k
have rw : n.descFactorial k / k ! < n.descFactorial k
Tactic: rw [choose_eq_descFactorial_div_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ HPow.hPow (α := α) (↑(n + 1 - r) : α) r / (↑r ! : α) ≤ (↑(n.choose r) : α)
have rw : HPow.hPow (α := α) (↑(n + 1 - r) : α) r ≤ HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α)
Tactic: rw [div_le_iff₀']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
rw : HPow.hPow (α := α) (↑(n + 1 - r) : α) r ≤ HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α)
⊢ HPow.hPow (α := α) (↑(n + 1 - r) : α) r / (↑r ! : α) ≤ (↑(n.choose r) : α)
have rw₁ : LT.lt.{u_1} (α := α) 0 (↑r ! : α)
Tactic: rw [div_le_iff₀']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ HPow.hPow (α := α) (↑(n + 1 - r) : α) r ≤ HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α)
have norm_cast : (n + 1 - r) ^ r ≤ r ! * n.choose r
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * n.choose r
have rw : (n + 1 - r) ^ r ≤ n.descFactorial r
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
have pos : ∀ (lt : n + 1 < k), (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
Tactic: by_cases lt : n + 1 < k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
pos : ∀ (lt : n + 1 < k), (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
have neg : ∀ (lt : ¬n + 1 < k), (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
Tactic: by_cases lt : n + 1 < k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
k : ℕ
lt : ¬HAdd.hAdd (α := ℕ) 0 1 < k
⊢ (HAdd.hAdd (α := ℕ) 0 1).choose k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
have neg : ∀ (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < 0), (HAdd.hAdd (α := ℕ) 0 1).choose 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: cases k
Cleared hypotheses: k, lt
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
k : ℕ
lt : ¬HAdd.hAdd (α := ℕ) 0 1 < k
neg : ∀ (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < 0), (HAdd.hAdd (α := ℕ) 0 1).choose 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ (HAdd.hAdd (α := ℕ) 0 1).choose k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
have neg₁ : ∀ (n : ℕ) (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < n + 1),
  (HAdd.hAdd (α := ℕ) 0 1).choose (n + 1) ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: cases k
Cleared hypotheses: k, lt
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
k n : ℕ
lt : ¬n + 1 + 1 < k
⊢ (n + 1 + 1).choose k ≤ HPow.hPow (α := ℕ) 2 (n + 1)
have neg : ∀ (lt : ¬n + 1 + 1 < 0), (n + 1 + 1).choose 0 ≤ HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: rcases k with - | k
Cleared hypotheses: k, lt
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
k n : ℕ
lt : ¬n + 1 + 1 < k
neg : ∀ (lt : ¬n + 1 + 1 < 0), (n + 1 + 1).choose 0 ≤ HPow.hPow (α := ℕ) 2 (n + 1)
⊢ (n + 1 + 1).choose k ≤ HPow.hPow (α := ℕ) 2 (n + 1)
have neg₁ : ∀ (k : ℕ) (lt : ¬n + 1 + 1 < k + 1), (n + 1 + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: rcases k with - | k
Cleared hypotheses: k, lt
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 (n + 1)
have neg : (n + 1).choose k + (n + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
Tactic: rw [choose_succ_succ', two_pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
lt : ¬n + 1 < k
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
have neg : ∀ (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < k), (HAdd.hAdd (α := ℕ) 0 1).choose k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: cases n with
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))
Cleared hypotheses: n, lt
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
lt : ¬n + 1 < k
neg : ∀ (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < k), (HAdd.hAdd (α := ℕ) 0 1).choose k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
have neg₁ : ∀ (n : ℕ) (lt : ¬n + 1 + 1 < k), (n + 1 + 1).choose k ≤ HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: cases n with
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))
Cleared hypotheses: n, lt
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
p : 0 < n
⊢ n.choose k < HPow.hPow (α := ℕ) 2 n
have refine : n.choose k ≤ HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: refine lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
p : 0 < n
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 (n - 1)
have rw : (n - succ 0 + succ 0).choose k ≤ HPow.hPow (α := ℕ) 2 (n - succ 0 + succ 0 - 1)
Tactic: rw [← Nat.sub_add_cancel p]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 n
have inl : choose 0 k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: obtain (rfl | hn) := eq_zero_or_pos n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
n k : ℕ
inl : choose 0 k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 n
have inr : ∀ (hn : n > 0), n.choose k ≤ HPow.hPow (α := ℕ) 2 n
Tactic: obtain (rfl | hn) := eq_zero_or_pos n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
k : ℕ
⊢ choose 0 k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
have inl : choose 0 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Bounds (goal)
Goal:
k : ℕ
inl : choose 0 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ choose 0 k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
have inl₁ : ∀ (n : ℕ), choose 0 (n + 1) ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (hypothesis)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
⊢ (↑(b.choose a) : K) = (↑b ! : K) / HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K)
have this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0
Tactic: have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_pos _).ne'
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0
⊢ (↑(b.choose a) : K) = (↑b ! : K) / HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K)
have rw : (↑(b.choose a) : K) * HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K) = (↑b ! : K)
Tactic: rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0
⊢ (↑(b.choose a) : K) * HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K) = (↑b ! : K)
have rw_mod_cast : ∀ (this : ∀ {n : ℕ}, ¬n ! = 0), b.choose a * (a ! * (b - a)!) = b !
Tactic: rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Cast (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  ∀ (this : ∀ {n : ℕ}, ¬n ! = 0), b.choose a * (a ! * (b - a)!) = b !
⊢ (↑(b.choose a) : K) * HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K) = (↑b ! : K)
have rw_mod_cast₆ : ∀ (this : ∀ {n : ℕ}, ¬n ! = 0), b.choose a * a ! * (b - a)! = b !
Tactic: rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]
Cleared hypotheses: this