awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₄ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₅ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₆ : 0 + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₄ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₅ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₆ : 0 + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₇ : HAdd.hAdd (α := k) 0 0 = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₄ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₅ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₆ : 0 + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₇ : HAdd.hAdd (α := k) 0 0 = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₈ : Eq.{y + 1} (α := k) 0 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α f = 0
have obtain : ∀ (p : R[X]) (hp : f = EuclideanDomain.gcd f g * p), eval₂ ϕ α f = 0
Tactic: obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α f = 0
have rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
⊢ eval₂ ϕ α f = 0
have rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
⊢ eval₂ ϕ α f = 0
have rw₂ : 0 * eval₂ ϕ α p = 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
rw₂ : 0 * eval₂ ϕ α p = 0
⊢ eval₂ ϕ α f = 0
have rw₃ : Eq.{y + 1} (α := k) 0 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α g = 0
have obtain : ∀ (p : R[X]) (hp : g = EuclideanDomain.gcd f g * p), eval₂ ϕ α g = 0
Tactic: obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α g = 0
have rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
⊢ eval₂ ϕ α g = 0
have rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
⊢ eval₂ ϕ α g = 0
have rw₂ : 0 * eval₂ ϕ α p = 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
rw₂ : 0 * eval₂ ϕ α p = 0
⊢ eval₂ ϕ α g = 0
have rw₃ : Eq.{y + 1} (α := k) 0 0
Tactic: rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
Tactic: rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
Tactic: rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw₂ : IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
Tactic: rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
rw₂ : IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw₃ : IsUnit (EuclideanDomain.gcd p q) ↔ IsUnit (EuclideanDomain.gcd p q)
Tactic: rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
Tactic: classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
Tactic: classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw₂ : IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
Tactic: classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
rw₂ : IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
have rw₃ : IsUnit (EuclideanDomain.gcd p q) ↔ IsUnit (EuclideanDomain.gcd p q)
Tactic: classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p : R[X]
inst_1 : CommRing k
inst_2 : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0
have rw : (map f p).IsRoot x ↔ eval₂ f x p = 0
Tactic: rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p : R[X]
inst_1 : CommRing k
inst_2 : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
rw : (map f p).IsRoot x ↔ eval₂ f x p = 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0
have rw₁ : eval x (map f p) = 0 ↔ eval₂ f x p = 0
Tactic: rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p : R[X]
inst_1 : CommRing k
inst_2 : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
rw : (map f p).IsRoot x ↔ eval₂ f x p = 0
rw₁ : eval x (map f p) = 0 ↔ eval₂ f x p = 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0
have rw₂ : eval₂ f x p = 0 ↔ eval₂ f x p = 0
Tactic: rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
Tactic: rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
Tactic: rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
Tactic: rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₃ : (↑{0} : Set S) = {0}
Tactic: rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
rw₃ : (↑{0} : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₄ : Eq (α := Set S) {0} {0}
Tactic: rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
Tactic: classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
Tactic: classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
Tactic: classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₃ : (↑{0} : Set S) = {0}
Tactic: classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
rw₃ : (↑{0} : Set S) = {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
have rw₄ : Eq (α := Set S) {0} {0}
Tactic: classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).rootSet S = {0}
have rw : rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
Tactic: rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).rootSet S = {0}
have rw₁ : Eq (α := Set S) {0} {0}
Tactic: rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ (HPow.hPow (α := R[X]) X n).rootSet S = {0}
have rw : Ne.{u + 1} (α := R) 1 0
Tactic: rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ (↑(roots (map (algebraMap R S) (s.prod f))).toFinset : Set S) =
    ⋃ i ∈ (↑s : Set ι), (↑(roots (map (algebraMap R S) (f i))).toFinset : Set S)
have a : Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
Tactic: rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
have a : Ne (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
Tactic: rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
a : Ne (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
⊢ Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
have a₁ : ¬Eq (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
Tactic: rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
a : Ne (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
a₁ : ¬Eq (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
⊢ Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
have a₂ : ¬Eq.{u + 1} (α := R[X]) (∏ i ∈ s, f i) 0
Tactic: rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S
have simp : (↑(roots (map (algebraMap R S) (s.prod f))).toFinset : Set S) =
  ⋃ i ∈ (↑s : Set ι), (↑(roots (map (algebraMap R S) (f i))).toFinset : Set S)
Tactic: classical
  simp only [rootSet, aroots, ← Finset.mem_coe]
  rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
  rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
simp :
  (↑(roots (map (algebraMap R S) (s.prod f))).toFinset : Set S) =
    ⋃ i ∈ (↑s : Set ι), (↑(roots (map (algebraMap R S) (f i))).toFinset : Set S)
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S
have a : Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
Tactic: classical
  simp only [rootSet, aroots, ← Finset.mem_coe]
  rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
  rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
⊢ p.degree ≤ 1
have rw : LE.le (α := WithBot ℕ) 1 1
Tactic: rw [h]