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]
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
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
⊢ 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]) ^
          (multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p + 1) *
        q =
      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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hq : q.Monic
⊢ p * q %ₘ q = 0
have rw : q ∣ p * q
Tactic: rw [modByMonic_eq_zero_iff_dvd hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
⊢ p₁ %ₘ q = p₂ %ₘ q
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
h_1 : Nontrivial R
⊢ p₁ %ₘ q = p₂ %ₘ q
have obtain : ∀ (f : R[X]) (sub_eq : p₁ - p₂ = q * f), p₁ %ₘ q = p₂ %ₘ q
Tactic: obtain ⟨f, sub_eq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₁ %ₘ q = p₂ %ₘ q
have refine : p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
Tactic: refine (div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
have rw : p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
Tactic: rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
rw : p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
have rw₁ : p₂ %ₘ q + (q * (p₂ /ₘ q) + q * f) = q * f + p₂
Tactic: rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
rw : p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
rw₁ : p₂ %ₘ q + (q * (p₂ /ₘ q) + q * f) = q * f + p₂
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
have rw₂ : p₂ %ₘ q + q * (p₂ /ₘ q) + q * f = q * f + p₂
Tactic: rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
rw : p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
rw₁ : p₂ %ₘ q + (q * (p₂ /ₘ q) + q * f) = q * f + p₂
rw₂ : p₂ %ₘ q + q * (p₂ /ₘ q) + q * f = q * f + p₂
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
have rw₃ : p₂ + q * f = q * f + p₂
Tactic: rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
rw : p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
rw₁ : p₂ %ₘ q + (q * (p₂ /ₘ q) + q * f) = q * f + p₂
rw₂ : p₂ %ₘ q + q * (p₂ /ₘ q) + q * f = q * f + p₂
rw₃ : p₂ + q * f = q * f + p₂
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
have rw₄ : q * f + p₂ = q * f + p₂
Tactic: rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
have pos : ∀ (hq : q.Monic), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Tactic: by_cases hq : q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
pos : ∀ (hq : q.Monic), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
have neg : ∀ (hq : ¬q.Monic), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Tactic: by_cases hq : q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
have pos : ∀ (hR : Subsingleton R), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
pos : ∀ (hR : Subsingleton R), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
have pos₁ : ∀ (hR : Nontrivial R), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw₂ : q * (p₁ /ₘ q) + (p₁ %ₘ q + (p₂ %ₘ q + q * (p₂ /ₘ q))) = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
rw₂ : q * (p₁ /ₘ q) + (p₁ %ₘ q + (p₂ %ₘ q + q * (p₂ /ₘ q))) = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw₃ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂) = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
rw₂ : q * (p₁ /ₘ q) + (p₁ %ₘ q + (p₂ %ₘ q + q * (p₂ /ₘ q))) = p₁ + p₂
rw₃ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂) = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw₄ : q * (p₁ /ₘ q) + p₁ %ₘ q + p₂ = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
rw₂ : q * (p₁ /ₘ q) + (p₁ %ₘ q + (p₂ %ₘ q + q * (p₂ /ₘ q))) = p₁ + p₂
rw₃ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂) = p₁ + p₂
rw₄ : q * (p₁ /ₘ q) + p₁ %ₘ q + p₂ = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw₅ : p₁ %ₘ q + q * (p₁ /ₘ q) + p₂ = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
rw₂ : q * (p₁ /ₘ q) + (p₁ %ₘ q + (p₂ %ₘ q + q * (p₂ /ₘ q))) = p₁ + p₂
rw₃ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂) = p₁ + p₂
rw₄ : q * (p₁ /ₘ q) + p₁ %ₘ q + p₂ = p₁ + p₂
rw₅ : p₁ %ₘ q + q * (p₁ /ₘ q) + p₂ = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
have rw₆ : p₁ + p₂ = p₁ + p₂
Tactic: rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
⊢ -p %ₘ q = -(p %ₘ q)
have rw : -p %ₘ q + p %ₘ q = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
rw : -p %ₘ q + p %ₘ q = 0
⊢ -p %ₘ q = -(p %ₘ q)
have rw₁ : (-p + p) %ₘ q = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
rw : -p %ₘ q + p %ₘ q = 0
rw₁ : (-p + p) %ₘ q = 0
⊢ -p %ₘ q = -(p %ₘ q)
have rw₂ : 0 %ₘ q = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
rw : -p %ₘ q + p %ₘ q = 0
rw₁ : (-p + p) %ₘ q = 0
rw₂ : 0 %ₘ q = 0
⊢ -p %ₘ q = -(p %ₘ q)
have rw₃ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
have pos : ∀ (h : ¬q.Monic), p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
Tactic: by_cases! h : ¬ q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
pos : ∀ (h : ¬q.Monic), p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
have neg : ∀ (h : q.Monic), p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
Tactic: by_cases! h : ¬ q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
have neg : q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)
Tactic: apply Polynomial.modByMonic_eq_of_dvd_sub h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)
have this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
Tactic: have : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = (p₁ %ₘ q) * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q) := by ring
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)
have neg : q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
have neg : q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
neg : q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
have neg₁ : q ∣ p₂ * (p₁ - p₁ %ₘ q)
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)
have neg : q ∣ p₂ - p₂ %ₘ q
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)
have neg : q ∣ p₁ - p₁ %ₘ q
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inl : eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
  (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
inl :
  eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inr : ∀ (hp : p ≠ 0),
  eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
t : R
⊢ eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inl : eval t 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
t : R
inl : eval t 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
⊢ eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inl₁ : 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
t : R
inl : eval t 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inl₁ : 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
⊢ eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inl₂ : Eq.{u + 1} (α := R) 0 (trailingCoeff 0)
Tactic: rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
t : R
inl : eval t 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inl₁ : 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inl₂ : Eq.{u + 1} (α := R) 0 (trailingCoeff 0)
⊢ eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inl₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have mul_eq : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
  p
Tactic: have mul_eq := p.pow_mul_divByMonic_rootMultiplicity_eq t
-- 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
mul_eq :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    p
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inr : let m := rootMultiplicity t p;
∀
  (mul_eq :
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
      p),
  eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: set m := p.rootMultiplicity t
Cleared hypotheses: mul_eq
-- 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
mul_eq :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
    p
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inr : let g := 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),
  eval t g = (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
Tactic: set g := p /ₘ (X - C t) ^ m
Cleared hypotheses: mul_eq
-- 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
⊢ (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g
have rw : eval 0 (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) = eval t g
Tactic: rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
-- 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
rw : eval 0 (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) = eval t g
⊢ (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g
have rw₁ : eval (eval 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) g = eval t g
Tactic: rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
-- 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
rw : eval 0 (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) = eval t g
rw₁ : eval (eval 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) g = eval t g
⊢ (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g
have rw₂ : eval (HAdd.hAdd (α := R) (eval 0 X) (eval 0 ((C : (a : R) → R[X]) t))) g = eval t g
Tactic: rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
-- 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
rw : eval 0 (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) = eval t g
rw₁ : eval (eval 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) g = eval t g
rw₂ : eval (HAdd.hAdd (α := R) (eval 0 X) (eval 0 ((C : (a : R) → R[X]) t))) g = eval t g
⊢ (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g
have rw₃ : eval (HAdd.hAdd (α := R) 0 (eval 0 ((C : (a : R) → R[X]) t))) g = eval t g
Tactic: rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]