awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
x : σ → ℕ
hx : x ∈ a.support.piAntidiag n
hnc : ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
⊢ (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

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
hnc : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
⊢ False

Tactic:
apply hs
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
⊢ a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support

Tactic:
simp only [Finset.mem_piAntidiag] at hx

Premises used: Finset.mem_piAntidiag
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
⊢ ∀ i ∈ a.support, Eq (α := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
hnc :
  ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x
⊢ (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n

Tactic:
rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]

Premises used: Finsupp.support, And.left, Finsupp.support_indicator_subset, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
hnc : (fun (x_1 : σ) ↦ (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1) = x
⊢ ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
hnc : ∀ (i : σ), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
⊢ (fun (x_1 : σ) ↦ (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1) = x

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
i : σ
pos : ∀ (hi : i ∈ a.support), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
neg : ∀ (hi : i ∉ a.support), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
⊢ (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i

Tactic:
by_cases hi : i ∈ a.support

Premises used: Finsupp.support
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
i : σ
hi : i ∈ a.support
⊢ (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i

Tactic:
simp [Finsupp.indicator_of_mem hi]

Premises used: Finsupp.indicator_of_mem
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
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
i : σ
hi : i ∉ a.support
⊢ (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i

Tactic:
grind [Finsupp.indicator_of_notMem hi]

Premises used: Finsupp.indicator_of_notMem
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
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)
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
⊢ 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

Tactic:
split_ifs with hs
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
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:
coeff_linearCombination_X_pow_of_eq a hs

Premises used: _private.0.MvPolynomial.coeff_linearCombination_X_pow_of_eq
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
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:
exact coeff_linearCombination_X_pow_of_eq a hs

Premises used: _private.0.MvPolynomial.coeff_linearCombination_X_pow_of_eq
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
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:
coeff_linearCombination_X_pow_of_ne a hs

Premises used: _private.0.MvPolynomial.coeff_linearCombination_X_pow_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
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:
exact coeff_linearCombination_X_pow_of_ne a hs

Premises used: _private.0.MvPolynomial.coeff_linearCombination_X_pow_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
a : σ → R
s : σ →₀ ℕ
n : ℕ
rw :
  coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        (∑ i : σ, HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((ofSupportFinite a ⋯ : (a : σ) → R) i : R) (X i)) n) =
    coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) (ofSupportFinite a ⋯) : MvPolynomial σ R) 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

Tactic:
rw [← ofSupportFinite_coe (f := a) (hf := Set.toFinite _),
    prod_congr (fun r _ ↦ rfl), ← coeff_linearCombination_X_pow]

Premises used: Finsupp.prod_congr, MvPolynomial.coeff_linearCombination_X_pow, Finsupp.ofSupportFinite_coe, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
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 (α := R) (β := MvPolynomial σ R) ((ofSupportFinite a ⋯ : (a : σ) → R) i : R) (X i)) n) =
    coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) (ofSupportFinite a ⋯) : MvPolynomial σ R) n)

Tactic:
simp [linearCombination_apply, sum_of_support_subset (s := Finset.univ)]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (∑ i : σ, HSMul.hSMul (α := R) (β := MvPolynomial σ R) (1 i) (X i))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ 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
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
d : σ →₀ ℕ
n : ℕ
this : Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (∑ i : σ, HSMul.hSMul (α := R) (β := MvPolynomial σ R) (1 i) (X i))
⊢ coeff d (HPow.hPow (α := MvPolynomial σ R) (∑ i : σ, X i) n) =
    (↑(if (d.sum fun (x : σ) (m : ℕ) ↦ m) = n then d.multinomial else 0) : R)

Tactic:
simp [this, coeff_linearCombination_X_pow_of_fintype]

Premises used: MvPolynomial.coeff_linearCombination_X_pow_of_fintype
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
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)
⊢ 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)

Tactic:
rw [← Fin.sum_univ_two, coeff_sum_X_pow_of_fintype]

Premises used: MvPolynomial.coeff_sum_X_pow_of_fintype, Fin.sum_univ_two
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
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
⊢ 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:
congr 1
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ (d.sum fun (x : Fin 2) (m : ℕ) ↦ m) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ)

Tactic:
simp [Finsupp.sum_of_support_subset d (Finset.subset_univ d.support)]

Premises used: Finsupp.support, Finset.subset_univ, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
inst : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ (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)]
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
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 : ℕ)
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
⊢ (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:
simp only [Finset.mem_antidiagonal, this]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
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)
neg :
  ∀ (hd : ¬HAdd.hAdd (α := ℕ) (β := ℕ) ((d : (a : Fin 2) → ℕ) 0 : ℕ) ((d : (a : Fin 2) → ℕ) 1 : ℕ) = n), Eq (α := ℕ) 0 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

Tactic:
split_ifs with hd
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
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)
pos₃ pos₄ : n.choose ((d : (a : Fin 2) → ℕ) 0) = n.choose ((d : (a : Fin 2) → ℕ) 0)
⊢ d.multinomial = 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]

Premises used: Finsupp.support, Finsupp.multinomial_eq_of_support_subset, Finset.univ_fin2, Fin.zero_ne_one, Nat.binomial_eq_choose, Finset.subset_univ
-- Module: Mathlib.Algebra.MvPolynomial.Coeff
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
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
x : τ → R
i : σ
⊢ comap f x i =
    (aeval x : (a : MvPolynomial τ R) → R) ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)

Tactic:
rfl

Premises used: MvPolynomial.comap, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : σ → R
h : ∀ (i : σ), comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x

Tactic:
funext i
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i

Tactic:
simp only [comap, AlgHom.id_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.comap, AlgHom.id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
h : ∀ (x : σ → R), comap (AlgHom.id R (MvPolynomial σ R)) x = id x
⊢ Eq (α := (σ → R) → σ → R) (comap (AlgHom.id R (MvPolynomial σ R))) id

Tactic:
funext x
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x

Tactic:
comap_id_apply x

Premises used: MvPolynomial.comap_id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x

Tactic:
exact comap_id_apply x

Premises used: MvPolynomial.comap_id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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
h : ∀ (i : σ), comap (g.comp f) x i = comap f (comap g x) i
⊢ comap (g.comp f) x = comap f (comap g x)

Tactic:
funext i
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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)
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
⊢ comap (g.comp f) x i = comap f (comap g x) i

Tactic:
trans aeval x (aeval (fun i => g (X i)) (f (X i)))

Premises used: MvPolynomial.aeval, MvPolynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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 : σ
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)
⊢ 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:
apply eval₂Hom_congr rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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 : σ
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)
⊢ 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:
rw [AlgHom.comp_apply]

Premises used: AlgHom.comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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)
rw 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)
⊢ 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 [← this]
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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 : σ
suffices : 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)

Tactic:
suffices g = aeval fun i => g (X i) by rw [← this]
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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 : σ
⊢ g = aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i)

Tactic:
aeval_unique g

Premises used: MvPolynomial.aeval_unique
-- Module: Mathlib.Algebra.MvPolynomial.Comap
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 : σ
⊢ g = aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i)

Tactic:
exact aeval_unique g

Premises used: MvPolynomial.aeval_unique