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
      k =
    u
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
        k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₃ :
  (if k = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₄ :
  ((if k = k then u else 0) + if k = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₅ : (((if k = k then u else 0) + if k = m then v else 0) + if k = n then w else 0) = u
rw₆ : ((u + if k = m then v else 0) + if k = n then w else 0) = u
rw₇ : (u + 0 + if k = n then w else 0) = u
rw₈ : u + 0 + 0 = u
⊢ coeff (trinomial k m n u v w) k = u
have rw₉ : u + 0 = u
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_pos rfl, if_neg hkm.ne, if_neg (hkm.trans hmn).ne, add_zero, 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
      k =
    u
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
        k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₃ :
  (if k = k then u else 0) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₄ :
  ((if k = k then u else 0) + if k = m then v else 0) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff k =
    u
rw₅ : (((if k = k then u else 0) + if k = m then v else 0) + if k = n then w else 0) = u
rw₆ : ((u + if k = m then v else 0) + if k = n then w else 0) = u
rw₇ : (u + 0 + if k = n then w else 0) = u
rw₈ : u + 0 + 0 = u
rw₉ : u + 0 = u
⊢ coeff (trinomial k m n u v w) k = u
have rw₁₀ : u = u
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_pos rfl, if_neg hkm.ne, if_neg (hkm.trans hmn).ne, add_zero, 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
hw : w ≠ 0
⊢ natDegree (trinomial k m n u v w) = n
have fun : ∀ (i : ℕ) (h : i ∈ support (trinomial k m n u v w)), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
Tactic: refine
    natDegree_eq_of_degree_eq_some
      ((Finset.sup_le fun i h => ?_).antisymm <|
        le_degree_of_ne_zero <| by rwa [trinomial_leading_coeff' hkm hmn])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ support (trinomial k m n u v w)
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have h₁ : Membership.mem (γ := Finset ℕ) {k, m, n} i
Tactic: replace h := support_trinomial' k m n u v w h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : Membership.mem (γ := Finset ℕ) {k, m, n} i
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have h₁ : i = k ∨ i = m ∨ i = n
Tactic: rw [mem_insert, mem_insert, mem_singleton] at h
Cleared hypotheses: h
-- 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
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have inl : ∀ (hkm : i < m), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
Tactic: rcases h with (rfl | rfl | rfl)
Cleared hypotheses: k, hkm, h
-- 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
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
inl : ∀ (hkm : i < m), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have inr : ∀ (hkm : k < i) (hmn : i < n), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
Tactic: rcases h with (rfl | rfl | rfl)
Cleared hypotheses: m, hkm, hmn, h
-- 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
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
inl : ∀ (hkm : i < m), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
inr : ∀ (hkm : k < i) (hmn : i < n), (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ (↑i : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have inr₁ : ∀ (hmn : m < i), (↑i : WithBot ℕ) ≤ (↑i : WithBot ℕ)
Tactic: rcases h with (rfl | rfl | rfl)
Cleared hypotheses: n, hmn, h
-- 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
hu : u ≠ 0
⊢ natTrailingDegree (trinomial k m n u v w) = k
have fun : ∀ (i : ℕ) (h : i ∈ support (trinomial k m n u v w)), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
Tactic: refine
    natTrailingDegree_eq_of_trailingDegree_eq_some
      ((Finset.le_inf fun i h => ?_).antisymm <|
          trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ support (trinomial k m n u v w)
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
have h₁ : Membership.mem (γ := Finset ℕ) {k, m, n} i
Tactic: replace h := support_trinomial' k m n u v w h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : Membership.mem (γ := Finset ℕ) {k, m, n} i
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
have h₁ : i = k ∨ i = m ∨ i = n
Tactic: rw [mem_insert, mem_insert, mem_singleton] at h
Cleared hypotheses: h
-- 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
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
have inl : ∀ (hkm : i < m), (↑i : ℕ∞) ≤ (↑i : WithTop ℕ)
Tactic: rcases h with (rfl | rfl | rfl)
Cleared hypotheses: k, hkm, h
-- 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
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
inl : ∀ (hkm : i < m), (↑i : ℕ∞) ≤ (↑i : WithTop ℕ)
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
have inr : ∀ (hkm : k < i) (hmn : i < n), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
Tactic: rcases h with (rfl | rfl | rfl)
Cleared hypotheses: m, hkm, hmn, h
-- 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
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
inl : ∀ (hkm : i < m), (↑i : ℕ∞) ≤ (↑i : WithTop ℕ)
inr : ∀ (hkm : k < i) (hmn : i < n), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
⊢ (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
have inr₁ : ∀ (hmn : m < i), (↑k : ℕ∞) ≤ (↑i : WithTop ℕ)
Tactic: rcases h with (rfl | rfl | rfl)
Cleared hypotheses: n, hmn, h
-- 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
hw : w ≠ 0
⊢ leadingCoeff (trinomial k m n u v w) = w
have rw : coeff (trinomial k m n u v w) (natDegree (trinomial k m n u v w)) = w
Tactic: rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]
-- 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
hw : w ≠ 0
rw : coeff (trinomial k m n u v w) (natDegree (trinomial k m n u v w)) = w
⊢ leadingCoeff (trinomial k m n u v w) = w
have rw₁ : coeff (trinomial k m n u v w) n = w
Tactic: rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]
-- 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
hw : w ≠ 0
rw : coeff (trinomial k m n u v w) (natDegree (trinomial k m n u v w)) = w
rw₁ : coeff (trinomial k m n u v w) n = w
⊢ leadingCoeff (trinomial k m n u v w) = w
have rw₂ : w = w
Tactic: rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]
-- 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
hu : u ≠ 0
⊢ trailingCoeff (trinomial k m n u v w) = u
have rw : coeff (trinomial k m n u v w) (natTrailingDegree (trinomial k m n u v w)) = u
Tactic: rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]
-- 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
hu : u ≠ 0
rw : coeff (trinomial k m n u v w) (natTrailingDegree (trinomial k m n u v w)) = u
⊢ trailingCoeff (trinomial k m n u v w) = u
have rw₁ : coeff (trinomial k m n u v w) k = u
Tactic: rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]
-- 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
hu : u ≠ 0
rw : coeff (trinomial k m n u v w) (natTrailingDegree (trinomial k m n u v w)) = u
rw₁ : coeff (trinomial k m n u v w) k = u
⊢ trailingCoeff (trinomial k m n u v w) = u
have rw₂ : u = u
Tactic: rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
⊢ Monic (trinomial k m n u v 1)
have a : Nontrivial R
Tactic: nontriviality R
-- 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
hu : u ≠ 0
hw : w ≠ 0
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- 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
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- 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
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₂ : reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- 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
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₂ :
  reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₃ : reflect n (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- 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
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₂ :
  reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₃ : reflect n (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₄ : reflect n
      (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)) *
    HPow.hPow (α := R[X]) X k =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- 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
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₂ :
  reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₃ : reflect n (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₄ :
  reflect n
        (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)) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₅ : (reflect n
        (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)) +
      reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
    HPow.hPow (α := R[X]) X k =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- 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
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₂ :
  reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₃ : reflect n (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₄ :
  reflect n
        (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)) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₅ :
  (reflect n
          (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)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₆ : (reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
      reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
    HPow.hPow (α := R[X]) X k =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]