awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ n.choose k = n.descFactorial k / k !

Tactic:
Nat.eq_div_of_mul_eq_right k.factorial_ne_zero (descFactorial_eq_factorial_mul_choose _ _).symm

Premises used: Nat.eq_div_of_mul_eq_right, Nat.factorial_ne_zero, Nat.descFactorial_eq_factorial_mul_choose, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ choose = fast_choose

Tactic:
funext (fun _ => funext (Nat.choose_eq_descFactorial_div_factorial _))

Premises used: funext, Nat.choose_eq_descFactorial_div_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))

Premises used: Nat.sub_pos_of_lt, Nat.div_le_self, LT.lt.trans_le, OfNat.ofNat, Nat.le_of_mul_le_mul_right
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
refine : n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))

Premises used: Nat.sub_pos_of_lt, Nat.div_le_self, LT.lt.trans_le, OfNat.ofNat, Nat.le_of_mul_le_mul_right
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
rw : n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)
⊢ n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)

Tactic:
rw [← choose_succ_right_eq]

Premises used: Nat.choose_succ_right_eq
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
h₁ : r + 1 ≤ n - r
⊢ n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)

Tactic:
apply Nat.mul_le_mul_left

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
h₁ : r * 2 < n
⊢ r + 1 ≤ n - r

Tactic:
rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]

Premises used: Nat.lt_sub_iff_add_lt, Nat.lt_iff_add_one_le, Nat.mul_two
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
⊢ r * 2 < n

Tactic:
lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

Premises used: Nat.div_mul_le_self, Nat.mul_lt_mul_of_pos_right, Nat.zero_lt_two, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
h : r < n / 2
⊢ r * 2 < n

Tactic:
exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

Premises used: Nat.div_mul_le_self, Nat.mul_lt_mul_of_pos_right, Nat.zero_lt_two, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n r : ℕ
⊢ n.choose (n / 2) ≤ n.choose (n / 2)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n r k : ℕ
hk : k < n / 2
ih : n.choose (k + 1) ≤ n.choose (n / 2)
⊢ n.choose k ≤ n.choose (n / 2)

Tactic:
(choose_le_succ_of_lt_half_left hk).trans ih

Premises used: Nat.choose_le_succ_of_lt_half_left, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n r k : ℕ
hk : k < n / 2
ih : n.choose (k + 1) ≤ n.choose (n / 2)
⊢ n.choose k ≤ n.choose (n / 2)

Tactic:
exact (choose_le_succ_of_lt_half_left hk).trans ih

Premises used: Nat.choose_le_succ_of_lt_half_left, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n r : ℕ
hr : r ≤ n / 2
self : n.choose (n / 2) ≤ n.choose (n / 2)
of_succ : ∀ (k : ℕ) (hk : k < n / 2) (ih : n.choose (k + 1) ≤ n.choose (n / 2)), n.choose k ≤ n.choose (n / 2)
⊢ n.choose r ≤ 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
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
inl : ∀ (b : r ≤ n), n.choose r ≤ n.choose (n / 2)
inr : ∀ (b : n < r), n.choose r ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_gt r n with b | b

Premises used: le_or_gt
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : r ≤ n
inl : ∀ (a : r ≤ n / 2), n.choose r ≤ n.choose (n / 2)
inl₁ : ∀ (h : n / 2 < r), n.choose r ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_gt r (n / 2) with a | h

Premises used: HDiv.hDiv, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
apply choose_le_middle_of_le_half_left a

Premises used: _private.0.Nat.choose_le_middle_of_le_half_left
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : r ≤ n
h : n / 2 < r
inl : n.choose (n - r) ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rw [← choose_symm b]

Premises used: Nat.choose_symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : r ≤ n
h : n / 2 < r
inl : n - r ≤ n / 2
⊢ n.choose (n - r) ≤ n.choose (n / 2)

Tactic:
apply choose_le_middle_of_le_half_left

Premises used: _private.0.Nat.choose_le_middle_of_le_half_left
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : n < r
inr : 0 ≤ n.choose (n / 2)
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rw [choose_eq_zero_of_lt b]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
r n : ℕ
b : n < r
⊢ 0 ≤ n.choose (n / 2)

Tactic:
apply zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a c : ℕ
zero : a.choose 0 ≤ a.succ.choose 0
succ : ∀ (n : ℕ), a.choose (n + 1) ≤ a.succ.choose (n + 1)
⊢ a.choose c ≤ a.succ.choose c

Tactic:
cases c
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a : ℕ
⊢ a.choose 0 ≤ a.succ.choose 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a n : ℕ
⊢ a.choose (n + 1) ≤ a.succ.choose (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a c : ℕ
⊢ a.choose c ≤ (a + 0).choose c

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a c b_n : ℕ
b_ih : a.choose c ≤ (a + b_n).choose c
⊢ a.choose c ≤ (a + (b_n + 1)).choose c

Tactic:
b_ih.trans (choose_le_succ (a + b_n) c)

Premises used: HAdd.hAdd, Nat.choose_le_succ, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a c b_n : ℕ
b_ih : a.choose c ≤ (a + b_n).choose c
⊢ a.choose c ≤ (a + (b_n + 1)).choose c

Tactic:
exact b_ih.trans (choose_le_succ (a + b_n) c)

Premises used: HAdd.hAdd, Nat.choose_le_succ, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a b c : ℕ
zero : a.choose c ≤ (a + 0).choose c
succ : ∀ (b_n : ℕ) (b_ih : a.choose c ≤ (a + b_n).choose c), a.choose c ≤ (a + (b_n + 1)).choose c
⊢ a.choose c ≤ (a + b).choose c

Tactic:
induction b with
  | zero => simp
  | succ b_n b_ih => exact b_ih.trans (choose_le_succ (a + b_n) c)

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
a b c : ℕ
h : a ≤ b
⊢ a.choose c ≤ b.choose c

Tactic:
Nat.add_sub_cancel' h ▸ choose_le_add a (b - a) c

Premises used: HSub.hSub, Eq.rec, Nat.choose_le_add, Nat.add_sub_cancel'
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
b : ℕ
⊢ Monotone (β := ℕ) fun (a : ℕ) ↦ a.choose b

Tactic:
fun _ _ => choose_le_choose b

Premises used: Monotone, Nat.choose_le_choose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
inl : ∀ (hk : k < n), n.choose k = 1 ↔ k = 0 ∨ n = k
inr : k.choose k = 1 ↔ k = 0 ∨ k = k
inr₁ : ∀ (hk : n < k), n.choose k = 1 ↔ k = 0 ∨ n = k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
rcases lt_trichotomy k n with hk | rfl | hk

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k < n
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
grind [k.choose_mono hk]

Premises used: Nat.choose_mono
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : multichoose 0 0 = 1
succ : ∀ (n : ℕ), (n + 1).multichoose 0 = 1
⊢ n.multichoose 0 = 1

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ multichoose 0 0 = 1

Tactic:
simp [multichoose]

Premises used: Nat.multichoose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ (n + 1).multichoose 0 = 1

Tactic:
simp [multichoose]

Premises used: Nat.multichoose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
simp [multichoose]

Premises used: Nat.multichoose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k

Tactic:
simp [multichoose]

Premises used: Nat.multichoose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ multichoose 1 0 = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
IH : multichoose 1 k = 1
⊢ multichoose 1 (k + 1) = 1

Tactic:
simp [multichoose_succ_succ 0 k, IH]

Premises used: Nat.multichoose_succ_succ, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
zero : multichoose 1 0 = 1
succ : ∀ (k : ℕ) (IH : multichoose 1 k = 1), multichoose 1 (k + 1) = 1
⊢ multichoose 1 k = 1

Tactic:
induction k with
  | zero => simp
  | succ k IH => simp [multichoose_succ_succ 0 k, IH]

Premises used: Nat.multichoose_succ_succ, Nat.zero, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ multichoose 2 0 = HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
IH : multichoose 2 k = k + 1
succ : multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1

Tactic:
rw [multichoose, IH]

Premises used: Nat.multichoose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1

Tactic:
simp [Nat.add_comm]

Premises used: Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
zero : multichoose 2 0 = HAdd.hAdd (α := ℕ) 0 1
succ : ∀ (k : ℕ) (IH : multichoose 2 k = k + 1), multichoose 2 (k + 1) = k + 1 + 1
⊢ multichoose 2 k = k + 1

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [multichoose, IH]; simp [Nat.add_comm]

Premises used: Nat.zero, Nat.succ, Nat.multichoose, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ multichoose 0 1 = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
IH : n.multichoose 1 = n
⊢ (n + 1).multichoose 1 = n + 1

Tactic:
simp [multichoose_succ_succ n 0, IH]

Premises used: Nat.multichoose_succ_succ, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : multichoose 0 1 = 0
succ : ∀ (n : ℕ) (IH : n.multichoose 1 = n), (n + 1).multichoose 1 = n + 1
⊢ n.multichoose 1 = n

Tactic:
induction n with
  | zero => simp
  | succ n IH => simp [multichoose_succ_succ n 0, IH]

Premises used: Nat.multichoose_succ_succ, Nat.zero, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
x : ℕ
⊢ x.multichoose 0 = (x + 0 - 1).choose 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
⊢ multichoose 0 (k + 1) = (0 + (k + 1) - 1).choose (k + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ 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 _) _
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ 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 _) _
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
this_1 : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
rw : (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
      Nat.choose_succ_succ]

Premises used: Nat.succ_add_sub_one, Nat.choose_succ_succ, Nat.multichoose_succ_succ, Nat.add_assoc, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
this_1 : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ

Tactic:
simp [multichoose_eq n (k + 1), multichoose_eq (n + 1) k]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Bounds
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
rw₁ : LT.lt.{u_1} (α := α) 0 (↑r ! : α)
⊢ (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r / (↑r ! : α)

Tactic:
rw [le_div_iff₀']

Premises used: le_div_iff₀'
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
norm_cast : r ! * n.choose r ≤ n ^ r
⊢ HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α) ≤ HPow.hPow (α := α) (↑n : α) r

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
rw : n.descFactorial r ≤ n ^ r
⊢ r ! * n.choose r ≤ n ^ r

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Premises used: Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r

Tactic:
n.descFactorial_le_pow r

Premises used: Nat.descFactorial_le_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r

Tactic:
exact n.descFactorial_le_pow r

Premises used: Nat.descFactorial_le_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ LT.lt.{u_1} (α := α) 0 (↑r ! : α)

Tactic:
mod_cast r.factorial_pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, Nat.factorial, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Nat.factorial_pos, Eq.trans
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ LT.lt.{u_1} (α := α) 0 (↑r ! : α)

Tactic:
exact mod_cast r.factorial_pos

Premises used: Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
rw : HMul.hMul (α := α) (↑k ! : α) (↑(n.choose k) : α) < HPow.hPow (α := α) (↑n : α) k
⊢ (↑(n.choose k) : α) < HPow.hPow (α := α) (↑n : α) k / (↑k ! : α)

Tactic:
rw [lt_div_iff₀' (mod_cast k.factorial_pos)]

Premises used: lt_div_iff₀'
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
norm_cast : k ! * n.choose k < n ^ k
⊢ HMul.hMul (α := α) (↑k ! : α) (↑(n.choose k) : α) < HPow.hPow (α := α) (↑n : α) k

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
rw : n.descFactorial k < n ^ k
⊢ k ! * n.choose k < n ^ k

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Premises used: Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.descFactorial k < n ^ k

Tactic:
descFactorial_lt_pow hn hk

Premises used: Nat.descFactorial_lt_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.descFactorial k < n ^ k

Tactic:
exact descFactorial_lt_pow hn hk

Premises used: Nat.descFactorial_lt_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
rw : n.descFactorial k / k ! ≤ n.descFactorial k
⊢ n.choose k ≤ n.descFactorial k

Tactic:
rw [choose_eq_descFactorial_div_factorial]

Premises used: Nat.choose_eq_descFactorial_div_factorial
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
⊢ n.descFactorial k / k ! ≤ n.descFactorial k

Tactic:
Nat.div_le_self _ _

Premises used: Nat.div_le_self
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
⊢ n.descFactorial k / k ! ≤ n.descFactorial k

Tactic:
exact Nat.div_le_self _ _

Premises used: Nat.div_le_self
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
rw : n.descFactorial k / k ! < n.descFactorial k
⊢ n.choose k < n.descFactorial k

Tactic:
rw [choose_eq_descFactorial_div_factorial]

Premises used: Nat.choose_eq_descFactorial_div_factorial
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ 0 < n.descFactorial k

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ 1 < k !

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.descFactorial k / k ! < n.descFactorial k

Tactic:
exact Nat.div_lt_self (by simpa) (by simpa)

Premises used: Nat.div_lt_self
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
⊢ n.choose k ≤ n ^ k

Tactic:
(choose_le_descFactorial n k).trans (descFactorial_le_pow n k)

Premises used: Nat.descFactorial_le_pow, LE.le.trans, Nat.choose_le_descFactorial
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.choose k < n ^ k

Tactic:
(choose_le_descFactorial n k).trans_lt (descFactorial_lt_pow hn hk)

Premises used: Nat.descFactorial_lt_pow, LE.le.trans_lt, Nat.choose_le_descFactorial
-- Module: Mathlib.Data.Nat.Choose.Bounds
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) : α)
rw₁ : LT.lt.{u_1} (α := α) 0 (↑r ! : α)
⊢ HPow.hPow (α := α) (↑(n + 1 - r) : α) r / (↑r ! : α) ≤ (↑(n.choose r) : α)

Tactic:
rw [div_le_iff₀']

Premises used: div_le_iff₀'
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
norm_cast : (n + 1 - r) ^ r ≤ r ! * n.choose r
⊢ HPow.hPow (α := α) (↑(n + 1 - r) : α) r ≤ HMul.hMul (α := α) (↑r ! : α) (↑(n.choose r) : α)

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
rw : (n + 1 - r) ^ r ≤ n.descFactorial r
⊢ (n + 1 - r) ^ r ≤ r ! * n.choose r

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Premises used: Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r

Tactic:
n.pow_sub_le_descFactorial r

Premises used: Nat.pow_sub_le_descFactorial
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r

Tactic:
exact n.pow_sub_le_descFactorial r

Premises used: Nat.pow_sub_le_descFactorial
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
pos : ∀ (lt : n + 1 < k), (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
neg : ∀ (lt : ¬n + 1 < k), (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
by_cases lt : n + 1 < k
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
simp [choose_eq_zero_of_lt lt]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Bounds
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
neg₁ :
  ∀ (n : ℕ) (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < n + 1),
    (HAdd.hAdd (α := ℕ) 0 1).choose (n + 1) ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ (HAdd.hAdd (α := ℕ) 0 1).choose k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
cases k
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
lt : ¬HAdd.hAdd (α := ℕ) 0 1 < 0
⊢ (HAdd.hAdd (α := ℕ) 0 1).choose 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n : ℕ
lt : ¬HAdd.hAdd (α := ℕ) 0 1 < n + 1
⊢ (HAdd.hAdd (α := ℕ) 0 1).choose (n + 1) ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
k n : ℕ
lt : ¬n + 1 + 1 < k
neg : ∀ (lt : ¬n + 1 + 1 < 0), (n + 1 + 1).choose 0 ≤ HPow.hPow (α := ℕ) 2 (n + 1)
neg₁ : ∀ (k : ℕ) (lt : ¬n + 1 + 1 < k + 1), (n + 1 + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 (n + 1)
⊢ (n + 1 + 1).choose k ≤ HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
rcases k with - | k
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
Nat.one_le_two_pow

Premises used: Nat.one_le_two_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
exact Nat.one_le_two_pow

Premises used: Nat.one_le_two_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
neg : (n + 1).choose k + (n + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
⊢ (n + 1 + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
rw [choose_succ_succ', two_pow_succ]

Premises used: Nat.two_pow_succ, Nat.choose_succ_succ'
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n

Tactic:
Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

Premises used: HAdd.hAdd, Nat.add_le_add, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n

Tactic:
exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

Premises used: HAdd.hAdd, Nat.add_le_add, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
lt : ¬n + 1 < k
neg : ∀ (lt : ¬HAdd.hAdd (α := ℕ) 0 1 < k), (HAdd.hAdd (α := ℕ) 0 1).choose k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
neg₁ : ∀ (n : ℕ) (lt : ¬n + 1 + 1 < k), (n + 1 + 1).choose k ≤ HPow.hPow (α := ℕ) 2 (n + 1)
⊢ (n + 1).choose k ≤ HPow.hPow (α := ℕ) 2 n

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))

Premises used: Nat.two_pow_succ, Nat.one_le_two_pow, HAdd.hAdd, Nat.add_le_add, Nat.choose_succ_succ', Nat.zero, OfNat.ofNat, Nat.succ, Nat.choose_zero_right
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
p : 0 < n
⊢ n.choose k < HPow.hPow (α := ℕ) 2 n

Tactic:
lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)

Premises used: lt_of_le_of_lt, Nat.two_pow_pred_lt_two_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
p : 0 < n
refine : n.choose k ≤ HPow.hPow (α := ℕ) 2 (n - 1)
⊢ n.choose k < HPow.hPow (α := ℕ) 2 n

Tactic:
refine lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)

Premises used: lt_of_le_of_lt, Nat.two_pow_pred_lt_two_pow
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
p : 0 < n
rw : (n - succ 0 + succ 0).choose k ≤ HPow.hPow (α := ℕ) 2 (n - succ 0 + succ 0 - 1)
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
rw [← Nat.sub_add_cancel p]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ HPow.hPow (α := ℕ) 2 (n - succ 0 + succ 0 - 1)

Tactic:
choose_succ_le_two_pow (n - 1) k

Premises used: Nat.choose_succ_le_two_pow, HSub.hSub, OfNat.ofNat, Nat.pred
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ HPow.hPow (α := ℕ) 2 (n - succ 0 + succ 0 - 1)

Tactic:
exact choose_succ_le_two_pow (n - 1) k

Premises used: Nat.choose_succ_le_two_pow, HSub.hSub, OfNat.ofNat