awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
⊢ g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R
have refine : g • x ∈ f.rootSet R → x ∈ f.rootSet R
Tactic: refine ⟨?_, smul_mem_rootSet g⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
⊢ g • x ∈ f.rootSet R → x ∈ f.rootSet R
have obtain : ∀ (g : Gˣ), (↑g : G) • x ∈ f.rootSet R → x ∈ f.rootSet R
Tactic: obtain ⟨g, rfl⟩ := hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
⊢ p = 0
have by_contra : ∀ (hp : ¬p = 0), False
Tactic: by_contra hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ False
have refine : #p.roots.toFinset < #p.roots.toFinset
Tactic: refine lt_irrefl #p.roots.toFinset ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ Fintype.card.{u_1} (↑(Set.range f) : Type u_1) = #(image f univ)
have rw : #(Set.range f).toFinset = #(image f univ)
Tactic: rw [← Set.toFinset_card, Set.toFinset_range]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
rw : #(Set.range f).toFinset = #(image f univ)
⊢ Fintype.card.{u_1} (↑(Set.range f) : Type u_1) = #(image f univ)
have rw₁ : #(image f univ) = #(image f univ)
Tactic: rw [← Set.toFinset_card, Set.toFinset_range]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ #p.roots.toFinset < #p.roots.toFinset
have _ : image f univ ≤ p.roots.toFinset
Tactic: calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x : R
⊢ x ∈ image f univ → x ∈ p.roots.toFinset
have simp : ∀ (x_1 : ι) (h : f x_1 = x), eval x p = 0
Tactic: simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
⊢ p = 0
have by_contra : ¬p = 0 → False
Tactic: classical
  by_contra hp
  refine lt_irrefl #p.roots.toFinset ?_
  calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
  intro _
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
  rintro x rfl
  exact heval _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
⊢ p = 0
have by_contra₃ : ∀ (hp : ¬p = 0), #p.roots.toFinset < #p.roots.toFinset
Tactic: classical
  by_contra hp
  refine lt_irrefl #p.roots.toFinset ?_
  calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
  intro _
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
  rintro x rfl
  exact heval _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
by_contra₃ : ∀ (hp : ¬p = 0), #p.roots.toFinset < #p.roots.toFinset
⊢ p = 0
have by_contra₄ : ∀ (hp : ¬p = 0), image f univ ≤ p.roots.toFinset
Tactic: classical
  by_contra hp
  refine lt_irrefl #p.roots.toFinset ?_
  calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
  intro _
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
  rintro x rfl
  exact heval _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
by_contra₃ : ∀ (hp : ¬p = 0), #p.roots.toFinset < #p.roots.toFinset
by_contra₄ : ∀ (hp : ¬p = 0), image f univ ≤ p.roots.toFinset
⊢ p = 0
have by_contra₅ : ∀ (hp : ¬p = 0) ⦃x : R⦄, x ∈ image f univ → x ∈ p.roots.toFinset
Tactic: classical
  by_contra hp
  refine lt_irrefl #p.roots.toFinset ?_
  calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
  intro _
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
  rintro x rfl
  exact heval _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
by_contra₃ : ∀ (hp : ¬p = 0), #p.roots.toFinset < #p.roots.toFinset
by_contra₄ : ∀ (hp : ¬p = 0), image f univ ≤ p.roots.toFinset
by_contra₅ : ∀ (hp : ¬p = 0) ⦃x : R⦄, x ∈ image f univ → x ∈ p.roots.toFinset
⊢ p = 0
have by_contra₆ : ∀ (hp : ¬p = 0) ⦃x : R⦄ (x_1 : ι) (h : f x_1 = x), eval x p = 0
Tactic: classical
  by_contra hp
  refine lt_irrefl #p.roots.toFinset ?_
  calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
  intro _
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
  rintro x rfl
  exact heval _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
by_contra₃ : ∀ (hp : ¬p = 0), #p.roots.toFinset < #p.roots.toFinset
by_contra₄ : ∀ (hp : ¬p = 0), image f univ ≤ p.roots.toFinset
by_contra₅ : ∀ (hp : ¬p = 0) ⦃x : R⦄, x ∈ image f univ → x ∈ p.roots.toFinset
by_contra₆ : ∀ (hp : ¬p = 0) ⦃x : R⦄ (x_1 : ι) (h : f x_1 = x), eval x p = 0
⊢ p = 0
have by_contra₇ : ∀ (hp : ¬p = 0) (x : ι), eval (f x) p = 0
Tactic: classical
  by_contra hp
  refine lt_irrefl #p.roots.toFinset ?_
  calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_
  intro _
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
  rintro x rfl
  exact heval _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ p = q
have rw : p - q = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ p - q = 0
have heval₁ : ∀ (i : ι), eval (f i) (p - q) = 0
Tactic: apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
heval₁ : ∀ (i : ι), eval (f i) (p - q) = 0
⊢ p - q = 0
have hcard₁ : (p - q).natDegree < Fintype.card ι
Tactic: apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : (↑f.natDegree : Cardinal.{u}) < #R
⊢ f = 0
have inl : ∀ (hR : Finite R), f = 0
Tactic: obtain hR | hR := finite_or_infinite R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : (↑f.natDegree : Cardinal.{u}) < #R
inl : ∀ (hR : Finite R), f = 0
⊢ f = 0
have inr : ∀ (hR : Infinite R), f = 0
Tactic: obtain hR | hR := finite_or_infinite R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : (↑f.natDegree : Cardinal.{u}) < #R
hR : Finite R
⊢ f = 0
have inl : ∀ (this : Fintype R), f = 0
Tactic: have := Fintype.ofFinite R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : (↑f.natDegree : Cardinal.{u}) < #R
hR : Finite R
this : Fintype R
⊢ f = 0
have inl : f.natDegree < Fintype.card R
Tactic: apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero f Function.injective_id hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : f ≠ 0
hfR : (↑f.natDegree : Cardinal.{u}) < #R
⊢ ∃ (r : R), eval r f ≠ 0
have contrapose! : ∀ (hf : ∀ (r : R), eval r f = 0), f = 0
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) ∣ p
have rw : Dvd.dvd (α := (FractionRing R)[X])
  (map (algebraMap R (FractionRing R) : R →+* FractionRing R)
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)))
  (map (algebraMap R (FractionRing R)) p)
Tactic: rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ Dvd.dvd (α := (FractionRing R)[X])
    (map (algebraMap R (FractionRing R) : R →+* FractionRing R)
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)))
    (map (algebraMap R (FractionRing R)) p)
have rw : Dvd.dvd (α := (FractionRing R)[X])
  (∏ i ∈ p.roots.toFinset,
    map (algebraMap R (FractionRing R))
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
  (map (algebraMap R (FractionRing R)) p)
Tactic: rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ Dvd.dvd (α := (FractionRing R)[X])
    (∏ i ∈ p.roots.toFinset,
      map (algebraMap R (FractionRing R))
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
    (map (algebraMap R (FractionRing R)) p)
have refine_1 : ∀ a ∈ (↑p.roots.toFinset : Set R),
  ∀ b ∈ (↑p.roots.toFinset : Set R),
    ∀ (h : a ≠ b),
      Function.onFun (β := (FractionRing R)[X]) IsCoprime
        (fun (i : R) ↦
          map (algebraMap R (FractionRing R))
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
        a b
Tactic: refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
refine_1 :
  ∀ a ∈ (↑p.roots.toFinset : Set R),
    ∀ b ∈ (↑p.roots.toFinset : Set R),
      ∀ (h : a ≠ b),
        Function.onFun (β := (FractionRing R)[X]) IsCoprime
          (fun (i : R) ↦
            map (algebraMap R (FractionRing R))
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
          a b
⊢ Dvd.dvd (α := (FractionRing R)[X])
    (∏ i ∈ p.roots.toFinset,
      map (algebraMap R (FractionRing R))
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
    (map (algebraMap R (FractionRing R)) p)
have refine_2 : ∀ a ∈ p.roots.toFinset,
  Dvd.dvd (α := (FractionRing R)[X])
    (map (algebraMap R (FractionRing R))
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p))
    (map (algebraMap R (FractionRing R)) p)
Tactic: refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a : R
h_1 : a ∈ (↑p.roots.toFinset : Set R)
b : R
h_2 : b ∈ (↑p.roots.toFinset : Set R)
h : a ≠ b
⊢ Function.onFun (β := (FractionRing R)[X]) IsCoprime
    (fun (i : R) ↦
      map (algebraMap R (FractionRing R))
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
    a b
have refine_1 : Function.onFun (β := (FractionRing R)[X]) IsCoprime
  (fun (i : R) ↦
    HSub.hSub (α := (FractionRing R)[X]) (β := (FractionRing R)[X]) X
        ((C : (a : FractionRing R) → (FractionRing R)[X])
            (((algebraMap R (FractionRing R) : R →+* FractionRing R) : (a : R) → FractionRing R) i) :
          (FractionRing R)[X]) ^
      rootMultiplicity i p)
  a b
Tactic: simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) ∣ p
have rw : Dvd.dvd (α := (FractionRing R)[X])
  (map (algebraMap R (FractionRing R) : R →+* FractionRing R)
    (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)))
  (map (algebraMap R (FractionRing R)) p)
Tactic: classical
  rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
  rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
  refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
  · simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
    exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
  · exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw rw₁ rw₂ :
  Dvd.dvd (α := (FractionRing R)[X])
    (map (algebraMap R (FractionRing R) : R →+* FractionRing R)
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)))
    (map (algebraMap R (FractionRing R)) p)
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) ∣ p
have rw₃ : Dvd.dvd (α := (FractionRing R)[X])
  (∏ i ∈ p.roots.toFinset,
    map (algebraMap R (FractionRing R))
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
  (map (algebraMap R (FractionRing R)) p)
Tactic: classical
  rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
  rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
  refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
  · simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
    exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
  · exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw rw₁ rw₂ :
  Dvd.dvd (α := (FractionRing R)[X])
    (map (algebraMap R (FractionRing R) : R →+* FractionRing R)
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)))
    (map (algebraMap R (FractionRing R)) p)
rw₃ :
  Dvd.dvd (α := (FractionRing R)[X])
    (∏ i ∈ p.roots.toFinset,
      map (algebraMap R (FractionRing R))
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
    (map (algebraMap R (FractionRing R)) p)
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) ∣ p
have refine_1 : ∀ a ∈ (↑p.roots.toFinset : Set R),
  ∀ b ∈ (↑p.roots.toFinset : Set R),
    ∀ (h : a ≠ b),
      Function.onFun (β := (FractionRing R)[X]) IsCoprime
        (fun (i : R) ↦
          map (algebraMap R (FractionRing R))
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
        a b
Tactic: classical
  rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
  rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
  refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
  · simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
    exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
  · exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw rw₁ rw₂ :
  Dvd.dvd (α := (FractionRing R)[X])
    (map (algebraMap R (FractionRing R) : R →+* FractionRing R)
      (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)))
    (map (algebraMap R (FractionRing R)) p)
rw₃ :
  Dvd.dvd (α := (FractionRing R)[X])
    (∏ i ∈ p.roots.toFinset,
      map (algebraMap R (FractionRing R))
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
    (map (algebraMap R (FractionRing R)) p)
refine_1 :
  ∀ a ∈ (↑p.roots.toFinset : Set R),
    ∀ b ∈ (↑p.roots.toFinset : Set R),
      ∀ (h : a ≠ b),
        Function.onFun (β := (FractionRing R)[X]) IsCoprime
          (fun (i : R) ↦
            map (algebraMap R (FractionRing R))
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ^ rootMultiplicity i p))
          a b
⊢ prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) ∣ p
have refine_2 : ∀ a ∈ p.roots.toFinset,
  Dvd.dvd (α := (FractionRing R)[X])
    (map (algebraMap R (FractionRing R))
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p))
    (map (algebraMap R (FractionRing R)) p)
Tactic: classical
  rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
  rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
  refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
  · simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
    exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
  · exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s) ∣ p
r : R
⊢ count r s ≤ count r p.roots
have rw : prod
    (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
      (Multiset.filter (Eq r) s)) ∣
  p
Tactic: rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
        Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]