awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
⊢ p.natDegree < q.natDegree
have neg : ∀ (hpq : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : ¬q = 0), p.natDegree < q.natDegree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq
Cleared hypotheses: hpq, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
neg : ∀ (hpq : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : ¬q = 0), p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree
have neg₁ : ∀ (hpq : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)) (hq : ¬q = 0),
  p.natDegree < q.natDegree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq
Cleared hypotheses: hpq, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
neg : ∀ (hpq : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : ¬q = 0), p.natDegree < q.natDegree
neg₁ :
  ∀ (hpq : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)) (hq : ¬q = 0),
    p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree
have neg₂ : ∀ (hpq : p.natDegree < q.natDegree) (hq : ¬q = 0), p.natDegree < q.natDegree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq
Cleared hypotheses: hpq, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.coeff n = 0
have h₁ : p.degree < (↑n : WithBot ℕ)
Tactic: apply coeff_eq_zero_of_degree_lt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.degree < (↑n : WithBot ℕ)
have pos : ∀ (hp : p = 0), p.degree < (↑n : WithBot ℕ)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
pos : ∀ (hp : p = 0), p.degree < (↑n : WithBot ℕ)
⊢ p.degree < (↑n : WithBot ℕ)
have neg : ∀ (hp : ¬p = 0), p.degree < (↑n : WithBot ℕ)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
⊢ p.degree < (↑n : WithBot ℕ)
have pos : ∀ (h : natDegree.{u} (R := R) 0 < n), degree.{u} (R := R) 0 < (↑n : WithBot ℕ)
Tactic: subst hp
Cleared hypotheses: p, h, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < (↑n : WithBot ℕ)
have neg : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree hp, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
have refine : (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i
Tactic: refine Iff.trans Polynomial.ext_iff ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i
have refine : ∀ (i : ℕ) (h : i ≤ n → p.coeff i = q.coeff i), p.coeff i = q.coeff i
Tactic: refine forall_congr' fun i => ⟨fun h _ => h, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
⊢ p.coeff i = q.coeff i
have k : n < i
Tactic: refine (le_or_gt i n).elim h fun k => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
⊢ (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n
have pos : ∀ (h : n < 1 + p.natDegree), p.coeff n = p.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
pos : ∀ (h : n < 1 + p.natDegree), p.coeff n = p.coeff n
⊢ (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n
have neg : ∀ (h : ¬n < 1 + p.natDegree), 0 = p.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
⊢ p.degree ≠ ⊥
have rwa : ¬p.degree = ⊥
Tactic: rwa [Ne, Polynomial.degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
rwa : ¬p.degree = ⊥
⊢ p.degree ≠ ⊥
have rwa₁ : ¬p = 0
Tactic: rwa [Ne, Polynomial.degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
⊢ p.degree < q.degree
have pos : ∀ (hp : p = 0), p.degree < q.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
pos : ∀ (hp : p = 0), p.degree < q.degree
⊢ p.degree < q.degree
have neg : ∀ (hp : ¬p = 0), p.degree < q.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ p.degree < q.degree
have pos : ⊥ < q.degree
Tactic: simp only [hp, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ ⊥ < q.degree
have pos : q.degree ≠ ⊥
Tactic: rw [bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
⊢ p.degree < q.degree
have neg : (↑p.natDegree : WithBot ℕ) < q.degree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
neg : (↑p.natDegree : WithBot ℕ) < q.degree
⊢ p.degree < q.degree
have neg₁ : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
⊢ p.natDegree < q.natDegree
have hq : q ≠ 0
Tactic: have hq : q ≠ 0 := ne_zero_of_degree_gt h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
⊢ p.natDegree < q.natDegree
have rwa : ∀ (h : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : q ≠ 0), p.natDegree < q.natDegree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h
Cleared hypotheses: h, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
rwa : ∀ (h : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : q ≠ 0), p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree
have rwa₁ : ∀ (h : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)) (hq : q ≠ 0),
  p.natDegree < q.natDegree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h
Cleared hypotheses: h, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
rwa : ∀ (h : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : q ≠ 0), p.natDegree < q.natDegree
rwa₁ :
  ∀ (h : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)) (hq : q ≠ 0),
    p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree
have rwa₂ : ∀ (h : p.natDegree < q.natDegree) (hq : q ≠ 0), p.natDegree < q.natDegree
Tactic: rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h
Cleared hypotheses: h, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)
have a : p.coeff 0 = coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
a : p.coeff 0 = coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)
have a₁ : ∀ (n : ℕ), p.coeff (n + 1) = coeff ((C : (a : R) → R[X]) (p.coeff 0)) (n + 1)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = coeff ((C : (a : R) → R[X]) (p.coeff 0)) (n + 1)
have a : p.degree < (↑(n + 1) : WithBot ℕ)
Tactic: rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).coeff p.natDegree ≠ 0
have rw : p.coeff p.natDegree ≠ 0
Tactic: rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ (p + q).degree = q.degree
have rw : (q + p).degree = q.degree
Tactic: rw [add_comm, degree_add_eq_left_of_degree_lt h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
rw : (q + p).degree = q.degree
⊢ (p + q).degree = q.degree
have rw₁ : q.degree = q.degree
Tactic: rw [add_comm, degree_add_eq_left_of_degree_lt h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have inl : (HAdd.hAdd (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).natDegree = natDegree.{u} (R := R) 0
Tactic: rcases eq_or_ne p 0 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inl :
  (HAdd.hAdd (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).natDegree = natDegree.{u} (R := R) 0
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have inr : ∀ (hp : p ≠ 0), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
Tactic: rcases eq_or_ne p 0 with rfl | hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have pos : ∀ (hpd : p.degree ≤ 0), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
Tactic: by_cases! hpd : p.degree ≤ 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
pos : ∀ (hpd : p.degree ≤ 0), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have neg : ∀ (hpd : 0 < p.degree), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
Tactic: by_cases! hpd : p.degree ≤ 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have pos : (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      ((C : (a : R) → R[X]) a : R[X])).natDegree =
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
Tactic: rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
pos :
  (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        ((C : (a : R) → R[X]) a : R[X])).natDegree =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have pos₁ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + a)) =
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
Tactic: rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
pos :
  (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        ((C : (a : R) → R[X]) a : R[X])).natDegree =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
pos₁ :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + a)) =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have pos₂ : 0 = natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
Tactic: rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
pos :
  (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        ((C : (a : R) → R[X]) a : R[X])).natDegree =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
pos₁ :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + a)) =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
pos₂ : 0 = natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have hpd₁ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) < p.natDegree
Tactic: rw [degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd
Cleared hypotheses: hpd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
⊢ max p.degree q.degree ≤ (p + q).degree
have rw : max p.degree q.degree ≤ q.degree
Tactic: rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
rw : max p.degree q.degree ≤ q.degree
⊢ max p.degree q.degree ≤ (p + q).degree
have rw₁ : q.degree ≤ q.degree
Tactic: rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : max p.degree q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0
have hlt₁ : q.degree > (p + q).degree
Tactic: rw [HEq, max_self] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0
have rw : (p + q).coeff q.natDegree = 0
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : q.degree < p.degree
⊢ max p.degree q.degree ≤ (p + q).degree
have rw : max p.degree q.degree ≤ p.degree
Tactic: rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : q.degree < p.degree
rw : max p.degree q.degree ≤ p.degree
⊢ max p.degree q.degree ≤ (p + q).degree
have rw₁ : p.degree ≤ p.degree
Tactic: rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
⊢ p.natDegree = q.natDegree
have by_contra : ∀ (h : ¬p.natDegree = q.natDegree), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ q.natDegree < p.natDegree
have rwa : ∀ (H : q.natDegree < p.natDegree) (h : ¬p.natDegree = q.natDegree) (h : p.natDegree < q.natDegree),
  q.natDegree < p.natDegree
Tactic: rwa [natDegree_add_eq_right_of_natDegree_lt h] at H
Cleared hypotheses: H, h_1, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False
have H₁ : p.natDegree < p.natDegree
Tactic: rw [natDegree_add_eq_left_of_natDegree_lt h] at H
Cleared hypotheses: H, h_1, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h : ¬p.natDegree = q.natDegree
⊢ False
have x : p.natDegree < q.natDegree ∨ q.natDegree < p.natDegree
Tactic: cases Nat.lt_or_lt_of_ne h with
  | inl h => exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)
  | inr h =>
    rw [natDegree_add_eq_left_of_natDegree_lt h] at H
    exact LT.lt.false H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
⊢ p.natDegree = q.natDegree
have pos : ∀ (h₁ : p.natDegree = 0), p.natDegree = q.natDegree
Tactic: by_cases h₁ : natDegree p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
pos : ∀ (h₁ : p.natDegree = 0), p.natDegree = q.natDegree
⊢ p.natDegree = q.natDegree
have neg : ∀ (h₁ : ¬p.natDegree = 0), p.natDegree = q.natDegree
Tactic: by_cases h₁ : natDegree p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree
have pos : ∀ (h₂ : q.natDegree = 0), p.natDegree = q.natDegree
Tactic: by_cases h₂ : natDegree q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
pos : ∀ (h₂ : q.natDegree = 0), p.natDegree = q.natDegree
⊢ p.natDegree = q.natDegree
have neg : ∀ (h₂ : ¬q.natDegree = 0), p.natDegree = q.natDegree
Tactic: by_cases h₂ : natDegree q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree
have pos : ∀ (h₂ : q.natDegree = 0), p.natDegree = q.natDegree
Tactic: on_goal 1 => by_cases h₂ : natDegree q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
pos : ∀ (h₂ : q.natDegree = 0), p.natDegree = q.natDegree
⊢ p.natDegree = q.natDegree
have neg : ∀ (h₂ : ¬q.natDegree = 0), p.natDegree = q.natDegree
Tactic: on_goal 1 => by_cases h₂ : natDegree q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree
have neg : (p + q).natDegree < q.natDegree
Tactic: apply natDegree_eq_of_natDegree_add_lt_right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ (p + q).natDegree < q.natDegree
have neg : 0 < q.natDegree
Tactic: rwa [H, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
neg : 0 < q.natDegree
⊢ (p + q).natDegree < q.natDegree
have neg₁ : q.natDegree ≠ 0
Tactic: rwa [H, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree
have neg : (p + q).natDegree < p.natDegree
Tactic: apply natDegree_eq_of_natDegree_add_lt_left
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ (p + q).natDegree < p.natDegree
have neg : 0 < p.natDegree
Tactic: rwa [H, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
neg : 0 < p.natDegree
⊢ (p + q).natDegree < p.natDegree
have neg₁ : p.natDegree ≠ 0
Tactic: rwa [H, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ p.leadingCoeff = 1
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
h : Nontrivial R
⊢ p.leadingCoeff = 1
have refine : p.coeff n ≠ 0
Tactic: refine (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ (p + q).leadingCoeff = q.leadingCoeff
have this : p.coeff q.natDegree = 0
Tactic: have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).leadingCoeff = p.leadingCoeff
have rw : (q + p).leadingCoeff = p.leadingCoeff
Tactic: rw [add_comm]