awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
rw :
  eval a
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
    0
rw₁ :
  eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₂ :
  (eval a X - eval a ((C : (a : R) → R[X]) a)) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₃ :
  (a - eval a ((C : (a : R) → R[X]) a)) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₄ : (a - a) * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0
⊢ eval a p = 0
have rw₅ : 0 * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0
Tactic: rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
rw :
  eval a
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
    0
rw₁ :
  eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₂ :
  (eval a X - eval a ((C : (a : R) → R[X]) a)) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₃ :
  (a - eval a ((C : (a : R) → R[X]) a)) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₄ : (a - a) * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0
rw₅ : 0 * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0
⊢ eval a p = 0
have rw₆ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : eval a p = 0
| p
have rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : eval a p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
have conv_rhs : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
  p
Tactic: conv_rhs => rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : eval a p = 0
conv_rhs :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
have conv_rhs₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: conv_rhs => rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
⊢ p.IsRoot a
have rwa : ∀ (h : p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0), p.IsRoot a
Tactic: rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
rwa : ∀ (h : p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0), p.IsRoot a
⊢ p.IsRoot a
have rwa₁ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) (0 : R[X])), p.IsRoot a
Tactic: rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
rwa : ∀ (h : p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0), p.IsRoot a
rwa₁ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) (0 : R[X])), p.IsRoot a
⊢ p.IsRoot a
have rwa₂ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) ((C : (a : R) → R[X]) 0 : R[X])), p.IsRoot a
Tactic: rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
rwa : ∀ (h : p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0), p.IsRoot a
rwa₁ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) (0 : R[X])), p.IsRoot a
rwa₂ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) ((C : (a : R) → R[X]) 0 : R[X])), p.IsRoot a
⊢ p.IsRoot a
have rwa₃ : ∀ (h : eval a p = 0), p.IsRoot a
Tactic: rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : p.IsRoot a
⊢ p =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have rw : p = p
Tactic: rw [mul_divByMonic_eq_iff_isRoot.2 h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])
have rw : (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])).IsRoot a
Tactic: rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
rw : (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])).IsRoot a
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])
have rw₁ : eval a (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])) = 0
Tactic: rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
rw : (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])).IsRoot a
rw₁ : eval a (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])) = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])
have rw₂ : eval a p - eval a ((C : (a : R) → R[X]) (eval a p)) = 0
Tactic: rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
rw : (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])).IsRoot a
rw₁ : eval a (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])) = 0
rw₂ : eval a p - eval a ((C : (a : R) → R[X]) (eval a p)) = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])
have rw₃ : eval a p - eval a p = 0
Tactic: rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
rw : (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])).IsRoot a
rw₁ : eval a (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])) = 0
rw₂ : eval a p - eval a ((C : (a : R) → R[X]) (eval a p)) = 0
rw₃ : eval a p - eval a p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])
have rw₄ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
⊢ p %ₘ X = (C : (a : R) → R[X]) (eval 0 p)
have rw : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
Tactic: rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
rw : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
⊢ p %ₘ X = (C : (a : R) → R[X]) (eval 0 p)
have rw₁ : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X 0
Tactic: rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
rw : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
rw₁ : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X 0
⊢ p %ₘ X = (C : (a : R) → R[X]) (eval 0 p)
have rw₂ : p %ₘ X = p %ₘ X
Tactic: rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
have rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
Tactic: rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
have rw₁ : eval₂ f x p - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p
Tactic: rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
rw₁ : eval₂ f x p - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
have rw₂ : eval₂ f x p - eval₂ f x q * eval₂ f x (p /ₘ q) = eval₂ f x p
Tactic: rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
rw₁ : eval₂ f x p - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p
rw₂ : eval₂ f x p - eval₂ f x q * eval₂ f x (p /ₘ q) = eval₂ f x p
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
have rw₃ : eval₂ f x p - 0 * eval₂ f x (p /ₘ q) = eval₂ f x p
Tactic: rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
rw₁ : eval₂ f x p - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p
rw₂ : eval₂ f x p - eval₂ f x q * eval₂ f x (p /ₘ q) = eval₂ f x p
rw₃ : eval₂ f x p - 0 * eval₂ f x (p /ₘ q) = eval₂ f x p
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
have rw₄ : eval₂ f x p - 0 = eval₂ f x p
Tactic: rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
rw₁ : eval₂ f x p - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p
rw₂ : eval₂ f x p - eval₂ f x q * eval₂ f x (p /ₘ q) = eval₂ f x p
rw₃ : eval₂ f x p - 0 * eval₂ f x (p /ₘ q) = eval₂ f x p
rw₄ : eval₂ f x p - 0 = eval₂ f x p
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
have rw₅ : eval₂ f x p = eval₂ f x p
Tactic: rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p
have suffices : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]) ∣
  HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval b p) : R[X])
Tactic: suffices X - C b ∣ p - C (p.eval b) by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
have rw : rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
Tactic: rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
rw : rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
have rw₁ : ¬rootMultiplicity x p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
Tactic: rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
rw : rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₁ : ¬rootMultiplicity x p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
have rw₂ : ¬(p.IsRoot x → p = 0) ↔ p ≠ 0 ∧ p.IsRoot x
Tactic: rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
rw : rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₁ : ¬rootMultiplicity x p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₂ : ¬(p.IsRoot x → p = 0) ↔ p ≠ 0 ∧ p.IsRoot x
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
have rw₃ : p.IsRoot x ∧ ¬p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
Tactic: rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
rw : rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₁ : ¬rootMultiplicity x p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₂ : ¬(p.IsRoot x → p = 0) ↔ p ≠ 0 ∧ p.IsRoot x
rw₃ : p.IsRoot x ∧ ¬p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
have rw₄ : ¬p = 0 ∧ p.IsRoot x ↔ p ≠ 0 ∧ p.IsRoot x
Tactic: rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
have this : Nontrivial R
Tactic: haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
have rw : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p
Tactic: rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq :
  p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * q
⊢ False
have this₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
  p
Tactic: have := pow_mul_divByMonic_rootMultiplicity_eq p a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this_1 : Nontrivial R
q : R[X]
hq :
  p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * q
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
    p
⊢ False
have this₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      (multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p + 1) *
    q =
  p
Tactic: rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this_1 : Nontrivial R
q : R[X]
hq :
  p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * q
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
        (multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p + 1) *
      q =
    p
⊢ 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
have rw : LT.lt (α := WithBot ℕ) 0 1
Tactic: rw [degree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
have haveI : ∀ (this : Nontrivial R),
  eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
Tactic: classical
  haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
haveI haveI₁ haveI₂ :
  ∀ (this : Nontrivial R),
    eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
have haveI₃ : ∀ (this : Nontrivial R),
  ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p
Tactic: classical
  haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
haveI haveI₁ haveI₂ :
  ∀ (this : Nontrivial R),
    eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
haveI₃ :
  ∀ (this : Nontrivial R),
    ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
        p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
have haveI₄ : ∀ (this : Nontrivial R) (q : R[X])
  (hq :
    p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * q),
  False
Tactic: classical
  haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
haveI haveI₁ haveI₂ :
  ∀ (this : Nontrivial R),
    eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
haveI₃ :
  ∀ (this : Nontrivial R),
    ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
        p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p
haveI₄ :
  ∀ (this : Nontrivial R) (q : R[X])
    (hq :
      p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p =
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * q),
    False
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
have haveI₅ : ∀ (this : Nontrivial R) (q : R[X])
  (hq :
    p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * q)
  (this :
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
      p),
  False
Tactic: classical
  haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)