awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m
mul_eq : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g = p
this : (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g
inr :
  eval t g =
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g).comp
        (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₁ :
  eval t g =
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m).comp
          (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₂ :
  eval t g =
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])).comp
            (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₃ :
  eval t g =
    ((comp X (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) -
            comp ((C : (a : R) → R[X]) t) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₄ :
  eval t g =
    ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) -
            comp ((C : (a : R) → R[X]) t) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₅ :
  eval t g =
    (HSub.hSub (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))
            ((C : (a : R) → R[X]) t : R[X]) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₆ :
  eval t g =
    (HPow.hPow (α := R[X]) X m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₇ :
  eval t g =
    (HPow.hPow (α := R[X]) X m *
          g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).reverse.leadingCoeff
inr₈ : eval t g = (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).reverse.leadingCoeff
⊢ eval t g = (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inr₉ : eval t g = (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: rw [← congr_arg (comp · <| X + C t) mul_eq, mul_comp, pow_comp, sub_comp, X_comp, C_comp,
    add_sub_cancel_right, ← reverse_leadingCoeff, reverse_X_pow_mul, reverse_leadingCoeff,
    trailingCoeff, Nat.le_zero.1 (natTrailingDegree_le_of_ne_zero <|
      this ▸ eval_divByMonic_pow_rootMultiplicity_ne_zero t hp), this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have simp_rw : (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have refine : ∀ (h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have zero : ∀ (h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
  HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0 ∣ p
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p
zero :
  ∀ (h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0 ∣ p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have succ : ∀ (n : ℕ) (h : ∀ m < n + 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have simp_rw : (n ≤
    if h : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        sorry) ↔
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      if h : p = 0 then 0
      else
        Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have simp_rw₁ : n ≤ Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) sorry ↔
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      if h : p = 0 then 0
      else
        Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₁ :
  n ≤
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯ ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have simp_rw₂ : (∀ m < n, ¬¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      if h : p = 0 then 0
      else
        Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₁ :
  n ≤
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯ ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₂ :
  (∀ m < n, ¬¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have simp_rw₃ : (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      if h : p = 0 then 0
      else
        Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₁ :
  n ≤
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯ ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₂ :
  (∀ m < n, ¬¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₃ :
  (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have simp_rw₄ : ∀ (h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      if h : p = 0 then 0
      else
        Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₁ :
  n ≤
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯ ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₂ :
  (∀ m < n, ¬¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₃ :
  (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₄ :
  ∀ (h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have zero : ∀ (h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
  HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0 ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      if h : p = 0 then 0
      else
        Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₁ :
  n ≤
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯ ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₂ :
  (∀ m < n, ¬¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₃ :
  (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₄ :
  ∀ (h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
zero :
  ∀ (h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0 ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
have succ : ∀ (n : ℕ) (h : ∀ m < n + 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
Tactic: classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
have rw : rootMultiplicity a p ≤ n ↔ ¬n + 1 ≤ rootMultiplicity a p
Tactic: rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
rw : rootMultiplicity a p ≤ n ↔ ¬n + 1 ≤ rootMultiplicity a p
⊢ rootMultiplicity a p ≤ n ↔ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
have rw₁ : rootMultiplicity a p ≤ n ↔ rootMultiplicity a p < n + 1
Tactic: rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
rw : rootMultiplicity a p ≤ n ↔ ¬n + 1 ≤ rootMultiplicity a p
rw₁ : rootMultiplicity a p ≤ n ↔ rootMultiplicity a p < n + 1
⊢ rootMultiplicity a p ≤ n ↔ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
have rw₂ : rootMultiplicity a p ≤ n ↔ rootMultiplicity a p ≤ n
Tactic: rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)
have rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
    min (rootMultiplicity a p) (rootMultiplicity a q) ∣
  p + q
Tactic: rw [le_rootMultiplicity_iff hzero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)
have rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p *
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣
  p * q
Tactic: rw [le_rootMultiplicity_iff hpq, pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣
    p * q
have a : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p ∣ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
a : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p ∣ p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣
    p * q
have a₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣ q
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hq : q ≠ 0
hpq : p ∣ q
x : R
⊢ rootMultiplicity x p ≤ rootMultiplicity x q
have obtain : ∀ (w : R[X]) (hq : p * w ≠ 0), rootMultiplicity x p ≤ rootMultiplicity x (p * w)
Tactic: obtain ⟨_, rfl⟩ := hpq
Cleared hypotheses: q, hq, hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (rootMultiplicity a p + 1) ∣ p
have rw : rootMultiplicity a p ≤ rootMultiplicity a p
Tactic: rw [← rootMultiplicity_le_iff p0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
⊢ rootMultiplicity 0 p = p.natTrailingDegree
have pos : ∀ (h : p = 0), rootMultiplicity 0 p = p.natTrailingDegree
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
pos : ∀ (h : p = 0), rootMultiplicity 0 p = p.natTrailingDegree
⊢ rootMultiplicity 0 p = p.natTrailingDegree
have neg : ∀ (h : ¬p = 0), rootMultiplicity 0 p = p.natTrailingDegree
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree
have neg : rootMultiplicity 0 p ≤ p.natTrailingDegree
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
neg : rootMultiplicity 0 p ≤ p.natTrailingDegree
⊢ rootMultiplicity 0 p = p.natTrailingDegree
have neg₁ : p.natTrailingDegree ≤ rootMultiplicity 0 p
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree
have neg : ∃ (x : ℕ), ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)
Tactic: rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p
have neg : ∀ d < p.natTrailingDegree, p.coeff d = 0
Tactic: rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h : Nontrivial R
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
Tactic: have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
    simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
      Nat.WithBot.one_le_iff_zero_lt] using hdegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff
have nth_rw : (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff
Tactic: nth_rw 2 [← modByMonic_add_div p q]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff
have rw : (p %ₘ q).degree < (q * (p /ₘ q)).degree
Tactic: rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree
have rw : (p %ₘ q).degree < p.degree
Tactic: rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ p.degree = 1
have h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
Tactic: have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
⊢ p.degree = 1
have h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 0
Tactic: have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h