awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m ≠
      0
simp_rw₃ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m ≠
      0
simp_rw₄ :
  x * (HPow.hPow (α := R[X]) X k).coeff k + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y * (HPow.hPow (α := R[X]) X m).coeff m ≠ 0
simp_rw₅ : x * 1 + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y * 1 ≠ 0
simp_rw₆ : x + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y ≠ 0
simp_rw₇ : (x + y * if k = m then 1 else 0) ≠ 0 ∧ (x * if m = k then 1 else 0) + y ≠ 0
simp_rw₈ : x + y * 0 ≠ 0 ∧ (x * if m = k then 1 else 0) + y ≠ 0
simp_rw₉ : x + y * 0 ≠ 0 ∧ x * 0 + y ≠ 0
simp_rw₁₀ : x + 0 ≠ 0 ∧ 0 + y ≠ 0
simp_rw₁₁ : x + 0 ≠ 0 ∧ y ≠ 0
simp_rw₁₂ : x ≠ 0 ∧ y ≠ 0
simp_rw₁₃ : ¬x = 0 ∧ ¬y = 0
simp_rw₁₄ : ¬False ∧ ¬y = 0
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₁₅ : ¬False ∧ ¬False
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m ≠
      0
simp_rw₃ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m ≠
      0
simp_rw₄ :
  x * (HPow.hPow (α := R[X]) X k).coeff k + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y * (HPow.hPow (α := R[X]) X m).coeff m ≠ 0
simp_rw₅ : x * 1 + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y * 1 ≠ 0
simp_rw₆ : x + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y ≠ 0
simp_rw₇ : (x + y * if k = m then 1 else 0) ≠ 0 ∧ (x * if m = k then 1 else 0) + y ≠ 0
simp_rw₈ : x + y * 0 ≠ 0 ∧ (x * if m = k then 1 else 0) + y ≠ 0
simp_rw₉ : x + y * 0 ≠ 0 ∧ x * 0 + y ≠ 0
simp_rw₁₀ : x + 0 ≠ 0 ∧ 0 + y ≠ 0
simp_rw₁₁ : x + 0 ≠ 0 ∧ y ≠ 0
simp_rw₁₂ : x ≠ 0 ∧ y ≠ 0
simp_rw₁₃ : ¬x = 0 ∧ ¬y = 0
simp_rw₁₄ : ¬False ∧ ¬y = 0
simp_rw₁₅ : ¬False ∧ ¬False
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₁₆ : True ∧ True
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    {k, m, n}
have apply : {k, m, n} ⊆
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
Tactic: apply subset_antisymm (support_trinomial' k m n x y z)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
have simp_rw : k ∈
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
  m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
    {n} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne,
    if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero,
    zero_add, Ne, hx, hy, hz, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
    m ∈
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
      {n} ⊆
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
⊢ {k, m, n} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
have simp_rw₁ : k ∈
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
  m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
    n ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne,
    if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero,
    zero_add, Ne, hx, hy, hz, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support =
    2
have rw : card (α := ℕ) {k, m} = 2
Tactic: rw [support_binomial h hx hy, card_insert_of_notMem (mt mem_singleton.mp h), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
rw : card (α := ℕ) {k, m} = 2
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support =
    2
have rw₁ : card (α := ℕ) {m} + 1 = 2
Tactic: rw [support_binomial h hx hy, card_insert_of_notMem (mt mem_singleton.mp h), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
rw : card (α := ℕ) {k, m} = 2
rw₁ : card (α := ℕ) {m} + 1 = 2
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support =
    2
have rw₂ : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: rw [support_binomial h hx hy, card_insert_of_notMem (mt mem_singleton.mp h), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    3
have rw : card (α := ℕ) {k, m, n} = 3
Tactic: rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : card (α := ℕ) {k, m, n} = 3
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    3
have rw₁ : card (α := ℕ) {m, n} + 1 = 3
Tactic: rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : card (α := ℕ) {k, m, n} = 3
rw₁ : card (α := ℕ) {m, n} + 1 = 3
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    3
have rw₂ : card (α := ℕ) {n} + 1 + 1 = 3
Tactic: rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : card (α := ℕ) {k, m, n} = 3
rw₁ : card (α := ℕ) {m, n} + 1 = 3
rw₂ : card (α := ℕ) {n} + 1 + 1 = 3
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    3
have rw₃ : HAdd.hAdd (α := ℕ) 1 1 + 1 = 3
Tactic: rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = p.coeff d
have h₀ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n), b ≠ (d, n) → p.coeff b.1 * (HPow.hPow (α := R[X]) X n).coeff b.2 = 0
Tactic: rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h₀ :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n),
    b ≠ (d, n) → p.coeff b.1 * (HPow.hPow (α := R[X]) X n).coeff b.2 = 0
⊢ (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = p.coeff d
have h₁ : (d, n) ∉ @antidiagonal _ Nat.instAddMonoid _ (d + n) → p.coeff (d, n).1 * (HPow.hPow (α := R[X]) X n).coeff (d, n).2 = 0
Tactic: rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n)
h2 : (i, j) ≠ (d, n)
⊢ p.coeff (i, j).1 * (HPow.hPow (α := R[X]) X n).coeff (i, j).2 = 0
have h₀ : ¬(i, j).2 = n
Tactic: rw [coeff_X_pow, if_neg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
⊢ (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = p.coeff d
have rw : (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = p.coeff d
Tactic: rw [(commute_X_pow p n).eq, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
rw : (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = p.coeff d
⊢ (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = p.coeff d
have rw₁ : p.coeff d = p.coeff d
Tactic: rw [(commute_X_pow p n).eq, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = if n ≤ d then p.coeff (d - n) else 0
have pos : ∀ (h : n ≤ d), (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
pos : ∀ (h : n ≤ d), (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = if n ≤ d then p.coeff (d - n) else 0
have neg : ∀ (h : ¬n ≤ d), (p * HPow.hPow (α := R[X]) X n).coeff d = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)
have pos : (p * HPow.hPow (α := R[X]) X n).coeff (d - n + n) = p.coeff (d - n + n - n)
Tactic: rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
pos : (p * HPow.hPow (α := R[X]) X n).coeff (d - n + n) = p.coeff (d - n + n - n)
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)
have pos₁ : p.coeff (d - n) = p.coeff (d - n + n - n)
Tactic: rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
pos : (p * HPow.hPow (α := R[X]) X n).coeff (d - n + n) = p.coeff (d - n + n - n)
pos₁ : p.coeff (d - n) = p.coeff (d - n + n - n)
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)
have pos₂ : p.coeff (d - n) = p.coeff (d - n)
Tactic: rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = 0
have neg : ∀ (x : ℕ × ℕ) (hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d), p.coeff x.1 * (HPow.hPow (α := R[X]) X n).coeff x.2 = 0
Tactic: refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
⊢ p.coeff x.1 * (HPow.hPow (α := R[X]) X n).coeff x.2 = 0
have neg : ¬x.2 = n
Tactic: rw [coeff_X_pow, if_neg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
⊢ (HPow.hPow (α := R[X]) X n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0
have rw : (p * HPow.hPow (α := R[X]) X n).coeff d = if n ≤ d then p.coeff (d - n) else 0
Tactic: rw [(commute_X_pow p n).eq, coeff_mul_X_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
rw : (p * HPow.hPow (α := R[X]) X n).coeff d = if n ≤ d then p.coeff (d - n) else 0
⊢ (HPow.hPow (α := R[X]) X n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0
have rw₁ : (if n ≤ d then p.coeff (d - n) else 0) = if n ≤ d then p.coeff (d - n) else 0
Tactic: rw [(commute_X_pow p n).eq, coeff_mul_X_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (X * p).coeff (n + 1) = p.coeff n
have rw : (p * X).coeff (n + 1) = p.coeff n
Tactic: rw [(commute_X p).eq, coeff_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw : (p * X).coeff (n + 1) = p.coeff n
⊢ (X * p).coeff (n + 1) = p.coeff n
have rw₁ : p.coeff n = p.coeff n
Tactic: rw [(commute_X p).eq, coeff_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (HMul.hMul (β := R[X]) p ((monomial n : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
have rw : (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).coeff (d + n) = p.coeff d * r
Tactic: rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).coeff (d + n) = p.coeff d * r
⊢ (HMul.hMul (β := R[X]) p ((monomial n : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
have rw₁ : (p * HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
Tactic: rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).coeff (d + n) = p.coeff d * r
rw₁ :
  (p * HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
⊢ (HMul.hMul (β := R[X]) p ((monomial n : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
have rw₂ : (HMul.hMul (β := R[X]) (p * HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
Tactic: rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).coeff (d + n) = p.coeff d * r
rw₁ :
  (p * HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
rw₂ :
  (HMul.hMul (β := R[X]) (p * HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
⊢ (HMul.hMul (β := R[X]) p ((monomial n : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
have rw₃ : (p * HPow.hPow (α := R[X]) X n).coeff (d + n) * r = p.coeff d * r
Tactic: rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]