awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ aroots.{w, v} (T := T) ((monomial n : (a : T) → T[X]) a) S = HSMul.hSMul (β := Multiset S) n {0}
have rw : (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) X n)).aroots S =
  HSMul.hSMul (β := Multiset S) n {0}
Tactic: rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
rw :
  (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) X n)).aroots S =
    HSMul.hSMul (β := Multiset S) n {0}
⊢ aroots.{w, v} (T := T) ((monomial n : (a : T) → T[X]) a) S = HSMul.hSMul (β := Multiset S) n {0}
have rw₁ : HSMul.hSMul (β := Multiset S) n {0} = HSMul.hSMul (β := Multiset S) n {0}
Tactic: rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing T
p : T[X]
inst_3 : CommRing S
inst_4 : Algebra T S
inst_5 : Algebra S R
inst_6 : Algebra T R
inst_7 : IsScalarTower T S R
⊢ aroots (map (algebraMap T S) p) R = p.aroots R
have rw : roots (map (algebraMap S R) (map (algebraMap T S) p)) = p.aroots R
Tactic: rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing T
p : T[X]
inst_3 : CommRing S
inst_4 : Algebra T S
inst_5 : Algebra S R
inst_6 : Algebra T R
inst_7 : IsScalarTower T S R
rw : roots (map (algebraMap S R) (map (algebraMap T S) p)) = p.aroots R
⊢ aroots (map (algebraMap T S) p) R = p.aroots R
have rw₁ : roots (map (algebraMap S R) (map (algebraMap T S) p)) = roots (map (algebraMap T R) p)
Tactic: rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing T
p : T[X]
inst_3 : CommRing S
inst_4 : Algebra T S
inst_5 : Algebra S R
inst_6 : Algebra T R
inst_7 : IsScalarTower T S R
rw : roots (map (algebraMap S R) (map (algebraMap T S) p)) = p.aroots R
rw₁ : roots (map (algebraMap S R) (map (algebraMap T S) p)) = roots (map (algebraMap T R) p)
⊢ aroots (map (algebraMap T S) p) R = p.aroots R
have rw₂ : roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p) =
  roots (map (algebraMap T R) p)
Tactic: rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing T
p : T[X]
inst_3 : CommRing S
inst_4 : Algebra T S
inst_5 : Algebra S R
inst_6 : Algebra T R
inst_7 : IsScalarTower T S R
rw : roots (map (algebraMap S R) (map (algebraMap T S) p)) = p.aroots R
rw₁ : roots (map (algebraMap S R) (map (algebraMap T S) p)) = roots (map (algebraMap T R) p)
rw₂ :
  roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p) =
    roots (map (algebraMap T R) p)
⊢ aroots (map (algebraMap T S) p) R = p.aroots R
have rw₃ : roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p) =
  roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p)
Tactic: rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
Tactic: rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw₁ : (↑(toFinset 0) : Set S) = ∅
Tactic: rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
rw₁ : (↑(toFinset 0) : Set S) = ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw₂ : (↑∅ : Set S) = ∅
Tactic: rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
rw₁ : (↑(toFinset 0) : Set S) = ∅
rw₂ : (↑∅ : Set S) = ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw₃ : Eq.{v + 1} (α := Set S) ∅ ∅
Tactic: rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
Tactic: classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw₁ : (↑(toFinset 0) : Set S) = ∅
Tactic: classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
rw₁ : (↑(toFinset 0) : Set S) = ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw₂ : (↑∅ : Set S) = ∅
Tactic: classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
rw₁ : (↑(toFinset 0) : Set S) = ∅
rw₂ : (↑∅ : Set S) = ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅
have rw₃ : Eq.{v + 1} (α := Set S) ∅ ∅
Tactic: classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
⊢ rootSet.{w, u_1} (T := T) 0 S = ∅
have rw : rootSet.{w, u_1} (T := T) ((C : (a : T) → T[X]) 0) S = ∅
Tactic: rw [← C_0, rootSet_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : rootSet.{w, u_1} (T := T) ((C : (a : T) → T[X]) 0) S = ∅
⊢ rootSet.{w, u_1} (T := T) 0 S = ∅
have rw₁ : Eq.{u_1 + 1} (α := Set S) ∅ ∅
Tactic: rw [← C_0, rootSet_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
⊢ rootSet.{w, u_1} (T := T) 1 S = ∅
have rw : rootSet.{w, u_1} (T := T) ((C : (a : T) → T[X]) 1) S = ∅
Tactic: rw [← C_1, rootSet_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : rootSet.{w, u_1} (T := T) ((C : (a : T) → T[X]) 1) S = ∅
⊢ rootSet.{w, u_1} (T := T) 1 S = ∅
have rw₁ : Eq.{u_1 + 1} (α := Set S) ∅ ∅
Tactic: rw [← C_1, rootSet_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
⊢ (-p).rootSet S = p.rootSet S
have rw : (↑((-p).aroots S).toFinset : Set S) = p.rootSet S
Tactic: rw [rootSet, aroots_neg, rootSet]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : (↑((-p).aroots S).toFinset : Set S) = p.rootSet S
⊢ (-p).rootSet S = p.rootSet S
have rw₁ : (↑(p.aroots S).toFinset : Set S) = p.rootSet S
Tactic: rw [rootSet, aroots_neg, rootSet]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : (↑((-p).aroots S).toFinset : Set S) = p.rootSet S
rw₁ : (↑(p.aroots S).toFinset : Set S) = p.rootSet S
⊢ (-p).rootSet S = p.rootSet S
have rw₂ : (↑(p.aroots S).toFinset : Set S) = (↑(p.aroots S).toFinset : Set S)
Tactic: rw [rootSet, aroots_neg, rootSet]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
⊢ Set.Finite.{u_1} (α := R[X]) fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
have refine_1 : (π '' fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆
  Set.pi (α := fun (i : Fin (d + 1)) ↦ R) Set.univ fun (x : Fin (d + 1)) ↦ U
Tactic: refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
refine_1 :
  (π '' fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆
    Set.pi (α := fun (i : Fin (d + 1)) ↦ R) Set.univ fun (x : Fin (d + 1)) ↦ U
⊢ Set.Finite.{u_1} (α := R[X]) fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
have refine_2 : Set.InjOn π fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
Tactic: refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
⊢ Set.InjOn π fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
have refine_2 : ∀ (x : R[X]) (hx : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) x)
  (y : R[X]) (hy : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) y)
  (hxy : π x = π y) (i : ℕ) (hi : i ≤ d), x.coeff i = y.coeff i
Tactic: refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw : a ∈ (↑(p.aroots S).toFinset : Set S) ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₁ : a ∈ (p.aroots S).toFinset ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  a ∈ (p.aroots S).toFinset ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₂ : a ∈ p.aroots S ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  a ∈ (p.aroots S).toFinset ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₂ :
  a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₃ : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw : a ∈ (↑(p.aroots S).toFinset : Set S) ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₁ : a ∈ (p.aroots S).toFinset ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  a ∈ (p.aroots S).toFinset ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₂ : a ∈ p.aroots S ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  a ∈ (p.aroots S).toFinset ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₂ :
  a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₃ : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : S
⊢ a ∈ p.rootSet S ↔ p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
  p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : S
rw :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
    p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔ p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₁ : p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
  p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ (C : (a : R) → R[X]) a
⊢ Set.preimage (β := R) (fun (x : R) ↦ eval x p) {a} =
    (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).rootSet R
have h : ∀ (x : R),
  Membership.mem (γ := Set R) (Set.preimage (β := R) (fun (x : R) ↦ eval x p) {a}) x ↔
    x ∈ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).rootSet R
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : CommRing S'
inst_5 : IsDomain S'
inst_6 : Algebra T S'
hp : Eq (α := S'[X]) (map (algebraMap T S') p) 0 → Eq (α := S[X]) (map (algebraMap T S) p) 0
f : S →ₐ[T] S'
x : S
hx : x ∈ p.rootSet S
⊢ Membership.mem (α := S') (p.rootSet S') ((f : (a : S) → S') x : S')
have rw : ∀ (hx : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval x : (a : T[X]) → S) p : S) (0 : S)),
  Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧
    Eq.{u_2 + 1} (α := S') (((aeval ((f : (a : S) → S') x) : T[X] →ₐ[T] S') : (a : T[X]) → S') p : S') (0 : S')
Tactic: rw [mem_rootSet'] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : CommRing S'
inst_5 : IsDomain S'
inst_6 : Algebra T S'
hp : Eq (α := S'[X]) (map (algebraMap T S') p) 0 → Eq (α := S[X]) (map (algebraMap T S) p) 0
f : S →ₐ[T] S'
x : S
hx : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval x : (a : T[X]) → S) p : S) (0 : S)
⊢ Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧
    Eq.{u_2 + 1} (α := S') (((aeval ((f : (a : S) → S') x) : T[X] →ₐ[T] S') : (a : T[X]) → S') p : S') (0 : S')
have rw : Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧ Eq.{u_2 + 1} (α := S') 0 0
Tactic: rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
p : T[X]
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
h : a ∈ p.rootSet S
hf : p = 0
⊢ False
have rwa : ∀ (h : a ∈ rootSet.{w, v} (T := T) 0 S) (hf : p = 0), False
Tactic: rwa [hf, rootSet_zero] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
S : Type v
T : Type w
inst : CommRing T
p : T[X]
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
h : a ∈ p.rootSet S
hf : p = 0
rwa : ∀ (h : a ∈ rootSet.{w, v} (T := T) 0 S) (hf : p = 0), False
⊢ False
have rwa₁ : ∀ (h : Membership.mem (γ := Set S) ∅ a) (hf : p = 0), False
Tactic: rwa [hf, rootSet_zero] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f : (a : S) → S') (p.rootSet S) (p.rootSet S')
have refine : ∀ (h₀ : Eq (α := S'[X]) (map (algebraMap T S') p) 0), Eq (α := S[X]) (map (algebraMap T S) p) 0
Tactic: refine rootSet_maps_to' (fun h₀ => ?_) f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
T : Type w
inst : CommRing T
p : T[X]
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : Eq (α := S'[X]) (map (algebraMap T S') p) 0
⊢ Eq (α := S[X]) (map (algebraMap T S) p) 0
have obtain : ∀ (h₀ : Eq (α := S'[X]) (map (algebraMap T S') 0) 0), Eq (α := S[X]) (map (algebraMap T S) 0) 0
Tactic: obtain rfl : p = 0 :=
    map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])
Cleared hypotheses: p, h₀
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
h : 0 < n
a : R
⊢ (↑(nthRootsFinset n a) : Set R) = {r : R | r ^ n = a}
have h₁ : ∀ (x : R), x ∈ (↑(nthRootsFinset n a) : Set R) ↔ Membership.mem (γ := Set R) {r : R | r ^ n = a} x
Tactic: ext x