awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
succ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ (n + 1)
succ₁ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
⊢ eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)
have succ₂ : eval₂ (algebraMap R S) x (p ^ n) * eval₂ (algebraMap R S) x p =
  eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
Tactic: rw [pow_succ, pow_succ, eval₂_mul', ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
succ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ (n + 1)
succ₁ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
succ₂ :
  eval₂ (algebraMap R S) x (p ^ n) * eval₂ (algebraMap R S) x p =
    eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
⊢ eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)
have succ₃ : eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p =
  eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
Tactic: rw [pow_succ, pow_succ, eval₂_mul', ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
⊢ eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
have zero : eval₂ (algebraMap R S) x (HPow.hPow (β := ℕ) p 0) = HPow.hPow (β := ℕ) (eval₂ (algebraMap R S) x p) 0
Tactic: induction n with
  | zero => simp only [pow_zero, eval₂_one]
  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
zero : eval₂ (algebraMap R S) x (HPow.hPow (β := ℕ) p 0) = HPow.hPow (β := ℕ) (eval₂ (algebraMap R S) x p) 0
⊢ eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
have succ : ∀ (n : ℕ) (ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n),
  eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)
Tactic: induction n with
  | zero => simp only [pow_zero, eval₂_one]
  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p
have add : ∀ (r s : R[X]) (hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r)
  (hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s),
  eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
  | monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Algebra (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q : R[X]
add :
  ∀ (r s : R[X]) (hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r)
    (hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s),
    eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)
⊢ eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p
have monomial : ∀ (n : ℕ) (a : R),
  eval₂ (algebraMap R S) x (comp ((monomial n : (a : R) → R[X]) a) q) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) ((monomial n : (a : R) → R[X]) a)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
  | monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.Monic
h_irr : Irreducible (map φ f)
⊢ Irreducible f
have refine : ∀ (a b : R[X]) (h : f = a * b), IsUnit a ∨ IsUnit b
Tactic: refine ⟨h_irr.not_isUnit ∘ IsUnit.map (mapRingHom φ), fun a b h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
have q : a.leadingCoeff * b.leadingCoeff = (a * b).leadingCoeff
Tactic: have q := (leadingCoeff_mul a b).symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = (a * b).leadingCoeff
⊢ IsUnit a ∨ IsUnit b
have q₁ : a.leadingCoeff * b.leadingCoeff = 1
Tactic: rw [← h, h_mon] at q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a ∨ IsUnit b
have refine_1 : IsUnit (map φ a) → IsUnit a
Tactic: refine (h_irr.isUnit_or_isUnit <|
    (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_1 : IsUnit (map φ a) → IsUnit a
⊢ IsUnit a ∨ IsUnit b
have refine_2 : IsUnit (map φ b) → IsUnit b
Tactic: refine (h_irr.isUnit_or_isUnit <|
    (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ a) → IsUnit a
have refine_1 : IsUnit a.leadingCoeff
Tactic: apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ b) → IsUnit b
have refine_2 : IsUnit b.leadingCoeff
Tactic: apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_1 : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a.leadingCoeff
have refine_1₁ : R
Tactic: apply IsUnit.of_mul_eq_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b.leadingCoeff
have refine_2 : b.leadingCoeff * a.leadingCoeff = 1
Tactic: apply IsUnit.of_mul_eq_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_2 : b.leadingCoeff * a.leadingCoeff = 1
⊢ IsUnit b.leadingCoeff
have refine_2₁ : R
Tactic: apply IsUnit.of_mul_eq_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Irreducible (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_2 : a.leadingCoeff * b.leadingCoeff = 1
⊢ b.leadingCoeff * a.leadingCoeff = 1
have refine_2₁ : R
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
⊢ c • p %ₘ q = c • (p %ₘ q)
have pos : ∀ (hq : q.Monic), c • p %ₘ q = c • (p %ₘ q)
Tactic: by_cases hq : q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
pos : ∀ (hq : q.Monic), c • p %ₘ q = c • (p %ₘ q)
⊢ c • p %ₘ q = c • (p %ₘ q)
have neg : ∀ (hq : ¬q.Monic), c • p %ₘ q = c • (p %ₘ q)
Tactic: by_cases hq : q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)
have pos : ∀ (hR : Subsingleton R), c • p %ₘ q = c • (p %ₘ q)
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
pos : ∀ (hR : Subsingleton R), c • p %ₘ q = c • (p %ₘ q)
⊢ c • p %ₘ q = c • (p %ₘ q)
have pos₁ : ∀ (hR : Nontrivial R), c • p %ₘ q = c • (p %ₘ q)
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p
have rw : c • (p %ₘ q) + c • (q * (p /ₘ q)) = c • p
Tactic: rw [mul_smul_comm, ← smul_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
rw : c • (p %ₘ q) + c • (q * (p /ₘ q)) = c • p
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p
have rw₁ : c • (p %ₘ q + q * (p /ₘ q)) = c • p
Tactic: rw [mul_smul_comm, ← smul_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
rw : c • (p %ₘ q) + c • (q * (p /ₘ q)) = c • p
rw₁ : c • (p %ₘ q + q * (p /ₘ q)) = c • p
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p
have rw₂ : c • p = c • p
Tactic: rw [mul_smul_comm, ← smul_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)
have rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
Tactic: rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)
have rw₁ : HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) (q * (p /ₘ q)) : S) =
  (aeval x : (a : R[X]) → S) p
Tactic: rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) (q * (p /ₘ q)) : S) =
    (aeval x : (a : R[X]) → S) p
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)
have rw₂ : HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) q : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
  (aeval x : (a : R[X]) → S) p
Tactic: rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) (q * (p /ₘ q)) : S) =
    (aeval x : (a : R[X]) → S) p
rw₂ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) q : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)
have rw₃ : HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (HMul.hMul (α := S) (β := S) (0 : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
  (aeval x : (a : R[X]) → S) p
Tactic: rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) (q * (p /ₘ q)) : S) =
    (aeval x : (a : R[X]) → S) p
rw₂ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) q : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
rw₃ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) (0 : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)
have rw₄ : HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) = (aeval x : (a : R[X]) → S) p
Tactic: rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) (q * (p /ₘ q)) : S) =
    (aeval x : (a : R[X]) → S) p
rw₂ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) q : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
rw₃ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) (0 : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
rw₄ : HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) = (aeval x : (a : R[X]) → S) p
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)
have rw₅ : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) p : S)
Tactic: rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos : ∀ (hp : p = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
pos : ∀ (hp : p = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have neg : ∀ (hp : ¬p = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos : (0 * q).trailingDegree = trailingDegree.{u} (R := R) 0 + q.trailingDegree
Tactic: rw [hp, zero_mul, trailingDegree_zero, top_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p = 0
pos : (0 * q).trailingDegree = trailingDegree.{u} (R := R) 0 + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos₁ : trailingDegree.{u} (R := R) 0 = trailingDegree.{u} (R := R) 0 + q.trailingDegree
Tactic: rw [hp, zero_mul, trailingDegree_zero, top_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p = 0
pos : (0 * q).trailingDegree = trailingDegree.{u} (R := R) 0 + q.trailingDegree
pos₁ : trailingDegree.{u} (R := R) 0 = trailingDegree.{u} (R := R) 0 + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos₂ : ⊤ = ⊤ + q.trailingDegree
Tactic: rw [hp, zero_mul, trailingDegree_zero, top_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p = 0
pos : (0 * q).trailingDegree = trailingDegree.{u} (R := R) 0 + q.trailingDegree
pos₁ : trailingDegree.{u} (R := R) 0 = trailingDegree.{u} (R := R) 0 + q.trailingDegree
pos₂ : ⊤ = ⊤ + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos₃ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [hp, zero_mul, trailingDegree_zero, top_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos : ∀ (hq : q = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
pos : ∀ (hq : q = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have neg : ∀ (hq : ¬q = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos : (p * 0).trailingDegree = p.trailingDegree + trailingDegree.{u} (R := R) 0
Tactic: rw [hq, mul_zero, trailingDegree_zero, add_top]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
pos : (p * 0).trailingDegree = p.trailingDegree + trailingDegree.{u} (R := R) 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos₁ : trailingDegree.{u} (R := R) 0 = p.trailingDegree + trailingDegree.{u} (R := R) 0
Tactic: rw [hq, mul_zero, trailingDegree_zero, add_top]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
pos : (p * 0).trailingDegree = p.trailingDegree + trailingDegree.{u} (R := R) 0
pos₁ : trailingDegree.{u} (R := R) 0 = p.trailingDegree + trailingDegree.{u} (R := R) 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos₂ : ⊤ = p.trailingDegree + ⊤
Tactic: rw [hq, mul_zero, trailingDegree_zero, add_top]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
pos : (p * 0).trailingDegree = p.trailingDegree + trailingDegree.{u} (R := R) 0
pos₁ : trailingDegree.{u} (R := R) 0 = p.trailingDegree + trailingDegree.{u} (R := R) 0
pos₂ : ⊤ = p.trailingDegree + ⊤
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have pos₃ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [hq, mul_zero, trailingDegree_zero, add_top]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have neg : (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑p.natTrailingDegree : ℕ∞) (↑q.natTrailingDegree : ℕ∞)
Tactic: rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p =
    rootMultiplicity 0 (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
have simp_rw : (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p) =
  if p = 0 then 0
  else
    multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
      (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
Tactic: simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]