awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
rw :
  (lift (evalRingHom x) y ⋯ : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g
⊢ (evalEval h : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g
have rw₁ : eval₂ (evalRingHom x) y g = Polynomial.evalEval x y g
Tactic: rw [evalEval, lift_mk, eval₂_evalRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
rw :
  (lift (evalRingHom x) y ⋯ : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g
rw₁ : eval₂ (evalRingHom x) y g = Polynomial.evalEval x y g
⊢ (evalEval h : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g
have rw₂ : Polynomial.evalEval x y g = Polynomial.evalEval x y g
Tactic: rw [evalEval, lift_mk, eval₂_evalRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
⊢ (p.cancelLeads q).natDegree < q.natDegree
have pos : ∀ (hp : p = 0), (p.cancelLeads q).natDegree < q.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
pos : ∀ (hp : p = 0), (p.cancelLeads q).natDegree < q.natDegree
⊢ (p.cancelLeads q).natDegree < q.natDegree
have neg : ∀ (hp : ¬p = 0), (p.cancelLeads q).natDegree < q.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : p = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree
have h₁ : (p.cancelLeads q).natDegree = 0
Tactic: convert! hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p)).natDegree <
  q.natDegree
Tactic: rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
have pos : ∀
  (h0 :
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
Tactic: by_cases h0 :
    C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
pos :
  ∀
    (h0 :
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p) =
        0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p)).natDegree <
      q.natDegree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
have neg : ∀
  (h0 :
    ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p) =
        0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
Tactic: by_cases h0 :
    C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p)).natDegree ≤
  q.natDegree
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≤
    q.natDegree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
have neg₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p)).natDegree ≠
  q.natDegree
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≤
    q.natDegree
have neg : q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
⊢ q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree
have neg : q.natDegree ≤ q.natDegree
Tactic: rwa [Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≠
    q.natDegree
have neg : ∀
  (h0 :
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p)).natDegree =
      q.natDegree),
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p) =
    0
Tactic: contrapose h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p) =
    0
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (p * HPow.hPow (α := R[X]) X (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree))).coeff
    (p.natDegree + (q.natDegree - p.natDegree)) =
  0
Tactic: rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
      add_comm _ p.natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (p * HPow.hPow (α := R[X]) X (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0
have neg : p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Tactic: simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
have neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Tactic: rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
have neg₁ : p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Tactic: rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₁ : p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
have neg₂ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Tactic: rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₁ : p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₂ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.coeff p.natDegree) = 0
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
have neg₃ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
Tactic: rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₁ : p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₂ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₃ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
have neg₄ : q.leadingCoeff * p.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
Tactic: rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CancelLeads (goal)
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₁ : p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₂ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₃ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
neg₄ : q.leadingCoeff * p.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
have neg₅ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Cardinal (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ #(AddMonoidAlgebra R ℕ) = max #R ℵ₀
have rw : max (#R) (lift.{u, 0} #ℕ) = max #R ℵ₀
Tactic: rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Cardinal (goal)
Goal:
R : Type u
inst : Semiring R
⊢ #R[X] ≤ max #R ℵ₀
have inl : Subsingleton R → #R[X] ≤ max #R ℵ₀
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Cardinal (goal)
Goal:
R : Type u
inst : Semiring R
inl : Subsingleton R → #R[X] ≤ max #R ℵ₀
⊢ #R[X] ≤ max #R ℵ₀
have inr : Nontrivial R → #R[X] ≤ max #R ℵ₀
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
⊢ (p + q).coeff n = p.coeff n + q.coeff n
have rcases : ∀ (toFinsupp : R[ℕ]),
  ({ toFinsupp := toFinsupp : R[X] } + q).coeff n = { toFinsupp := toFinsupp : R[X] }.coeff n + q.coeff n
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
q : R[X]
n : ℕ
toFinsupp : R[ℕ]
⊢ ({ toFinsupp := toFinsupp : R[X] } + q).coeff n = { toFinsupp := toFinsupp : R[X] }.coeff n + q.coeff n
have rcases : ∀ (toFinsupp_1 : R[ℕ]),
  ({ toFinsupp := toFinsupp : R[X] } + { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n + { toFinsupp := toFinsupp_1 : R[X] }.coeff n
Tactic: rcases q with ⟨⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
⊢ ({ toFinsupp := toFinsupp : R[X] } + { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n + { toFinsupp := toFinsupp_1 : R[X] }.coeff n
have simp_rw : (toFinsupp + toFinsupp_1 : (a : ℕ) → R) n =
  HAdd.hAdd (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)
Tactic: simp_rw [← ofFinsupp_add, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
⊢ i ∈ p.support
have rw : ∀ (hi : (r • p).coeff i ≠ 0), p.coeff i ≠ 0
Tactic: rw [mem_support_iff] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : (r • p).coeff i ≠ 0
⊢ p.coeff i ≠ 0
have contrapose : ∀ (hi : p.coeff i = 0), (r • p).coeff i = 0
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ #(p * q).support = #(p.toFinsupp * q.toFinsupp).support
have rw : #(p * q).toFinsupp.support = #(p.toFinsupp * q.toFinsupp).support
Tactic: rw [← support_toFinsupp, toFinsupp_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rw : #(p * q).toFinsupp.support = #(p.toFinsupp * q.toFinsupp).support
⊢ #(p * q).support = #(p.toFinsupp * q.toFinsupp).support
have rw₁ : #(p.toFinsupp * q.toFinsupp).support = #(p.toFinsupp * q.toFinsupp).support
Tactic: rw [← support_toFinsupp, toFinsupp_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ #(p * q).support ≤ #p.support * #q.support
have calc : #(p * q).support = #(p.toFinsupp * q.toFinsupp).support
Tactic: calc #(p * q).support
    _ = #(p.toFinsupp * q.toFinsupp).support := by rw [← support_toFinsupp, toFinsupp_mul]
    _ ≤ #(p.toFinsupp.support + q.toFinsupp.support) :=
      Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)
    _ ≤ #p.support * #q.support := Finset.card_image₂_le ..