awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : n / p + 1 ≤ (k % p, k / p).2
⊢ n / p < (k % p, k / p).2

Tactic:
tauto
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : n / p + 1 ≤ (k % p, k / p).2
⊢ Eq (α := ZMod p) 0
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ))

Tactic:
simp [choose_eq_zero_of_lt (by tauto)]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
rw : (↑(n.choose k) : ℤ) ≡ (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑(n.choose k) : ℤ) ≡ (↑((n % p).choose (k % p) * (n / p).choose (k / p)) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
exact_mod_cast choose_modEq_choose_mod_mul_choose_div

Premises used: Choose.choose_modEq_choose_mod_mul_choose_div
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
⊢ (↑(n.choose k) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ zero).choose (k / p ^ zero)) : ℤ)
      (↑(∏ i ∈ range zero, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD
    (↑p : ℤ)]

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
rw :
  HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
        (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) *
      (↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑(∏ i ∈ range a.succ, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD
    (↑p : ℤ)]

Tactic:
rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]

Premises used: mul_assoc, Nat.cast_mul, mul_right_comm, Finset.prod_range_succ
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
h₁ :
  (↑((n / p ^ a).choose (k / p ^ a)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
        (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) *
      (↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) : ℤ) [ZMOD
    (↑p : ℤ)]

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
h₁ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
⊢ (↑((n / p ^ a).choose (k / p ^ a)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]

Tactic:
apply choose_modEq_choose_mod_mul_choose_div.trans

Premises used: Int.ModEq.trans, Choose.choose_modEq_choose_mod_mul_choose_div
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a_1 a : ℕ
h₁ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
h₂ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ)
      (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]
h₃ :
  HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ)
      (↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ)
      (↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) : ℤ) [ZMOD
    (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) (↑((n / p ^ a / p).choose (k / p ^ a / p)) : ℤ) ≡
    HMul.hMul (α := ℤ) (↑((n / p ^ a.succ).choose (k / p ^ a.succ)) : ℤ)
      (↑((n / p ^ a % p).choose (k / p ^ a % p)) : ℤ) [ZMOD
    (↑p : ℤ)]

Tactic:
simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]

Premises used: pow_succ, Int.ModEq.refl, mul_comm, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
apply :
  HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑(n.choose k) : ℤ) ≡ ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
apply (choose_modEq_choose_mul_prod_range_choose a).trans

Premises used: Int.ModEq.trans, Choose.choose_modEq_choose_mul_prod_range_choose
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
simp_rw :
  HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₁ :
  HMul.hMul (α := ℤ) (↑(choose 0 0) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₂ :
  HMul.hMul (α := ℤ) (↑1 : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₃ :
  HMul.hMul (α := ℤ) 1 (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₄ :
  (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₅ :
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]

Premises used: Nat.choose, Int.ModEq.refl, Nat.cast_prod, Nat.div_eq_of_lt, Nat.cast_one, one_mul
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
rw : (↑(n.choose k) : ℤ) ≡ (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ n.choose k ≡ ∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ (↑(n.choose k) : ℤ) ≡ (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
exact_mod_cast choose_modEq_prod_range_choose ha₁ ha₂

Premises used: Choose.choose_modEq_prod_range_choose
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
a b p : ℕ
inst : Fact (Nat.Prime p)
grw :
  HMul.hMul (α := ℤ) (↑((p * a % p).choose (p * b % p)) : ℤ) (↑((p * a / p).choose (p * b / p)) : ℤ) ≡
    (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p * a).choose (p * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
grw [choose_modEq_choose_mod_mul_choose_div]

Premises used: Choose.choose_modEq_choose_mod_mul_choose_div
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ HMul.hMul (α := ℤ) (↑((p * a % p).choose (p * b % p)) : ℤ) (↑((p * a / p).choose (p * b / p)) : ℤ) ≡
    (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
simp [NeZero.pos, Int.ModEq.refl]

Premises used: Int.ModEq.refl, NeZero.pos
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
a b p : ℕ
inst : Fact (Nat.Prime p)
rw : (↑((p * a).choose (p * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (p * a).choose (p * b) ≡ a.choose b [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑((p * a).choose (p * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
exact_mod_cast choose_mul_mul_modEq_choose

Premises used: Choose.choose_mul_mul_modEq_choose
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑((HPow.hPow (β := ℕ) p 0 * a).choose (HPow.hPow (β := ℕ) p 0 * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
simp [Int.ModEq.refl]

Premises used: Int.ModEq.refl
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
k_1 a b p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ : (↑((p * p ^ k * a).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₁ : (↑((p * (p ^ k * a)).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₂ : (↑((p * (p ^ k * a)).choose (p * (p ^ k * b))) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₃ : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₄ succ₅ : (↑(a.choose b) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]

Premises used: Nat.pow_succ', mul_assoc, Choose.choose_mul_mul_modEq_choose
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
zero : (↑((HPow.hPow (β := ℕ) p 0 * a).choose (HPow.hPow (β := ℕ) p 0 * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ :
  ∀ (k : ℕ) (ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]),
    (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
induction k with
  | zero => simp [Int.ModEq.refl]
  | succ k ih =>
    grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]

Premises used: Nat.pow_succ', Int.ModEq.refl, mul_assoc, Nat.zero, Nat.succ, Choose.choose_mul_mul_modEq_choose
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
rw : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff
-- Module: Mathlib.Data.Nat.Choose.Lucas
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]

Tactic:
exact_mod_cast choose_pow_mul_pow_mul_modEq_choose

Premises used: Choose.choose_pow_mul_pow_mul_modEq_choose
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ 0 < multinomial s f

Tactic:
Nat.div_pos (le_of_dvd (factorial_pos _) (prod_factorial_dvd_factorial_sum s f))
    (prod_factorial_pos s f)

Premises used: Nat.prod_factorial_pos, Nat.multinomial, Nat.prod_factorial_dvd_factorial_sum, Nat.le_of_dvd, Nat.factorial_pos, Nat.div_pos
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∏ i ∈ s, (f i)!) * multinomial s f = (∑ i ∈ s, f i)!

Tactic:
Nat.mul_div_cancel' (prod_factorial_dvd_factorial_sum s f)

Premises used: Nat.multinomial, Nat.prod_factorial_dvd_factorial_sum, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
⊢ multinomial ∅ f = 1

Tactic:
simp [multinomial]

Premises used: Nat.multinomial
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
rw : LT.lt (α := ℕ) 0 (∏ i ∈ cons a s ha, (f i)!)
⊢ multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons,
    multinomial, mul_assoc, mul_left_comm _ (f a)!,
    Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
    Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]

Premises used: Nat.div_mul_cancel, Finset.sum_cons, Nat.multinomial, mul_assoc, Nat.prod_factorial_dvd_factorial_sum, mul_left_comm, Nat.choose_symm_add, Nat.factorial, Finset.prod_cons, Nat.add_choose_mul_factorial_mul_factorial, Nat.div_eq_iff_eq_mul_left
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ LT.lt (α := ℕ) 0 (∏ i ∈ cons a s ha, (f i)!)

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
ha : a ∉ s
f : α → ℕ
rw : multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
rw₁ rw₂ : (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
⊢ multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
rw [← cons_eq_insert _ _ ha, multinomial_cons]

Premises used: Nat.multinomial_cons, Finset.cons_eq_insert
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α → ℕ
rw : (f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1
⊢ multinomial {a} f = 1

Tactic:
rw [← cons_empty, multinomial_cons]

Premises used: Nat.multinomial_cons, Finset.cons_empty
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α → ℕ
⊢ (f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst : DecidableEq α
h : a ∉ s
h₁ : f a = 1
rw :
  HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) =
    (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
⊢ (∑ i ∈ insert a s, f i)! / ∏ i ∈ insert a s, (f i)! = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]

Premises used: Finset.prod_insert, Nat.succ_eq_add_one, Nat.factorial_succ, add_comm, Finset.sum_insert
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst : DecidableEq α
h : a ∉ s
h₁ : f a = 1
simp :
  HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! =
    (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) =
    (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
simp only [factorial, succ_eq_add_one, zero_add, mul_one, one_mul]

Premises used: Nat.succ_eq_add_one, zero_add, Nat.factorial, mul_one, one_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst : DecidableEq α
h : a ∉ s
h₁ : f a = 1
rw rw₁ :
  HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!) =
    (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! =
    (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)

Tactic:
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]

Premises used: Nat.prod_factorial_dvd_factorial_sum, Nat.mul_div_assoc
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
e_a : (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!
e_a₁ : Eq (α := ℕ) (∏ i ∈ s, (f i)!) (∏ i ∈ s, (g i)!)
⊢ (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)! = (∑ i ∈ s, g i)! / ∏ i ∈ s, (g i)!

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
e_a e_a₁ : (s.sum g)! = (∑ i ∈ s, g i)!
⊢ (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!

Tactic:
rw [Finset.sum_congr rfl h]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
a : α
ha : a ∈ s
rw rw₁ : (g a)! = (g a)!
⊢ (f a)! = (g a)!

Tactic:
rw [h a ha]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ Eq (α := ℕ) (∏ i ∈ s, (f i)!) (∏ i ∈ s, (g i)!)

Tactic:
exact Finset.prod_congr rfl fun a ha => by rw [h a ha]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ t, a ∉ s → (g a)! = 1

Tactic:
aesop
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ s, a ∉ t → Eq (α := ℕ) ((fun (a : α) ↦ (f a)!) a) 1

Tactic:
aesop
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ t, a ∈ s → (g a)! = (fun (a : α) ↦ (f a)!) a

Tactic:
aesop
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
rw : (∑ i ∈ s, f i)! = (∑ i ∈ t, g i)!
⊢ multinomial s f = multinomial t g

Tactic:
rw [← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun x _ ↦ factorial_ne_zero (g x))),
    multinomial_spec, prod_congr_of_eq_on_inter (g := fun a ↦ (f a)!) (s₂ := s) (by aesop)
    (by aesop) (by aesop), multinomial_spec s f]

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, Nat.multinomial_spec, Nat.factorial_ne_zero, Nat.mul_right_inj, Finset.prod_congr_of_eq_on_inter
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
e_a : Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ t, g i)
⊢ (∑ i ∈ s, f i)! = (∑ i ∈ t, g i)!

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ s, a ∉ t → f a = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ t, a ∉ s → g a = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ s, a ∈ t → f a = g a

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ t, g i)

Tactic:
exact sum_congr_of_eq_on_inter (by grind) (by grind) (by grind)

Premises used: Finset.sum_congr_of_eq_on_inter
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hst : s ⊆ t
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s, f a = g a
⊢ ∀ a ∈ s \ t, f a = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hst : s ⊆ t
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s, f a = g a
⊢ ∀ a ∈ s ∩ t, f a = g a

Tactic:
grind
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
rw : (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
⊢ multinomial s (Pi.single (M := fun (a : α) ↦ ℕ) a n) = 1

Tactic:
rw [← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun _ _ ↦ factorial_ne_zero _)), mul_one,
    multinomial_spec, sum_pi_single']

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, Nat.multinomial_spec, Nat.factorial_ne_zero, Finset.sum_pi_single', mul_one, Nat.mul_right_inj
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
pos : ∀ (ha : a ∈ s), n ! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
neg : ∀ (ha : a ∉ s), 0! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
⊢ (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!

Tactic:
split_ifs with ha
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∈ s
⊢ ∀ b ∈ s, b ≠ a → (Pi.single (M := fun (a : α) ↦ ℕ) a n b)! = 1

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∈ s
⊢ a ∉ s → (Pi.single (M := fun (a : α) ↦ ℕ) a n a)! = 1

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∈ s
pos : n ! = (Pi.single (M := fun (a : α) ↦ ℕ) a n a)!
pos₁ pos₂ : n ! = n !
⊢ n ! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!

Tactic:
rw [Finset.prod_eq_single a (by simp_all) (by simp_all), Pi.single_eq_same]

Premises used: Pi.single_eq_same, Finset.prod_eq_single
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
neg : Eq (α := ℕ) (∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!) 1
⊢ 0! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!

Tactic:
rw [eq_comm, factorial_zero]

Premises used: eq_comm, Nat.factorial_zero
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
neg : ∀ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)! = 1
⊢ Eq (α := ℕ) (∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!) 1

Tactic:
apply Finset.prod_eq_one

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
x : α
hb : x ∈ s
neg : (if x = a then n else 0)! = 1
neg₁ : 0! = 1
neg₂ neg₃ : Eq (α := ℕ) 1 1
⊢ (Pi.single (M := fun (a : α) ↦ ℕ) a n x)! = 1

Tactic:
rw [Pi.single_apply, if_neg (ne_of_mem_of_not_mem hb ha), factorial_zero]

Premises used: Pi.single_apply, ne_of_mem_of_not_mem, Nat.factorial_zero, if_neg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)

Tactic:
simp [multinomial, Finset.sum_pair h, Finset.prod_pair h]

Premises used: Finset.sum_pair, Nat.multinomial, Finset.prod_pair
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b).choose (f a)

Tactic:
simp [binomial_eq h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]

Premises used: Nat.le_add_right, Nat.binomial_eq, Nat.choose_eq_factorial_div_factorial