awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
⊢ coeff (trinomial k m n u v w) n = w
have rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
  w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
⊢ coeff (trinomial k m n u v w) n = w
have rw₃ : (if n = k then u else 0) + (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
  w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
⊢ coeff (trinomial k m n u v w) n = w
have rw₄ : ((if n = k then u else 0) + if n = m then v else 0) +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
  w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
⊢ coeff (trinomial k m n u v w) n = w
have rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
⊢ coeff (trinomial k m n u v w) n = w
have rw₆ : ((0 + if n = m then v else 0) + if n = n then w else 0) = w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
rw₆ : ((0 + if n = m then v else 0) + if n = n then w else 0) = w
⊢ coeff (trinomial k m n u v w) n = w
have rw₇ : (HAdd.hAdd (α := R) 0 0 + if n = n then w else 0) = w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
rw₆ : ((0 + if n = m then v else 0) + if n = n then w else 0) = w
rw₇ : (HAdd.hAdd (α := R) 0 0 + if n = n then w else 0) = w
⊢ coeff (trinomial k m n u v w) n = w
have rw₈ : HAdd.hAdd (α := R) 0 0 + w = w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
rw₆ : ((0 + if n = m then v else 0) + if n = n then w else 0) = w
rw₇ : (HAdd.hAdd (α := R) 0 0 + if n = n then w else 0) = w
rw₈ : HAdd.hAdd (α := R) 0 0 + w = w
⊢ coeff (trinomial k m n u v w) n = w
have rw₉ : 0 + w = w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₃ :
  (if n = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₄ :
  ((if n = k then u else 0) + if n = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
    w
rw₅ : (((if n = k then u else 0) + if n = m then v else 0) + if n = n then w else 0) = w
rw₆ : ((0 + if n = m then v else 0) + if n = n then w else 0) = w
rw₇ : (HAdd.hAdd (α := R) 0 0 + if n = n then w else 0) = w
rw₈ : HAdd.hAdd (α := R) 0 0 + w = w
rw₉ : 0 + w = w
⊢ coeff (trinomial k m n u v w) n = w
have rw₁₀ : w = w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ coeff (trinomial k m n u v w) m = v
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
    m =
  v
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      m =
    v
⊢ coeff (trinomial k m n u v w) m = v
have rw₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
      m +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
  v
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      m =
    v
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
⊢ coeff (trinomial k m n u v w) m = v
have rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
  v
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      m =
    v
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
⊢ coeff (trinomial k m n u v w) m = v
have rw₃ : (if m = k then u else 0) + (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
  v
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      m =
    v
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₃ :
  (if m = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
⊢ coeff (trinomial k m n u v w) m = v
have rw₄ : ((if m = k then u else 0) + if m = m then v else 0) +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
  v
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      m =
    v
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₃ :
  (if m = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
rw₄ :
  ((if m = k then u else 0) + if m = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m =
    v
⊢ coeff (trinomial k m n u v w) m = v
have rw₅ : (((if m = k then u else 0) + if m = m then v else 0) + if m = n then w else 0) = v
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]