awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
⊢ #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)
have 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
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
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)
have 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)
Tactic: obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).support = 1
have refine_2 : card (α := ℕ) {k} = 1
Tactic: rw [support_C_mul_X_pow k hx, card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
x : R
hx : x ≠ 0
refine_2 : card (α := ℕ) {k} = 1
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).support = 1
have refine_2₁ : Eq (α := ℕ) 1 1
Tactic: rw [support_C_mul_X_pow k hx, card_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
have 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)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
⊢ #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)
have 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
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
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)
have 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)
Tactic: obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
have 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))
Tactic: refine ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ ∑ 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))
have 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))
Tactic: rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
have 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)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
⊢ #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)
have 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
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
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)
have 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)
Tactic: obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
have 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))
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,
        ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ ∑ 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))
have 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))
Tactic: rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
x : R
⊢ Eq.{u + 1} (α := R[X]) (eval₂ C X ((monomial n : (a : R) → R[X]) x)) ((monomial n : (a : R) → R[X]) x)
have 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
Tactic: rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
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
⊢ Eq.{u + 1} (α := R[X]) (eval₂ C X ((monomial n : (a : R) → R[X]) x)) ((monomial n : (a : R) → R[X]) x)
have 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
Tactic: rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
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
⊢ Eq.{u + 1} (α := R[X]) (eval₂ C X ((monomial n : (a : R) → R[X]) x)) ((monomial n : (a : R) → R[X]) x)
have rw₂ : x • HPow.hPow (α := R[X]) X n = x • HPow.hPow (α := R[X]) X n
Tactic: rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0 = eval 0 p
have symm : eval 0 p = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ eval 0 p = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0
have rw : (p.sum fun (e : ℕ) (a : R) ↦ a * HPow.hPow (α := R) 0 e) = p.coeff 0 * HPow.hPow (α := R) (β := ℕ) 0 0
Tactic: rw [eval_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.IsRoot 0 ↔ p.coeff 0 = 0
have rw : p.IsRoot 0 ↔ eval 0 p = 0
Tactic: rw [coeff_zero_eq_eval_zero, IsRoot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.IsRoot 0 ↔ eval 0 p = 0
⊢ p.IsRoot 0 ↔ p.coeff 0 = 0
have rw₁ : eval 0 p = 0 ↔ eval 0 p = 0
Tactic: rw [coeff_zero_eq_eval_zero, IsRoot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ (map f p).coeff n = (f : (a : R) → S) (p.coeff n)
have 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)
Tactic: rw [map, eval₂_def, coeff_sum, sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).coeff = (⇑f : (a : R) → S) ∘ p.coeff
have h : ∀ (n : ℕ), (map f p).coeff n = ((⇑f : (a : R) → S) ∘ p.coeff) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n : ℕ
inst : Semiring R_1
p_1 q_1 r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h :
  Eq (α := (i : ι) → (R i)[X])
    ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        p :
      (i : ι) → (R i)[X])
    ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        q :
      (i : ι) → (R i)[X])
⊢ p = q
have a₁ : ∀ (n : ℕ) (i : ι), p.coeff n i = q.coeff n i
Tactic: ext n i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : Membership.mem (γ := Set ℕ) (Function.support (M := (i : ι) → R i) fun (n : ℕ) (i : ι) ↦ (p i).coeff n) n
⊢ Membership.mem (γ := Set ℕ) (⋃ (i : ι), (↑(p i).support : Set ℕ)) n
have simp : ∀ (hn : Ne (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0), ∃ (i : ι), (p i).coeff n ≠ 0
Tactic: simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : Ne (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0
⊢ ∃ (i : ι), (p i).coeff n ≠ 0
have contrapose! : ∀ (hn : ∀ (i : ι), (p i).coeff n = 0), Eq (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
⊢ (Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
        (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
      { toFinsupp := Finsupp.ofSupportFinite (fun (n : ℕ) (i : ι) ↦ (p i).coeff n) ⋯ } =
    p
have h : ∀ (i : ι) (n : ℕ),
  coeff
      ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        { toFinsupp := Finsupp.ofSupportFinite (fun (n : ℕ) (i : ι) ↦ (p i).coeff n) sorry } i)
      n =
    (p i).coeff n
Tactic: ext i n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
h : map f p = map f q
m : ℕ
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff m) : S) ((f : (a : R) → S) (q.coeff m) : S)
have rw : (map f p).coeff m = (f : (a : R) → S) (q.coeff m)
Tactic: rw [← coeff_map f, ← coeff_map f, h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
h : map f p = map f q
m : ℕ
rw : (map f p).coeff m = (f : (a : R) → S) (q.coeff m)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff m) : S) ((f : (a : R) → S) (q.coeff m) : S)
have rw₁ : (map f p).coeff m = (map f q).coeff m
Tactic: rw [← coeff_map f, ← coeff_map f, h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
h : map f p = map f q
m : ℕ
rw : (map f p).coeff m = (f : (a : R) → S) (q.coeff m)
rw₁ : (map f p).coeff m = (map f q).coeff m
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff m) : S) ((f : (a : R) → S) (q.coeff m) : S)
have rw₂ : (map f q).coeff m = (map f q).coeff m
Tactic: rw [← coeff_map f, ← coeff_map f, h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : S[X]
n : ℕ
s : S
r : R
hr : (f : (a : R) → S) r = s
⊢ map f ((monomial n : (a : R) → R[X]) r) = (monomial n : (a : S) → S[X]) s
have rw : Eq.{v + 1} (α := S[X]) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
  ((monomial n : (a : S) → S[X]) s : S[X])
Tactic: rw [map_monomial f, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : S[X]
n : ℕ
s : S
r : R
hr : (f : (a : R) → S) r = s
rw :
  Eq.{v + 1} (α := S[X]) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
    ((monomial n : (a : S) → S[X]) s : S[X])
⊢ map f ((monomial n : (a : R) → R[X]) r) = (monomial n : (a : S) → S[X]) s
have rw₁ : Eq (α := S[X]) ((monomial n : (a : S) → S[X]) s : S[X]) ((monomial n : (a : S) → S[X]) s : S[X])
Tactic: rw [map_monomial f, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T
g : S →+* T
x : T
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p
have rw : eval x (map g (map f p)) = eval₂ (g.comp f) x p
Tactic: rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T
g : S →+* T
x : T
rw : eval x (map g (map f p)) = eval₂ (g.comp f) x p
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p
have rw₁ : eval x (map g (map f p)) = eval x (map (g.comp f) p)
Tactic: rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T
g : S →+* T
x : T
rw : eval x (map g (map f p)) = eval₂ (g.comp f) x p
rw₁ : eval x (map g (map f p)) = eval x (map (g.comp f) p)
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p
have rw₂ : eval x (map (g.comp f) p) = eval x (map (g.comp f) p)
Tactic: rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]