awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
⊢ (↑(chineseRemainderOfList a s l co) : ℕ) < (List.map s l).prod
have nil : ∀ (co : List.Pairwise (Coprime on s) []) (hs : ∀ (i : ι), Membership.mem (γ := List ι) [] i → s i ≠ 0),
  (↑(chineseRemainderOfList a s [] co) : ℕ) < (List.map s []).prod
Tactic: cases l with
  | nil => simp
  | cons i l =>
    simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_
    simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
    intro j hj
    exact hs j (List.mem_cons_of_mem _ hj)
Cleared hypotheses: l, co, hs
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
nil :
  ∀ (co : List.Pairwise (Coprime on s) []) (hs : ∀ (i : ι), Membership.mem (γ := List ι) [] i → s i ≠ 0),
    (↑(chineseRemainderOfList a s [] co) : ℕ) < (List.map s []).prod
⊢ (↑(chineseRemainderOfList a s l co) : ℕ) < (List.map s l).prod
have cons : ∀ (i : ι) (l : List ι) (co : List.Pairwise (Coprime on s) (i :: l)) (hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0),
  (↑(chineseRemainderOfList a s (i :: l) co) : ℕ) < (List.map s (i :: l)).prod
Tactic: cases l with
  | nil => simp
  | cons i l =>
    simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_
    simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
    intro j hj
    exact hs j (List.mem_cons_of_mem _ hj)
Cleared hypotheses: l, co, hs
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ i ∈ l, z ≡ a i [MOD s i]),
    z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ (↑(chineseRemainderOfList a s (i :: l) co) : ℕ) [MOD (List.map s (i :: l)).prod]
have cons : z ≡ (↑(chineseRemainder sorry (a i) (↑(chineseRemainderOfList a s l sorry) : ℕ)) : ℕ) [MOD s i * (List.map s l).prod]
Tactic: simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ i ∈ l, z ≡ a i [MOD s i]),
    z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ (s i).Coprime (List.map s l).prod
have simp : ∀ a ∈ l, (s i).Coprime (s a)
Tactic: simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (hypothesis)
Goal:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ i ∈ l, z ≡ a i [MOD s i]),
    z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ (↑(chineseRemainder ⋯ (a i) (↑(chineseRemainderOfList a s l ⋯) : ℕ)) : ℕ) [MOD s i * (List.map s l).prod]
have this : (s i).Coprime (List.map s l).prod
Tactic: have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
z : ℕ
hz : ∀ i ∈ l, z ≡ a i [MOD s i]
⊢ z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod]
have nil : ∀ (co : List.Pairwise (Coprime on s) []) (hz : ∀ (i : ι), Membership.mem (γ := List ι) [] i → z ≡ a i [MOD s i]),
  z ≡ (↑(chineseRemainderOfList a s [] co) : ℕ) [MOD (List.map s []).prod]
Tactic: induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    exact chineseRemainder_modEq_unique this
      (hz i List.mem_cons_self) (ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))
Cleared hypotheses: l, co, hz
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
z : ℕ
hz : ∀ i ∈ l, z ≡ a i [MOD s i]
nil :
  ∀ (co : List.Pairwise (Coprime on s) []) (hz : ∀ (i : ι), Membership.mem (γ := List ι) [] i → z ≡ a i [MOD s i]),
    z ≡ (↑(chineseRemainderOfList a s [] co) : ℕ) [MOD (List.map s []).prod]
⊢ z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod]
have cons : ∀ (i : ι) (l : List ι)
  (ih :
    ∀ (co : List.Pairwise (Coprime on s) l) (hz : ∀ i ∈ l, z ≡ a i [MOD s i]),
      z ≡ (↑(chineseRemainderOfList a s l co) : ℕ) [MOD (List.map s l).prod])
  (co : List.Pairwise (Coprime on s) (i :: l)) (hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]),
  z ≡ (↑(chineseRemainderOfList a s (i :: l) co) : ℕ) [MOD (List.map s (i :: l)).prod]
Tactic: induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    exact chineseRemainder_modEq_unique this
      (hz i List.mem_cons_self) (ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))
Cleared hypotheses: l, co, hz
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (hypothesis)
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
⊢ (↑(chineseRemainderOfList a s l co) : ℕ) = (↑(chineseRemainderOfList a s l' ⋯) : ℕ)
have hlp : (List.map s l).prod = (List.map s l').prod
Tactic: have hlp : (l.map s).prod = (l'.map s).prod := List.Perm.prod_eq (List.Perm.map s hl)
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k : ℕ // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ (↑z : ℕ) < (List.map s l).prod
have rw : (↑z : ℕ) < (List.map s l').prod
Tactic: rw [hlp]
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : Set.Pairwise {x : ι | x ∈ l'} (Coprime on s)
co : Set.Pairwise {x : ι | x ∈ l} (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : (↑l : Multiset ι) = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : Set.Pairwise {x : ι | x ∈ m'} (Coprime on s)},
    (↑(Eq.ndrec (motive := fun (m : Multiset ι) ↦
            m.Nodup →
              (∀ i ∈ m, s i ≠ 0) →
                Set.Pairwise {x : ι | x ∈ m} (Coprime on s) → { k : ℕ // ∀ i ∈ m, k ≡ a i [MOD s i] })
            (fun (nod : (↑l : Multiset ι).Nodup) (x : ∀ i ∈ (↑l : Multiset ι), s i ≠ 0)
                (co : Set.Pairwise {x : ι | x ∈ (↑l : Multiset ι)} (Coprime on s)) ↦
              chineseRemainderOfList a s l ⋯)
            e nod'' hs'' co'') :
        ℕ) =
      (↑(chineseRemainderOfList a s l lco) : ℕ)
⊢ Eq.ndrec (a := ⟦l⟧) (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] })
      fun (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0) (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
      chineseRemainderOfList a s l ⋯ (b := ⟦l'⟧) ⋯ nod' hs' co' =
    chineseRemainderOfList a s l' ⋯
have a₁ : (↑(Eq.ndrec (a := ⟦l⟧) (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] })
        fun (nod : Multiset.Nodup ⟦l⟧) (x : ∀ i ∈ ⟦l⟧, s i ≠ 0) (co : Set.Pairwise {x : ι | x ∈ ⟦l⟧} (Coprime on s)) ↦
        chineseRemainderOfList a s l sorry (b := ⟦l'⟧) sorry nod' hs' co') :
    ℕ) =
  (↑(chineseRemainderOfList a s l' sorry) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.ChineseRemainder (goal)
Goal:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
nod : m.Nodup
hs : ∀ i ∈ m, s i ≠ 0
pp : Set.Pairwise {x : ι | x ∈ m} (Coprime on s)
⊢ (↑(chineseRemainderOfMultiset a s nod hs pp) : ℕ) < (Multiset.map s m).prod
have mk : ∀ (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)),
  (↑(chineseRemainderOfMultiset a s nod hs pp) : ℕ) <
    (Multiset.map s (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
Tactic: induction m using Quot.ind with | _ l
Cleared hypotheses: m, nod, hs, pp
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n.choose 0 = 1
have zero : choose 0 0 = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : choose 0 0 = 1
⊢ n.choose 0 = 1
have succ : ∀ (n : ℕ), (n + 1).choose 0 = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : 0 < k
⊢ (n + 1).choose k = n.choose (k - 1) + n.choose k
have obtain : ∀ (l : ℕ) (hk : 0 < l + 1), (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)
Tactic: obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hn : 0 < n
⊢ n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)
have obtain : ∀ (l : ℕ) (hn : 0 < l + 1), (l + 1).choose (k + 1) = (l + 1 - 1).choose k + (l + 1 - 1).choose (k + 1)
Tactic: obtain ⟨l, rfl⟩ : ∃ l, n = l + 1 := Nat.exists_eq_add_of_le' hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k
have obtain : ∀ (l : ℕ) (hk : 0 < l + 1), n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
Tactic: obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
have rw : (n - 1).choose l + (n - 1).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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
have rw₁ : (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose l + (n - 1).choose (l + 1)
Tactic: rw [choose_succ_right _ _ hn, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).choose (k + 1) = 0
have hnk : n < k
Tactic: have hnk : n < k := lt_of_succ_lt_succ hk
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ (n + 1).choose (k + 1) = 0
have hnk1 : n < k + 1
Tactic: have hnk1 : n < k + 1 := lt_of_succ_lt hk
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ (n + 1).choose (k + 1) = 0
have rw : n.choose k + n.choose k.succ = 0
Tactic: rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
rw : n.choose k + n.choose k.succ = 0
⊢ (n + 1).choose (k + 1) = 0
have rw₁ : 0 + n.choose k.succ = 0
Tactic: rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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
⊢ (n + 1).choose (k + 1) = 0
have rw₂ : HAdd.hAdd (α := ℕ) 0 0 = 0
Tactic: rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n.choose n = 1
have zero : choose 0 0 = 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : choose 0 0 = 1
⊢ n.choose n = 1
have succ : ∀ (n : ℕ), n.choose n = 1 → (n + 1).choose (n + 1) = 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n.choose 1 = n
have zero : choose 0 1 = 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : choose 0 1 = 0
⊢ n.choose 1 = n
have succ : ∀ (n : ℕ), n.choose 1 = n → (n + 1).choose 1 = n + 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
have rw : n * (n + 1) / 2 = n * (n - 1 + 2) / 2
Tactic: rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
rw : n * (n + 1) / 2 = n * (n - 1 + 2) / 2
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
have H : LT.lt (α := ℕ) 0 2
Tactic: rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2
have zero : 0 * HAdd.hAdd (α := ℕ) 0 1 / 2 = 0 * (HSub.hSub (α := ℕ) 0 1 + 2) / 2
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : 0 * HAdd.hAdd (α := ℕ) 0 1 / 2 = 0 * (HSub.hSub (α := ℕ) 0 1 + 2) / 2
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2
have succ : ∀ (n : ℕ), (n + 1) * (n + 1 + 1) / 2 = (n + 1) * (n + 1 - 1 + 2) / 2
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2
have succ : n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
Tactic: rw [triangle_succ n, choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ n.choose 2 = n * (n - 1) / 2
have zero : choose 0 2 = 0 * HSub.hSub (α := ℕ) 0 1 / 2
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
zero : choose 0 2 = 0 * HSub.hSub (α := ℕ) 0 1 / 2
⊢ n.choose 2 = n * (n - 1) / 2
have succ : ∀ (n : ℕ) (ih : n.choose 2 = n * (n - 1) / 2), (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
x : ℕ
hk : x ≤ 0
⊢ 0 < choose 0 x
have rw : 0 < choose 0 0
Tactic: rw [Nat.eq_zero_of_le_zero hk]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have rw : (n + 1 + 1) * (n + 1).choose (k + 1) = ((n + 1).choose (k + 1) + (n + 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have rw₂ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1) * n.choose (k + 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
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)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have rw₆ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n.choose k + n.choose (k + 1)) + (n + 1).choose (k + 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]