awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n),
    (if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
      0
hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
hnc₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n), False
hnc₂ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
hnc₃ :
  ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
    (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc₄ : ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
  (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
  ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n),
    (if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
      0
hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
hnc₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n), False
hnc₂ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
hnc₃ :
  ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
    (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
hnc₄ :
  ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
    (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
    ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc₅ : ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
  (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
  (fun (x_1 : σ) ↦ (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1) = x
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    if (s.sum fun (x : σ) (m : ℕ) ↦ m) = n then
      HMul.hMul (α := R) (↑s.multinomial : R)
        (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
    else 0
have pos : ∀ (hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n),
  coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
pos :
  ∀ (hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n),
    coeff s
        (HPow.hPow (α := MvPolynomial σ R)
          ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
      HMul.hMul (α := R) (↑s.multinomial : R)
        (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    if (s.sum fun (x : σ) (m : ℕ) ↦ m) = n then
      HMul.hMul (α := R) (↑s.multinomial : R)
        (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
    else 0
have neg : ∀ (hs : ¬(s.sum fun (x : σ) (m : ℕ) ↦ m) = n),
  coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
a : σ → R
s : σ →₀ ℕ
n : ℕ
⊢ coeff s (HPow.hPow (α := MvPolynomial σ R) (∑ i : σ, HSMul.hSMul (β := MvPolynomial σ R) (a i) (X i)) n) =
    if (s.sum fun (x : σ) (m : ℕ) ↦ m) = n then
      HMul.hMul (α := R) (↑s.multinomial : R) (s.prod fun (r : σ) (m : ℕ) ↦ a r ^ m)
    else 0
have rw : coeff s
    (HPow.hPow (α := MvPolynomial σ R)
      (∑ i : σ, HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((ofSupportFinite a sorry : (a : σ) → R) i : R) (X i)) n) =
  coeff s
    (HPow.hPow (α := MvPolynomial σ R)
      ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) (ofSupportFinite a sorry) : MvPolynomial σ R) n)
Tactic: rw [← ofSupportFinite_coe (f := a) (hf := Set.toFinite _),
    prod_congr (fun r _ ↦ rfl), ← coeff_linearCombination_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ coeff d (HPow.hPow (α := MvPolynomial σ R) (∑ i : σ, X i) n) =
    (↑(if (d.sum fun (x : σ) (m : ℕ) ↦ m) = n then d.multinomial else 0) : R)
have this : Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (∑ i : σ, HSMul.hSMul (α := R) (β := MvPolynomial σ R) (1 i) (X i))
Tactic: have : (∑ i, X i : MvPolynomial σ R) = ∑ i, (1 : σ → R) i • X i := by simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ coeff d (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (X 0) (X 1) ^ n) =
    (↑(if
            Membership.mem (α := ℕ × ℕ) (@Finset.antidiagonal _ Nat.instAddMonoid _ n)
              (((d : (a : Fin 2) → ℕ) 0, (d : (a : Fin 2) → ℕ) 1) : ℕ × ℕ) then
          n.choose ((d : (a : Fin 2) → ℕ) 0)
        else 0) :
      R)
have rw : Eq.{u_1 + 1} (α := R) (↑(if (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) = n then d.multinomial else 0) : R)
  (↑(if
          Membership.mem (α := ℕ × ℕ) (@Finset.antidiagonal _ Nat.instAddMonoid _ n)
            (((d : (a : Fin 2) → ℕ) 0, (d : (a : Fin 2) → ℕ) 1) : ℕ × ℕ) then
        n.choose ((d : (a : Fin 2) → ℕ) 0)
      else 0) :
    R)
Tactic: rw [← Fin.sum_univ_two, coeff_sum_X_pow_of_fintype]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑(if (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) = n then d.multinomial else 0) : R)
    (↑(if
            Membership.mem (α := ℕ × ℕ) (@Finset.antidiagonal _ Nat.instAddMonoid _ n)
              (((d : (a : Fin 2) → ℕ) 0, (d : (a : Fin 2) → ℕ) 1) : ℕ × ℕ) then
          n.choose ((d : (a : Fin 2) → ℕ) 0)
        else 0) :
      R)
have e_a : (if (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) = n then d.multinomial else 0) =
  if
      Membership.mem (α := ℕ × ℕ) (@Finset.antidiagonal _ Nat.instAddMonoid _ n)
        (((d : (a : Fin 2) → ℕ) 0, (d : (a : Fin 2) → ℕ) 1) : ℕ × ℕ) then
    n.choose ((d : (a : Fin 2) → ℕ) 0)
  else 0
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ (if (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) = n then d.multinomial else 0) =
    if
        Membership.mem (α := ℕ × ℕ) (@Finset.antidiagonal _ Nat.instAddMonoid _ n)
          (((d : (a : Fin 2) → ℕ) 0, (d : (a : Fin 2) → ℕ) 1) : ℕ × ℕ) then
      n.choose ((d : (a : Fin 2) → ℕ) 0)
    else 0
have this : (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
Tactic: have : d.sum (fun x m ↦ m) = d 0 + d 1 := by
    simp [Finsupp.sum_of_support_subset d (Finset.subset_univ d.support)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
⊢ (if (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) = n then d.multinomial else 0) =
    if
        Membership.mem (α := ℕ × ℕ) (@Finset.antidiagonal _ Nat.instAddMonoid _ n)
          (((d : (a : Fin 2) → ℕ) 0, (d : (a : Fin 2) → ℕ) 1) : ℕ × ℕ) then
      n.choose ((d : (a : Fin 2) → ℕ) 0)
    else 0
have e_a : (if HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n then d.multinomial
  else 0) =
  if HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n then
    n.choose ((d : (a : Fin 2) → ℕ) 0)
  else 0
Tactic: simp only [Finset.mem_antidiagonal, this]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
⊢ (if HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n then d.multinomial
    else 0) =
    if HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      n.choose ((d : (a : Fin 2) → ℕ) 0)
    else 0
have pos : ∀ (hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n),
  d.multinomial = n.choose ((d : (a : Fin 2) → ℕ) 0)
Tactic: split_ifs with hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
pos :
  ∀ (hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n),
    d.multinomial = n.choose ((d : (a : Fin 2) → ℕ) 0)
⊢ (if HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n then d.multinomial
    else 0) =
    if HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      n.choose ((d : (a : Fin 2) → ℕ) 0)
    else 0
have neg : ∀ (hd : ¬HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n), Eq (α := ℕ) 0 0
Tactic: split_ifs with hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n
⊢ d.multinomial = n.choose ((d : (a : Fin 2) → ℕ) 0)
have pos : Nat.multinomial (α := Fin 2) Finset.univ (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
Tactic: rw [multinomial_eq_of_support_subset (Finset.subset_univ d.support), Finset.univ_fin2,
      Nat.binomial_eq_choose Fin.zero_ne_one, hd]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n
pos : Nat.multinomial (α := Fin 2) Finset.univ (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
⊢ d.multinomial = n.choose ((d : (a : Fin 2) → ℕ) 0)
have pos₁ : Nat.multinomial (α := Fin 2) {0, 1} (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
Tactic: rw [multinomial_eq_of_support_subset (Finset.subset_univ d.support), Finset.univ_fin2,
      Nat.binomial_eq_choose Fin.zero_ne_one, hd]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n
pos : Nat.multinomial (α := Fin 2) Finset.univ (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
pos₁ : Nat.multinomial (α := Fin 2) {0, 1} (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
⊢ d.multinomial = n.choose ((d : (a : Fin 2) → ℕ) 0)
have pos₂ : (HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)).choose
    ((d : (a : Fin 2) → ℕ) 0) =
  n.choose ((d : (a : Fin 2) → ℕ) 0)
Tactic: rw [multinomial_eq_of_support_subset (Finset.subset_univ d.support), Finset.univ_fin2,
      Nat.binomial_eq_choose Fin.zero_ne_one, hd]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this :
  (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n
pos : Nat.multinomial (α := Fin 2) Finset.univ (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
pos₁ : Nat.multinomial (α := Fin 2) {0, 1} (⇑d : (a : Fin 2) → ℕ) = n.choose ((d : (a : Fin 2) → ℕ) 0)
pos₂ :
  (HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)).choose
      ((d : (a : Fin 2) → ℕ) 0) =
    n.choose ((d : (a : Fin 2) → ℕ) 0)
⊢ d.multinomial = n.choose ((d : (a : Fin 2) → ℕ) 0)
have pos₃ : n.choose ((d : (a : Fin 2) → ℕ) 0) = n.choose ((d : (a : Fin 2) → ℕ) 0)
Tactic: rw [multinomial_eq_of_support_subset (Finset.subset_univ d.support), Finset.univ_fin2,
      Nat.binomial_eq_choose Fin.zero_ne_one, hd]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x
have h : ∀ (i : σ), comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
⊢ Eq (α := (σ → R) → σ → R) (comap (AlgHom.id R (MvPolynomial σ R))) id
have h : ∀ (x : σ → R), comap (AlgHom.id R (MvPolynomial σ R)) x = id x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (g.comp f) x = comap f (comap g x)
have h : ∀ (i : σ), comap (g.comp f) x i = comap f (comap g x) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (g.comp f) x i = comap f (comap g x) i
have trans : comap (g.comp f) x i =
  (aeval x : (a : MvPolynomial υ R) → R)
    ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
          (a : MvPolynomial τ R) → MvPolynomial υ R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R)
Tactic: trans aeval x (aeval (fun i => g (X i)) (f (X i)))
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
trans :
  comap (g.comp f) x i =
    (aeval x : (a : MvPolynomial υ R) → R)
      ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
            (a : MvPolynomial τ R) → MvPolynomial υ R)
          ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
        MvPolynomial υ R)
⊢ comap (g.comp f) x i = comap f (comap g x) i
have trans₁ : (aeval x : (a : MvPolynomial υ R) → R)
    ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
          (a : MvPolynomial τ R) → MvPolynomial υ R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R) =
  comap f (comap g x) i
Tactic: trans aeval x (aeval (fun i => g (X i)) (f (X i)))
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (g.comp f) x i =
    (aeval x : (a : MvPolynomial υ R) → R)
      ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
            (a : MvPolynomial τ R) → MvPolynomial υ R)
          ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
        MvPolynomial υ R)
have apply : Eq (α := MvPolynomial υ R) ((g.comp f : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
  ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
        (a : MvPolynomial τ R) → MvPolynomial υ R)
      ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
    MvPolynomial υ R)
Tactic: apply eval₂Hom_congr rfl rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ Eq (α := MvPolynomial υ R) ((g.comp f : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
    ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
          (a : MvPolynomial τ R) → MvPolynomial υ R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R)
have rw : Eq (α := MvPolynomial υ R)
  ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
    MvPolynomial υ R)
  ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
        (a : MvPolynomial τ R) → MvPolynomial υ R)
      ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
    MvPolynomial υ R)
Tactic: rw [AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
this : g = aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i)
⊢ Eq (α := MvPolynomial υ R)
    ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R)
    ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
          (a : MvPolynomial τ R) → MvPolynomial υ R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R)
have rw : Eq (α := MvPolynomial υ R)
  ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
    MvPolynomial υ R)
  ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
    MvPolynomial υ R)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ Eq (α := MvPolynomial υ R)
    ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R)
    ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
          (a : MvPolynomial τ R) → MvPolynomial υ R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial υ R)
have suffices : g = aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i)
Tactic: suffices g = aeval fun i => g (X i) by rw [← this]