awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
refine_1 :
  ∀ (h : #f.support = 1),
    ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)
refine_2 :
  (∃ (k : ℕ) (x : R) (_ : x ≠ 0),
      f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)) →
    #f.support = 1
⊢ #f.support = 1 ↔
    ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support = 1
refine_1 :
  ∀ (k : Fin 1 → ℕ) (x : Fin 1 → R),
    StrictMono k →
      ∀ (hx : ∀ (i : Fin 1), x i ≠ 0)
        (h :
          #(support.{u_1} (R := R)
                (∑ i : Fin 1,
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
            1),
        ∃ (k_1 : ℕ) (x_1 : R) (_ : x_1 ≠ 0),
          ∑ i : Fin 1, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_1 : R[X]) (HPow.hPow (α := R[X]) X k_1)
⊢ ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)

Tactic:
obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h

Premises used: Polynomial.card_support_eq, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 1 → ℕ
x : Fin 1 → R
w : StrictMono k
hx : ∀ (i : Fin 1), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 1, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    1
⊢ ∃ (k_1 : ℕ) (x_1 : R) (_ : x_1 ≠ 0),
    ∑ i : Fin 1, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_1 : R[X]) (HPow.hPow (α := R[X]) X k_1)

Tactic:
⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩

Premises used: Fin.sum_univ_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 1 → ℕ
x : Fin 1 → R
w : StrictMono k
hx : ∀ (i : Fin 1), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 1, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    1
⊢ ∃ (k_1 : ℕ) (x_1 : R) (_ : x_1 ≠ 0),
    ∑ i : Fin 1, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_1 : R[X]) (HPow.hPow (α := R[X]) X k_1)

Tactic:
exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
x : R
hx : x ≠ 0
refine_2 : card (α := ℕ) {k} = 1
refine_2₁ refine_2₂ : Eq (α := ℕ) 1 1
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).support = 1

Tactic:
rw [support_C_mul_X_pow k hx, card_singleton]

Premises used: Polynomial.support_C_mul_X_pow, Finset.card_singleton
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ #f.support = 2 ↔
    ∃ (k : ℕ) (m : ℕ) (_ : k < m) (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0),
      f =
        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)

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
refine_1 :
  ∀ (h : #f.support = 2),
    ∃ (k : ℕ) (m : ℕ) (_ : k < m) (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0),
      f =
        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)
refine_2 :
  (∃ (k : ℕ) (m : ℕ) (_ : k < m) (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0),
      f =
        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)) →
    #f.support = 2
⊢ #f.support = 2 ↔
    ∃ (k : ℕ) (m : ℕ) (_ : k < m) (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0),
      f =
        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)

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support = 2
refine_1 :
  ∀ (k : Fin 2 → ℕ) (x : Fin 2 → R) (hk : StrictMono k) (hx : ∀ (i : Fin 2), x i ≠ 0)
    (h :
      #(support.{u_1} (R := R)
            (∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
        2),
    ∃ (k_1 : ℕ) (m : ℕ) (_ : k_1 < m) (x_2 : R) (y : R) (_ : x_2 ≠ 0) (_ : y ≠ 0),
      ∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_2 : R[X]) (HPow.hPow (α := R[X]) X k_1) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)
⊢ ∃ (k : ℕ) (m : ℕ) (_ : k < m) (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0),
    f =
      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)

Tactic:
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h

Premises used: Polynomial.card_support_eq, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    2
⊢ ∃ (k_1 : ℕ) (m : ℕ) (_ : k_1 < m) (x_2 : R) (y : R) (_ : x_2 ≠ 0) (_ : y ≠ 0),
    ∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_2 : R[X]) (HPow.hPow (α := R[X]) X k_1) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)

Tactic:
⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat, Nat.zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    2
refine_1 :
  ∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1))
⊢ ∃ (k_1 : ℕ) (m : ℕ) (_ : k_1 < m) (x_2 : R) (y : R) (_ : x_2 ≠ 0) (_ : y ≠ 0),
    ∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_2 : R[X]) (HPow.hPow (α := R[X]) X k_1) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)

Tactic:
refine ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    2
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.castSucc 0)) : R[X])
        (HPow.hPow (α := R[X]) X (k (Fin.castSucc 0))) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.last 1)) : R[X]) (HPow.hPow (α := R[X]) X (k (Fin.last 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1))
⊢ ∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1))

Tactic:
rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]

Premises used: Fin.sum_univ_castSucc, Fin.sum_univ_one
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 2, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    2
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.castSucc 0)) : R[X])
        (HPow.hPow (α := R[X]) X (k (Fin.castSucc 0))) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.last 1)) : R[X]) (HPow.hPow (α := R[X]) X (k (Fin.last 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1))

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k m : ℕ
hkm : 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

Tactic:
card_support_binomial hkm.ne hx hy

Premises used: Polynomial.card_support_binomial, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k m : ℕ
hkm : 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

Tactic:
exact card_support_binomial hkm.ne hx hy

Premises used: Polynomial.card_support_binomial, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ #f.support = 3 ↔
    ∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
      f =
        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)

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
refine_1 :
  ∀ (h : #f.support = 3),
    ∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
      f =
        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)
refine_2 :
  (∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
      f =
        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)) →
    #f.support = 3
⊢ #f.support = 3 ↔
    ∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
      f =
        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)

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support = 3
refine_1 :
  ∀ (k : Fin 3 → ℕ) (x : Fin 3 → R) (hk : StrictMono k) (hx : ∀ (i : Fin 3), x i ≠ 0)
    (h :
      #(support.{u_1} (R := R)
            (∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
        3),
    ∃ (k_1 : ℕ) (m : ℕ) (n : ℕ) (_ : k_1 < m) (_ : m < n) (x_3 : R) (y : R) (z : R) (_ : x_3 ≠ 0) (_ : y ≠ 0) (_ :
      z ≠ 0),
      ∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_3 : R[X]) (HPow.hPow (α := R[X]) X k_1) +
            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)
⊢ ∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
    f =
      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)

Tactic:
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h

Premises used: Polynomial.card_support_eq, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    3
⊢ ∃ (k_1 : ℕ) (m : ℕ) (n : ℕ) (_ : k_1 < m) (_ : m < n) (x_3 : R) (y : R) (z : R) (_ : x_3 ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
    ∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_3 : R[X]) (HPow.hPow (α := R[X]) X k_1) +
          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)

Tactic:
⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2,
        ?_⟩

Premises used: Nat.lt_succ_self, Exists.intro, OfNat.ofNat, Nat.zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    3
refine_1 :
  ∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 2) : R[X]) (HPow.hPow (α := R[X]) X (k 2))
⊢ ∃ (k_1 : ℕ) (m : ℕ) (n : ℕ) (_ : k_1 < m) (_ : m < n) (x_3 : R) (y : R) (z : R) (_ : x_3 ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
    ∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_3 : R[X]) (HPow.hPow (α := R[X]) X k_1) +
          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)

Tactic:
refine
      ⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2,
        ?_⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    3
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.castSucc (Fin.castSucc 0))) : R[X])
          (HPow.hPow (α := R[X]) X (k (Fin.castSucc (Fin.castSucc 0)))) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.castSucc (Fin.last 1))) : R[X])
          (HPow.hPow (α := R[X]) X (k (Fin.castSucc (Fin.last 1)))) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.last 2)) : R[X]) (HPow.hPow (α := R[X]) X (k (Fin.last 2))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 2) : R[X]) (HPow.hPow (α := R[X]) X (k 2))
⊢ ∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 2) : R[X]) (HPow.hPow (α := R[X]) X (k 2))

Tactic:
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]

Premises used: Fin.sum_univ_castSucc, Fin.sum_univ_one
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h :
  #(support.{u_1} (R := R)
        (∑ i : Fin 3, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    3
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.castSucc (Fin.castSucc 0))) : R[X])
          (HPow.hPow (α := R[X]) X (k (Fin.castSucc (Fin.castSucc 0)))) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.castSucc (Fin.last 1))) : R[X])
          (HPow.hPow (α := R[X]) X (k (Fin.castSucc (Fin.last 1)))) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x (Fin.last 2)) : R[X]) (HPow.hPow (α := R[X]) X (k (Fin.last 2))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 0) : R[X]) (HPow.hPow (α := R[X]) X (k 0)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 1) : R[X]) (HPow.hPow (α := R[X]) X (k 1)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x 2) : R[X]) (HPow.hPow (α := R[X]) X (k 2))

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
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

Tactic:
card_support_trinomial hkm hmn hx hy hz

Premises used: Polynomial.card_support_trinomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
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

Tactic:
exact card_support_trinomial hkm hmn hx hy hz

Premises used: Polynomial.card_support_trinomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
⊢ eval₂ f 0 p = (f : (a : R) → S) (p.coeff 0)

Tactic:
simp +contextual only [eval₂_eq_sum, zero_pow_eq, mul_ite, mul_zero,
    mul_one, sum, Classical.not_not, mem_support_iff, sum_ite_eq', ite_eq_left_iff, map_zero,
    imp_true_iff]

Premises used: Finset.sum_ite_eq', ite_eq_left_iff, Classical.not_not, Polynomial.sum, mul_ite, map_zero, Polynomial.mem_support_iff, MulZeroClass.mul_zero, imp_true_iff, zero_pow_eq, mul_one, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p_1 p q : R[X]
hp : eval₂ C X p = p
hq : eval₂ C X q = q
⊢ eval₂ C X (p + q) = p + q

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
x : R
rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X n) = (monomial n : (a : R) → R[X]) x
rw₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X n) = x • HPow.hPow (α := R[X]) X n
rw₂ rw₃ : x • HPow.hPow (α := R[X]) X n = x • HPow.hPow (α := R[X]) X n
⊢ Eq.{u + 1} (α := R[X]) (eval₂ C X ((monomial n : (a : R) → R[X]) x)) ((monomial n : (a : R) → R[X]) x)

Tactic:
rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']

Premises used: Polynomial.C_mul', Polynomial.eval₂_monomial, Polynomial.smul_X_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeff 0 = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
symm : eval 0 p = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0
⊢ p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0 = eval 0 p

Tactic:
symm
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : (p.sum fun (e : ℕ) (a : R) ↦ a * HPow.hPow (α := R) 0 e) = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0
⊢ eval 0 p = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0

Tactic:
rw [eval_eq_sum]

Premises used: Polynomial.eval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : ℕ
h : b ∈ p.support
hb : b ≠ 0
⊢ Eq.{u + 1} (α := R) ((fun (e : ℕ) (a : R) ↦ a * HPow.hPow (α := R) 0 e) b (p.coeff b)) 0

Tactic:
simp [zero_pow hb]

Premises used: zero_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ 0 ∉ p.support → Eq.{u + 1} (α := R) ((fun (e : ℕ) (a : R) ↦ a * HPow.hPow (α := R) 0 e) 0 (p.coeff 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ a * HPow.hPow (α := R) 0 e) = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0

Tactic:
exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow hb]) (by simp)

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.IsRoot 0 ↔ eval 0 p = 0
rw₁ rw₂ : eval 0 p = 0 ↔ eval 0 p = 0
⊢ p.IsRoot 0 ↔ p.coeff 0 = 0

Tactic:
rw [coeff_zero_eq_eval_zero, IsRoot]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.IsRoot
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
n : ℕ
rw :
  Eq.{v + 1} (α := S)
    (∑ n_1 ∈ p.support,
        (HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) (p.coeff n_1) : S[X])
              (HPow.hPow (α := S[X]) X n_1)).coeff
          n :
      S)
    ((f : (a : R) → S) (p.coeff n) : S)
⊢ (map f p).coeff n = (f : (a : R) → S) (p.coeff n)

Tactic:
rw [map, eval₂_def, coeff_sum, sum]

Premises used: Polynomial.sum, Polynomial.eval₂_def, Polynomial.coeff_sum, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ Eq.{v + 1} (α := S)
    (∑ n_1 ∈ p.support,
        (HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) (p.coeff n_1) : S[X])
              (HPow.hPow (α := S[X]) X n_1)).coeff
          n :
      S)
    ((f : (a : R) → S) (p.coeff n) : S)

Tactic:
simp_all