awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ False
have A₁ : p = 0
Tactic: simp only [inj (p.coeff 0) hz, map_zero] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
have pos : ∀ (h : p = 0), (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h : p = 0), (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
⊢ (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
have neg : ∀ (h : ¬p = 0), (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
have inl : ∀ (h : p = 0), (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
Tactic: rcases eq_or_ne p 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
inl :
  ∀ (h : p = 0),
    (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
have inr : ∀ (h : p ≠ 0), (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
Tactic: rcases eq_or_ne p 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
have inr : (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
Tactic: simp only [h, or_false]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr : ∀ (h2 : (map f p).degree = p.degree), Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
Tactic: refine ⟨fun h2 ↦ ?_, degree_map_eq_of_leadingCoeff_ne_zero f⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have h3 : (map f p).natDegree = p.natDegree
Tactic: have h3 : natDegree (map f p) = natDegree p := by simp_rw [natDegree, h2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ map f p ≠ 0
have rwa : ¬map f p = 0
Tactic: rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
rwa : ¬map f p = 0
⊢ map f p ≠ 0
have rwa₁ : ¬(map f p).degree = ⊥
Tactic: rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
rwa : ¬map f p = 0
rwa₁ : ¬(map f p).degree = ⊥
⊢ map f p ≠ 0
have rwa₂ : ¬p.degree = ⊥
Tactic: rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
rwa : ¬map f p = 0
rwa₁ : ¬(map f p).degree = ⊥
rwa₂ : ¬p.degree = ⊥
⊢ map f p ≠ 0
have rwa₃ : ¬p = 0
Tactic: rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have h4 : map f p ≠ 0
Tactic: have h4 : map f p ≠ 0 := by
    rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
Tactic: rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr₁ : (map f p).coeff p.natDegree ≠ 0
Tactic: rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
inr₁ : (map f p).coeff p.natDegree ≠ 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr₂ : (map f p).coeff (map f p).natDegree ≠ 0
Tactic: rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
inr₁ : (map f p).coeff p.natDegree ≠ 0
inr₂ : (map f p).coeff (map f p).natDegree ≠ 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr₃ : (map f p).leadingCoeff ≠ 0
Tactic: rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
inr₁ : (map f p).coeff p.natDegree ≠ 0
inr₂ : (map f p).coeff (map f p).natDegree ≠ 0
inr₃ : (map f p).leadingCoeff ≠ 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr₄ : ¬(map f p).leadingCoeff = 0
Tactic: rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
inr₁ : (map f p).coeff p.natDegree ≠ 0
inr₂ : (map f p).coeff (map f p).natDegree ≠ 0
inr₃ : (map f p).leadingCoeff ≠ 0
inr₄ : ¬(map f p).leadingCoeff = 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have inr₅ : ¬map f p = 0
Tactic: rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl : ∀ (h : p.natDegree = 0),
  (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
Tactic: rcases eq_or_ne (natDegree p) 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
inl :
  ∀ (h : p.natDegree = 0),
    (map f p).natDegree = p.natDegree ↔
      Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inr : ∀ (h : p.natDegree ≠ 0),
  (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
Tactic: rcases eq_or_ne (natDegree p) 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
Tactic: simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl₁ : (map f p).natDegree = 0 ↔ ¬Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
Tactic: simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₁ : (map f p).natDegree = 0 ↔ ¬Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl₂ : (map f p).natDegree = 0 ↔ True
Tactic: simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₁ : (map f p).natDegree = 0 ↔ ¬Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₂ : (map f p).natDegree = 0 ↔ True
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl₃ : (map f p).natDegree = 0
Tactic: simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₁ : (map f p).natDegree = 0 ↔ ¬Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₂ : (map f p).natDegree = 0 ↔ True
inl₃ : (map f p).natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl₄ : (map f p).natDegree ≤ 0
Tactic: simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₁ : (map f p).natDegree = 0 ↔ ¬Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₂ : (map f p).natDegree = 0 ↔ True
inl₃ : (map f p).natDegree = 0
inl₄ : (map f p).natDegree ≤ 0
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
have inl₅ : (map f p).natDegree ≤ p.natDegree
Tactic: simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
⊢ (map f p).nextCoeff = (f : (a : R) → S) p.nextCoeff
have simp : (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
  (f : (a : R) → S) (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
Tactic: simp only [hf, nextCoeff, natDegree_map_eq_of_injective]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    (f : (a : R) → S) (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
have pos : p.natDegree = 0 → Eq.{v + 1} (α := S) (0 : S) ((f : (a : R) → S) 0 : S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
pos : p.natDegree = 0 → Eq.{v + 1} (α := S) (0 : S) ((f : (a : R) → S) 0 : S)
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    (f : (a : R) → S) (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
have neg : ¬p.natDegree = 0 → (map f p).coeff (p.natDegree - 1) = (f : (a : R) → S) (p.coeff (p.natDegree - 1))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ (p - q).natDegree = (q - p).natDegree
have rw : (-(p - q)).natDegree = (q - p).natDegree
Tactic: rw [← natDegree_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
rw : (-(p - q)).natDegree = (q - p).natDegree
⊢ (p - q).natDegree = (q - p).natDegree
have rw₁ : (q - p).natDegree = (q - p).natDegree
Tactic: rw [← natDegree_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n
have qn₁ : (-q).natDegree ≤ n
Tactic: rw [← natDegree_neg] at qn
Cleared hypotheses: qn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n
have rw : (p + -q).natDegree ≤ n ↔ p.natDegree ≤ n
Tactic: rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
rw : (p + -q).natDegree ≤ n ↔ p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n
have rw₁ : p.natDegree ≤ n ↔ p.natDegree ≤ n
Tactic: rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ q.natDegree ≤ n
have rwa : (q - p).natDegree ≤ n ↔ q.natDegree ≤ n
Tactic: rwa [natDegree_sub, natDegree_sub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
pn : p.natDegree ≤ n
rwa : (q - p).natDegree ≤ n ↔ q.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ q.natDegree ≤ n
have rwa₁ : q.natDegree ≤ n ↔ q.natDegree ≤ n
Tactic: rwa [natDegree_sub, natDegree_sub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
dg : q.natDegree < n
⊢ (p - q).coeff n = p.coeff n
have dg₁ : (-q).natDegree < n
Tactic: rw [← natDegree_neg] at dg
Cleared hypotheses: dg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n
have rw : (p + -q).coeff n = p.coeff n
Tactic: rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
dg : (-q).natDegree < n
rw : (p + -q).coeff n = p.coeff n
⊢ (p - q).coeff n = p.coeff n
have rw₁ : p.coeff n = p.coeff n
Tactic: rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (p - q).coeff n = -q.coeff n
have rwa : (p + -q).coeff n = -q.coeff n
Tactic: rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
df : p.natDegree < n
rwa : (p + -q).coeff n = -q.coeff n
⊢ (p - q).coeff n = -q.coeff n
have rwa₁ : (-q).coeff n = -q.coeff n
Tactic: rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Ring R
p q : R[X]
df : p.natDegree < n
rwa : (p + -q).coeff n = -q.coeff n
rwa₁ : (-q).coeff n = -q.coeff n
rwa₂ : p.natDegree < n
⊢ (p - q).coeff n = -q.coeff n
have rwa₃ : -q.coeff n = -q.coeff n
Tactic: rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).nextCoeff =
    c
have rw : (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).coeff
    ((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).natDegree -
      1) =
  c
Tactic: rw [nextCoeff_of_natDegree_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
c : R
rw :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).coeff
      ((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) c : R[X])).natDegree -
        1) =
    c
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).nextCoeff =
    c
have rw₁ : 0 <
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X])).natDegree
Tactic: rw [nextCoeff_of_natDegree_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.natDegree = 1 ↔
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            p
have refine_1 : ∀ (hp : p.natDegree = 1) (h : p.coeff 1 = 0), False
Tactic: refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
refine_1 : ∀ (hp : p.natDegree = 1) (h : p.coeff 1 = 0), False
⊢ p.natDegree = 1 ↔
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            p
have refine_2 : ∀ (hp : p.natDegree = 1),
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    p
Tactic: refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
refine_1 : ∀ (hp : p.natDegree = 1) (h : p.coeff 1 = 0), False
refine_2 :
  ∀ (hp : p.natDegree = 1),
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
      p
⊢ p.natDegree = 1 ↔
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            p
have refine_3 : (∃ (a : R),
    a ≠ 0 ∧
      ∃ (b : R),
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]) =
          p) →
  p.natDegree = 1
Tactic: refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ False
have h₁ : p = 0
Tactic: rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    p
have refine_2 : ∀ (n : ℕ),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      n =
    p.coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      n =
    p.coeff n
have refine_2 : (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
    0 =
  p.coeff 0
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n