awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ (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])))
have e_e : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
  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: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    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])))
have e_e : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
  multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
Tactic: rw [C_0, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
have h : Eq.{u + 1} (α := R[X]) X
  ((algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
Tactic: convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
-- 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.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 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: classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
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.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 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])))
⊢ 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: classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
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.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 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])))
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])))
⊢ rootMultiplicity t p =
    rootMultiplicity 0 (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
have e_e : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
  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: classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
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.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 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])))
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])))
e_e :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    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])))
⊢ rootMultiplicity t p =
    rootMultiplicity 0 (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
have e_e₁ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
  multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
Tactic: classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
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.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 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])))
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])))
e_e :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    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])))
e_e₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
⊢ rootMultiplicity t p =
    rootMultiplicity 0 (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
have h : Eq.{u + 1} (α := R[X]) X
  ((algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
Tactic: classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
x : S
hx : Membership.mem (γ := Subring S) (RingHom.range.{u, v} (R := R) (algebraMap R S)) x
⊢ Ne.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
have obtain : ∀ (w : R),
  Ne.{v + 1} (α := S) (((aeval (((algebraMap R S : R →+* S) : (a : R) → S) w) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S)
    (0 : S)
Tactic: obtain ⟨_, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w : R
⊢ Ne.{v + 1} (α := S) (((aeval (((algebraMap R S : R →+* S) : (a : R) → S) w) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S)
    (0 : S)
have rw : Ne.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) (eval w p) : S) (0 : S)
Tactic: rw [aeval_algebraMap_apply_eq_algebraMap_eval]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a p + n
have h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
Tactic: have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a p + n
have refine_1 : rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) ≤
  rootMultiplicity a p + n
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
refine_1 :
  rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) ≤
    rootMultiplicity a p + n
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a p + n
have refine_2 : rootMultiplicity a p + n ≤
  rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) ≤
    rootMultiplicity a p + n
have refine_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (rootMultiplicity a p + 1) ∣ p
Tactic: rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ rootMultiplicity a p + n ≤
    rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n)
have refine_2 : 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]) ^ n ∣
  p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n
Tactic: rw [le_rootMultiplicity_iff h2, pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
⊢ rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
have this : rootMultiplicity a ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
  rootMultiplicity a ((C : (a : R) → R[X]) 1) + n
Tactic: have := rootMultiplicity_mul_X_sub_C_pow (a := a) (n := n) C.map_one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
this :
  rootMultiplicity a
      ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a ((C : (a : R) → R[X]) 1) + n
⊢ rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
have rwa : ∀
  (this :
    rootMultiplicity a
        ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
      0 + n),
  rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
Tactic: rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
this :
  rootMultiplicity a
      ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a ((C : (a : R) → R[X]) 1) + n
rwa :
  ∀
    (this :
      rootMultiplicity a
          ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
        0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
⊢ rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
have rwa₁ : ∀ (this : rootMultiplicity a (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
  rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
Tactic: rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
this :
  rootMultiplicity a
      ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a ((C : (a : R) → R[X]) 1) + n
rwa :
  ∀
    (this :
      rootMultiplicity a
          ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
        0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
rwa₁ :
  ∀ (this : rootMultiplicity a (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
⊢ rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
have rwa₂ : ∀ (this : rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
  rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
Tactic: rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
this :
  rootMultiplicity a
      ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a ((C : (a : R) → R[X]) 1) + n
rwa :
  ∀
    (this :
      rootMultiplicity a
          ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
        0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
rwa₁ :
  ∀ (this : rootMultiplicity a (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
rwa₂ :
  ∀ (this : rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
⊢ rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
have rwa₃ : ∀ (this : rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n),
  rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
Tactic: rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = if x = y then 1 else 0
have pos : ∀ (hxy : x = y), rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1
Tactic: split_ifs with hxy
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
pos : ∀ (hxy : x = y), rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = if x = y then 1 else 0
have neg : ∀ (hxy : ¬x = y), rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 0
Tactic: split_ifs with hxy
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1
have pos : rootMultiplicity y (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1
Tactic: rw [hxy]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq :
  eval x (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p) *
      eval x (q /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q) ≠
    0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have hpq₁ : (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff *
    (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff ≠
  0
Tactic: simp_rw [eval_divByMonic_eq_trailingCoeff_comp] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq :
  (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff *
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff ≠
    0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have simp_rw : ((p * q).comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree =
  (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree +
    (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree
Tactic: simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq :
  (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff *
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff ≠
    0
simp_rw :
  ((p * q).comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree +
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have simp_rw₁ : (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) *
      q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree =
  (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree +
    (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree
Tactic: simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
⊢ (HMul.hMul (β := R[X]) (p.comp (-X))
        ((C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff =
    1
have hp₁ : (p.comp (-X)).leadingCoeff * HPow.hPow (α := R) (-1) p.natDegree = 1
Tactic: apply monic_mul_C_of_leadingCoeff_mul_eq_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
⊢ (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff = 1
have C : (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff =
  (HMul.hMul (β := R[X]) (p.comp (-X)) ((C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff
Tactic: calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
C :
  (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff =
    (HMul.hMul (β := R[X]) (p.comp (-X))
        ((Polynomial.C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff
⊢ (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff = 1
have C₁ : (HMul.hMul (β := R[X]) (p.comp (-X))
      ((Polynomial.C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff =
  1
Tactic: calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Associated p q
⊢ p.degree = q.degree
have let : ∀ (u : R[X]ˣ) (hu : p * (↑u : R[X]) = q), p.degree = q.degree
Tactic: let ⟨u, hu⟩ := h