awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
hs : ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → s i ≠ 0
pp :
  Set.Pairwise {x : ι | Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) x}
    (Coprime on s)
⊢ ∀ i ∈ l, s i ≠ 0

Tactic:
simpa using hs
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
hs : ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → s i ≠ 0
pp :
  Set.Pairwise {x : ι | Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) x}
    (Coprime on s)
⊢ (↑(Quotient.recOn (motive := fun (x : Multiset ι) ↦
          x.Nodup →
            (∀ i ∈ x, s i ≠ 0) →
              Set.Pairwise {x_1 : ι | x_1 ∈ x} (Coprime on s) → { k : ℕ // ∀ i ∈ x, k ≡ a i [MOD s i] })
          (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
          (fun (l : List ι) (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0)
              (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
            chineseRemainderOfList a s l ⋯)
          ⋯ nod hs pp) :
      ℕ) <
    (Multiset.map s (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod

Tactic:
simpa using chineseRemainderOfList_lt_prod a s l
    (List.Nodup.pairwise_of_forall_ne nod pp) (by simpa using hs)

Premises used: List.Nodup.pairwise_of_forall_ne, Nat.chineseRemainderOfList_lt_prod
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t : Set ι).Pairwise (Coprime on s)
⊢ ∀ i ∈ t.val, s i ≠ 0

Tactic:
simpa using hs
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t : Set ι).Pairwise (Coprime on s)
⊢ Set.Pairwise {x : ι | x ∈ t.val} (Coprime on s)

Tactic:
simpa using pp
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t : Set ι).Pairwise (Coprime on s)
⊢ { k : ℕ // ∀ i ∈ t, k ≡ a i [MOD s i] }

Tactic:
simpa using chineseRemainderOfMultiset a s t.nodup (by simpa using hs) (by simpa using pp)

Premises used: Nat.chineseRemainderOfMultiset, Finset.nodup
-- Module: Mathlib.Data.Nat.ChineseRemainder
Goal:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t : Set ι).Pairwise (Coprime on s)
⊢ (↑(chineseRemainderOfFinset a s t hs pp) : ℕ) < ∏ i ∈ t, s i

Tactic:
simpa [chineseRemainderOfFinset] using
    chineseRemainderOfMultiset_lt_prod a s t.nodup (by simpa using hs) (by simpa using pp)

Premises used: Finset.nodup, Nat.chineseRemainderOfMultiset_lt_prod, Nat.chineseRemainderOfFinset
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : choose 0 0 = 1
succ : ∀ (n : ℕ), (n + 1).choose 0 = 1
⊢ n.choose 0 = 1

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

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

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
⊢ choose 0 k.succ = 0

Tactic:
rfl

Premises used: Nat.choose, rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ n.succ.choose k.succ = n.choose k + n.choose k.succ

Tactic:
rfl

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

Tactic:
rfl

Premises used: Nat.choose, rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : 0 < k
⊢ ∃ (l : ℕ), k = l + 1

Tactic:
Nat.exists_eq_add_of_le' hk

Premises used: Nat.exists_eq_add_of_le'
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : 0 < k
obtain : ∀ (l : ℕ) (hk : 0 < l + 1), (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)
⊢ (n + 1).choose k = n.choose (k - 1) + n.choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n l : ℕ
hk : 0 < l + 1
⊢ (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hn : 0 < n
⊢ ∃ (l : ℕ), n = l + 1

Tactic:
Nat.exists_eq_add_of_le' hn

Premises used: Nat.exists_eq_add_of_le'
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hn : 0 < n
obtain : ∀ (l : ℕ) (hn : 0 < l + 1), (l + 1).choose (k + 1) = (l + 1 - 1).choose k + (l + 1 - 1).choose (k + 1)
⊢ n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, n = l + 1 := Nat.exists_eq_add_of_le' hn

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k l : ℕ
hn : 0 < l + 1
⊢ (l + 1).choose (k + 1) = (l + 1 - 1).choose k + (l + 1 - 1).choose (k + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ ∃ (l : ℕ), k = l + 1

Tactic:
Nat.exists_eq_add_of_le' hk

Premises used: Nat.exists_eq_add_of_le'
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hn : 0 < n
hk : 0 < k
obtain : ∀ (l : ℕ) (hk : 0 < l + 1), n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
⊢ n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
rw : (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
rw₁ rw₂ : (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose l + (n - 1).choose (l + 1)
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)

Tactic:
rw [choose_succ_right _ _ hn, Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Nat.choose_succ_right
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : n + 1 < k + 1
⊢ n < k

Tactic:
have hnk : n < k := lt_of_succ_lt_succ hk
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ n < k + 1

Tactic:
have hnk1 : n < k + 1 := lt_of_succ_lt hk
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
rw : n.choose k + n.choose k.succ = 0
rw₁ : 0 + n.choose k.succ = 0
rw₂ rw₃ : HAdd.hAdd (α := ℕ) 0 0 = 0
⊢ (n + 1).choose (k + 1) = 0

Tactic:
rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]

Premises used: Nat.choose_succ_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : choose 0 0 = 1
succ : ∀ (n : ℕ), n.choose n = 1 → (n + 1).choose (n + 1) = 1
⊢ n.choose n = 1

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

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

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ n.choose n.succ = 0

Tactic:
choose_eq_zero_of_lt (lt_succ_self _)

Premises used: Nat.lt_succ_self, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : choose 0 1 = 0
succ : ∀ (n : ℕ), n.choose 1 = n → (n + 1).choose 1 = n + 1
⊢ n.choose 1 = n

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

Tactic:
simp [*, choose, Nat.add_comm]

Premises used: Nat.choose, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
h : n.choose 1 = n
⊢ (n + 1).choose 1 = n + 1

Tactic:
simp [*, choose, Nat.add_comm]

Premises used: Nat.choose, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
rw : n * (n + 1) / 2 = n * (n - 1 + 2) / 2
H : LT.lt (α := ℕ) 0 2
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]

Premises used: Nat.mul_comm, Nat.add_sub_cancel, Nat.add_mul_div_left, OfNat.ofNat, Nat.mul_add
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : 0 * HAdd.hAdd (α := ℕ) 0 1 / 2 = 0 * (HSub.hSub (α := ℕ) 0 1 + 2) / 2
succ : ∀ (n : ℕ), (n + 1) * (n + 1 + 1) / 2 = (n + 1) * (n + 1 - 1 + 2) / 2
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ 0 * HAdd.hAdd (α := ℕ) 0 1 / 2 = 0 * (HSub.hSub (α := ℕ) 0 1 + 2) / 2

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ (n + 1) * (n + 1 + 1) / 2 = (n + 1) * (n + 1 - 1 + 2) / 2

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) 0 2

Tactic:
apply zero_lt_succ

Premises used: Nat.zero_lt_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ choose 0 2 = 0 * HSub.hSub (α := ℕ) 0 1 / 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
succ : n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2

Tactic:
rw [triangle_succ n, choose, ih]

Premises used: Nat.triangle_succ, Nat.choose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
simp [Nat.add_comm]

Premises used: Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
zero : choose 0 2 = 0 * HSub.hSub (α := ℕ) 0 1 / 2
succ : ∀ (n : ℕ) (ih : n.choose 2 = n * (n - 1) / 2), (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2
⊢ n.choose 2 = n * (n - 1) / 2

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]

Premises used: Nat.triangle_succ, Nat.choose, Nat.zero, Nat.succ, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
x : ℕ
hk : x ≤ 0
rw : 0 < choose 0 0
⊢ 0 < choose 0 x

Tactic:
rw [Nat.eq_zero_of_le_zero hk]

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
x : ℕ
hk : x ≤ 0
⊢ 0 < choose 0 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
h : 0 ≤ n + 1
⊢ 0 < (n + 1).choose 0

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

Tactic:
⟨fun h => lt_of_not_ge (mt Nat.choose_pos h.symm.not_lt), Nat.choose_eq_zero_of_lt⟩

Premises used: lt_of_not_ge, mt, Nat.choose_pos, Nat.choose_eq_zero_of_lt, Iff.intro, Eq.not_lt, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
⊢ ¬n.choose k ≠ 0 ↔ ¬k ≤ n

Tactic:
simp [choose_eq_zero_iff]

Premises used: Nat.choose_eq_zero_iff
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
h : k ≤ n
⊢ n.choose k ≠ 0

Tactic:
(choose_pos h).ne'

Premises used: LT.lt.ne', Nat.choose_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ HAdd.hAdd (α := ℕ) 0 1 * choose 0 0 =
    (HAdd.hAdd (α := ℕ) 0 1).choose (HAdd.hAdd (α := ℕ) 0 1) * HAdd.hAdd (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
k : ℕ
⊢ HAdd.hAdd (α := ℕ) 0 1 * choose 0 (k + 1) = (HAdd.hAdd (α := ℕ) 0 1).choose (k + 1 + 1) * (k + 1 + 1)

Tactic:
simp [choose]

Premises used: Nat.choose
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
⊢ (n + 1 + 1) * (n + 1).choose 0 = (n + 1 + 1).choose (HAdd.hAdd (α := ℕ) 0 1) * HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp [choose, mul_succ, Nat.add_comm]

Premises used: Nat.mul_succ, Nat.choose, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
rw : (n + 1 + 1) * (n + 1).choose (k + 1) = ((n + 1).choose (k + 1) + (n + 1).choose (k + 1 + 1)) * (k + 1 + 1)
rw₁ :
  (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1).choose (k + 1 + 1) * (k + 1 + 1)
rw₂ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1) * n.choose (k + 1)
rw₃ :
  (n + 1 + 1) * (n + 1).choose (k + 1) =
    (n + 1).choose (k + 1) * (k + 1) + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
rw₄ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
rw₅ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1) * n.choose (k + 1) + (n + 1).choose (k + 1)
rw₆ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n.choose k + n.choose (k + 1)) + (n + 1).choose (k + 1)
rw₇ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n + 1).choose (k + 1) + (n + 1).choose (k + 1)
rw₈ rw₉ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1) * (n + 1).choose (k + 1)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)

Tactic:
rw [choose_succ_succ' (n + 1) (k + 1), Nat.add_mul _ _ (k + 1 + 1), ← add_one_mul_choose_eq n,
      mul_add_one, ← add_one_mul_choose_eq n, Nat.add_right_comm _ _ (_ * _), ← Nat.mul_add,
      ← choose_succ_succ', ← add_one_mul]

Premises used: HMul.hMul, HAdd.hAdd, Nat.mul_add_one, Nat.choose_succ_succ', OfNat.ofNat, Nat.mul_add, Nat.add_one_mul, Nat.add_mul, Nat.add_right_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
⊢ ∀ (n k : ℕ), n.succ * n.choose k = n.succ.choose k.succ * k.succ

Tactic:
add_one_mul_choose_eq

Premises used: Nat.add_one_mul_choose_eq
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
x : ℕ
hk : x ≤ 0
⊢ choose 0 x * x ! * (0 - x)! = 0!

Tactic:
simp [Nat.eq_zero_of_le_zero hk]

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n : ℕ
h : 0 ≤ n + 1
⊢ (n + 1).choose 0 * 0! * (n + 1 - 0)! = (n + 1)!

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
inl : ∀ (hk₁ : k.succ < n + 1), (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
inr : ∀ (hk₁ : k.succ = n + 1), (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
rcases lt_or_eq_of_le hk with hk₁ | hk₁

Premises used: lt_or_eq_of_le
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
rw : n.choose k * k.succ ! * (n - k)! = (k + 1) * (n.choose k * k ! * (n - k)!)
⊢ n.choose k * k.succ ! * (n - k)! = (k + 1) * n !

Tactic:
rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]

Premises used: Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
⊢ n.choose k * k.succ ! * (n - k)! = (k + 1) * (n.choose k * k ! * (n - k)!)

Tactic:
simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

Premises used: Nat.mul_left_comm, Nat.factorial_succ, Nat.mul_comm, Nat.mul_assoc
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
⊢ n.choose k * k.succ ! * (n - k)! = (k + 1) * n !

Tactic:
have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
rw : (n.succ - k.succ)! = (n.succ - k.succ) * (n - k.succ)!
rw₁ : (n - k.succ).succ ! = (n - k.succ).succ * (n - k.succ)!
rw₂ rw₃ : (n - k.succ + 1) * (n - k.succ)! = (n - k.succ).succ * (n - k.succ)!
⊢ (n - k)! = (n - k) * (n - k.succ)!

Tactic:
rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]

Premises used: Nat.factorial_succ, Nat.succ_sub, Nat.le_of_lt_succ, Nat.succ_sub_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k)! = (n - k) * (n - k.succ)!

Tactic:
have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
        rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
rw : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !

Tactic:
rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)

Tactic:
simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

Premises used: Nat.mul_left_comm, Nat.factorial_succ, Nat.mul_comm, Nat.mul_assoc
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !

Tactic:
have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
⊢ k * n ! ≤ n * n !

Tactic:
have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
inl : (n.choose k + n.choose k.succ) * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
inl₁ : (n.choose k * k.succ ! + n.choose k.succ * k.succ !) * (n + 1 - k.succ)! = (n + 1)!
inl₂ : n.choose k * k.succ ! * (n + 1 - k.succ)! + n.choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
inl₃ : n.choose k * k.succ ! * (n - k)! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
inl₄ : (k + 1) * n ! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
inl₅ : (k + 1) * n ! + n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n + 1)!
inl₆ : (k + 1) * n ! + (n - k) * n ! = (n + 1)!
inl₇ : k * n ! + 1 * n ! + (n - k) * n ! = (n + 1)!
inl₈ : k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1)!
inl₉ : k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1) * n !
inl₁₀ : k * n ! + 1 * n ! + n * n ! - k * n ! = (n + 1) * n !
inl₁₁ : k * n ! + (1 * n ! + n * n !) - k * n ! = (n + 1) * n !
inl₁₂ : k * n ! + (1 + n) * n ! - k * n ! = (n + 1) * n !
inl₁₃ : (1 + n) * n ! = (n + 1) * n !
inl₁₄ inl₁₅ : (n + 1) * n ! = (n + 1) * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]

Premises used: Nat.factorial_succ, Nat.add_sub_assoc, Nat.choose_succ_succ, Nat.add_sub_cancel_left, Nat.mul_sub_right_distrib, Nat.add_assoc, Nat.succ_sub_succ, Nat.add_mul, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
inr : (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
rw [hk₁]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!

Tactic:
simp [Nat.mul_comm, choose, Nat.sub_self]

Premises used: Nat.choose, Nat.mul_comm, Nat.sub_self
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
inl : ∀ (hnk : n < k), n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
inr : ∀ (hkn : k ≤ n), n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
obtain hnk | hkn := lt_or_ge n k

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hnk : n < k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ 0 < (n - k)! * (k - s)! * s !

Tactic:
apply_rules [factorial_pos, Nat.mul_pos]

Premises used: Nat.mul_pos, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ 0 < (n - k)! * (k - s)! * s !

Tactic:
have h : 0 < (n - k)! * (k - s)! * s ! := by apply_rules [factorial_pos, Nat.mul_pos]
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
inr :
  n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
apply Nat.mul_right_cancel h

Premises used: Nat.mul_right_cancel
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)

Tactic:
grind [choose_mul_factorial_mul_factorial]

Premises used: Nat.choose_mul_factorial_mul_factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
_ :
  n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)
_₁ :
  n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
calc
    _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
      grind [choose_mul_factorial_mul_factorial]
    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
      grind

Premises used: Nat.choose, HMul.hMul, HSub.hSub, Nat.factorial
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
rw : n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)
⊢ n.choose k = n ! / (k ! * (n - k)!)

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]

Premises used: Nat.choose_mul_factorial_mul_factorial, Nat.mul_assoc
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)

Tactic:
(mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm

Premises used: Nat.mul_pos, Nat.mul_div_left, Eq.symm, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)

Tactic:
exact (mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm

Premises used: Nat.mul_pos, Nat.mul_div_left, Eq.symm, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Choose.Basic
Goal:
i j : ℕ
rw : (i + j)! / (j ! * (i + j - j)!) = (i + j)! / (i ! * j !)
rw₁ : (i + j)! / (j ! * i !) = (i + j)! / (i ! * j !)
rw₂ rw₃ : (i + j)! / (i ! * j !) = (i + j)! / (i ! * j !)
⊢ (i + j).choose j = (i + j)! / (i ! * j !)

Tactic:
rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
    Nat.mul_comm]

Premises used: Nat.add_sub_cancel_right, Nat.le_add_left, Nat.mul_comm, Nat.choose_eq_factorial_div_factorial