awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
rw₁ :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X]) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
have rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff = a
Tactic: rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
rw₁ :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X]) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff =
    a
rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff = a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
have rw₃ : a = a
Tactic: rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).degree =
    3
have rw : Eq (α := WithBot ℕ) (↑3 : WithBot ℕ) 3
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
    degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    degree_C_mul_X_pow 3 ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
  a
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
have rw₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X]))).leadingCoeff =
  a
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
            ((C : (a : R) → R[X]) d : R[X]))).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
have rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
      HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
  a
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
            ((C : (a : R) → R[X]) d : R[X]))).leadingCoeff =
    a
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
have rw₃ : (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X]) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff =
  a
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
            ((C : (a : R) → R[X]) d : R[X]))).leadingCoeff =
    a
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₃ :
  (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X]) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
have rw₄ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff = a
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
            ((C : (a : R) → R[X]) d : R[X]))).leadingCoeff =
    a
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₃ :
  (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X]) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff =
    a
rw₄ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff = a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
have rw₅ : a = a
Tactic: rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
have inl : AddMonoidAlgebra.supDegree.{u, 0, 0} (R := R) id (toFinsupp 0) = natDegree.{u} (R := R) 0
Tactic: obtain rfl | h := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
inl : AddMonoidAlgebra.supDegree.{u, 0, 0} (R := R) id (toFinsupp 0) = natDegree.{u} (R := R) 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
have inr : ∀ (h : p ≠ 0), AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
Tactic: obtain rfl | h := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
have inr : (↑(AddMonoidAlgebra.supDegree id p.toFinsupp) : WithBot ℕ) = (↑p.natDegree : WithBot ℕ)
Tactic: apply WithBot.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ (↑(AddMonoidAlgebra.supDegree id p.toFinsupp) : WithBot ℕ) = (↑p.natDegree : WithBot ℕ)
have inr : p.toFinsupp.support.Nonempty
Tactic: rw [← AddMonoidAlgebra.supDegree_withBot_some_comp, Function.comp_id, supDegree_eq_degree,
    degree_eq_natDegree h, Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.support.Nonempty
have inr : p.support.Nonempty
Tactic: rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
inr : p.support.Nonempty
⊢ p.toFinsupp.support.Nonempty
have inr₁ : p.support ≠ ∅
Tactic: rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
inr : p.support.Nonempty
inr₁ : p.support ≠ ∅
⊢ p.toFinsupp.support.Nonempty
have inr₂ : ¬p.support = ∅
Tactic: rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
inr : p.support.Nonempty
inr₁ : p.support ≠ ∅
inr₂ : ¬p.support = ∅
⊢ p.toFinsupp.support.Nonempty
have inr₃ : ¬p = 0
Tactic: rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)
have this : p.support ⊆ range n
Tactic: have := supp_subset_range hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
this : p.support ⊆ range n
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)
have simp : Eq.{v + 1} (α := S) (∑ x ∈ p.toFinsupp.support, f x ((p.toFinsupp : (a : ℕ) → R) x))
  (∑ x ∈ range n, f x ((p.toFinsupp : (a : ℕ) → R) x))
Tactic: simp only [Polynomial.sum, support, coeff] at this ⊢
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
have pos : ∀ (hp : p = 0), ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
pos : ∀ (hp : p = 0), ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
have neg : ∀ (hp : ¬p = 0), ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : p = 0
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
have pos : ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) univ x → f (↑x : ℕ) (coeff 0 (↑x : ℕ)) = 0
Tactic: rw [hp, sum_zero_index, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : ¬p = 0
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
have neg : Eq.{v + 1} (α := S) (∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ))) (∑ a ∈ range n, f a (p.coeff a))
Tactic: rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
    Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : ¬p = 0
neg : Eq.{v + 1} (α := S) (∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ))) (∑ a ∈ range n, f a (p.coeff a))
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
have neg₁ : Eq.{v + 1} (α := S) (∑ i ∈ range n, f i (p.coeff i)) (∑ a ∈ range n, f a (p.coeff a))
Tactic: rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
    Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ #p.support ≤ p.natDegree + 1
have rw : #p.support ≤ #(range (p.natDegree + 1))
Tactic: rw [← Finset.card_range (p.natDegree + 1)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.support.Nonempty ↔ p ≠ 0
have rw : p.support.Nonempty ↔ ¬p = 0
Tactic: rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.support.Nonempty ↔ ¬p = 0
⊢ p.support.Nonempty ↔ p ≠ 0
have rw₁ : p.support ≠ ∅ ↔ ¬p = 0
Tactic: rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.support.Nonempty ↔ ¬p = 0
rw₁ : p.support ≠ ∅ ↔ ¬p = 0
⊢ p.support.Nonempty ↔ p ≠ 0
have rw₂ : ¬p.support = ∅ ↔ ¬p = 0
Tactic: rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.support.Nonempty ↔ ¬p = 0
rw₁ : p.support ≠ ∅ ↔ ¬p = 0
rw₂ : ¬p.support = ∅ ↔ ¬p = 0
⊢ p.support.Nonempty ↔ p ≠ 0
have rw₃ : ¬p.support = ∅ ↔ ¬p.support = ∅
Tactic: rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Support (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.natDegree ∈ p.support
have rw : p.coeff p.natDegree ≠ 0
Tactic: rw [mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.trailingDegree = (↑n : ℕ∞) ↔ p.natTrailingDegree = n
have rw : Eq (α := ℕ∞) (↑p.natTrailingDegree : ℕ∞) (↑n : ℕ∞) ↔ p.natTrailingDegree = n
Tactic: rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : Eq (α := ℕ∞) (↑p.natTrailingDegree : ℕ∞) (↑n : ℕ∞) ↔ p.natTrailingDegree = n
⊢ p.trailingDegree = (↑n : ℕ∞) ↔ p.natTrailingDegree = n
have rw₁ : p.natTrailingDegree = n ↔ p.natTrailingDegree = n
Tactic: rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
⊢ p.trailingDegree = (↑n : ℕ∞) ↔ p.natTrailingDegree = n
have rw : p.trailingDegree = (↑n : ℕ∞) ↔ p.trailingDegree.toNat = n
Tactic: rw [natTrailingDegree, ENat.toNat_eq_iff hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
rw : p.trailingDegree = (↑n : ℕ∞) ↔ p.trailingDegree.toNat = n
⊢ p.trailingDegree = (↑n : ℕ∞) ↔ p.natTrailingDegree = n
have rw₁ : p.trailingDegree = (↑n : ℕ∞) ↔ p.trailingDegree = (↑n : ℕ∞)
Tactic: rw [natTrailingDegree, ENat.toNat_eq_iff hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.trailingDegree.toNat = q.trailingDegree.toNat
have rw : q.trailingDegree.toNat = q.trailingDegree.toNat
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 ↔ p = 0
have mp : p.coeff p.natTrailingDegree = 0 → p = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
mp : p.coeff p.natTrailingDegree = 0 → p = 0
⊢ p.coeff p.natTrailingDegree = 0 ↔ p = 0
have mpr : p = 0 → p.coeff p.natTrailingDegree = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
⊢ p = 0
have mp : ∀ (hp : ¬p = 0), False
Tactic: by_contra hp