awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
⊢ p.roots = S.val
have refine_1 : S.val ≤ p.roots
Tactic: refine (Multiset.eq_of_le_of_card_le ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
refine_1 : S.val ≤ p.roots
⊢ p.roots = S.val
have refine_2 : p.roots.card ≤ S.val.card
Tactic: refine (Multiset.eq_of_le_of_card_le ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : (↑(#S) : WithBot ℕ) = p.degree
⊢ p ≠ 0
have contrapose! : ∀ (hcard : p = 0), (↑(#S) : WithBot ℕ) ≠ p.degree
Tactic: contrapose! hcard
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₃ : eval x (HPow.hPow (α := R[X]) X n) - eval x ((C : (a : R) → R[X]) a) = 0 ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
rw₃ : eval x (HPow.hPow (α := R[X]) X n) - eval x ((C : (a : R) → R[X]) a) = 0 ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₄ : eval x (HPow.hPow (α := R[X]) X n) - a = 0 ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
rw₃ : eval x (HPow.hPow (α := R[X]) X n) - eval x ((C : (a : R) → R[X]) a) = 0 ↔ x ^ n = a
rw₄ : eval x (HPow.hPow (α := R[X]) X n) - a = 0 ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₅ : eval x X ^ n - a = 0 ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
rw₃ : eval x (HPow.hPow (α := R[X]) X n) - eval x ((C : (a : R) → R[X]) a) = 0 ↔ x ^ n = a
rw₄ : eval x (HPow.hPow (α := R[X]) X n) - a = 0 ↔ x ^ n = a
rw₅ : eval x X ^ n - a = 0 ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₆ : x ^ n - a = 0 ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
rw₃ : eval x (HPow.hPow (α := R[X]) X n) - eval x ((C : (a : R) → R[X]) a) = 0 ↔ x ^ n = a
rw₄ : eval x (HPow.hPow (α := R[X]) X n) - a = 0 ↔ x ^ n = a
rw₅ : eval x X ^ n - a = 0 ↔ x ^ n = a
rw₆ : x ^ n - a = 0 ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a
have rw₇ : x ^ n = a ↔ x ^ n = a
Tactic: rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, 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
n : ℕ
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)
have rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
Tactic: rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)
have rw₁ : (HPow.hPow (α := R[X]) X n - 0).roots = replicate n 0
Tactic: rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
rw₁ : (HPow.hPow (α := R[X]) X n - 0).roots = replicate n 0
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)
have rw₂ : (HPow.hPow (α := R[X]) X n).roots = replicate n 0
Tactic: rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
rw₁ : (HPow.hPow (α := R[X]) X n - 0).roots = replicate n 0
rw₂ : (HPow.hPow (α := R[X]) X n).roots = replicate n 0
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)
have rw₃ : HSMul.hSMul (β := Multiset R) n (roots X) = replicate n 0
Tactic: rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
rw₁ : (HPow.hPow (α := R[X]) X n - 0).roots = replicate n 0
rw₂ : (HPow.hPow (α := R[X]) X n).roots = replicate n 0
rw₃ : HSMul.hSMul (β := Multiset R) n (roots X) = replicate n 0
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)
have rw₄ : HSMul.hSMul (β := Multiset R) n {0} = replicate n 0
Tactic: rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
rw₁ : (HPow.hPow (α := R[X]) X n - 0).roots = replicate n 0
rw₂ : (HPow.hPow (α := R[X]) X n).roots = replicate n 0
rw₃ : HSMul.hSMul (β := Multiset R) n (roots X) = replicate n 0
rw₄ : HSMul.hSMul (β := Multiset R) n {0} = replicate n 0
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)
have rw₅ : Eq.{u_1 + 1} (α := Multiset R) (replicate n 0) (replicate n 0)
Tactic: rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree ≤ (↑n : WithBot ℕ)
have rw : degree.{u} (R := R) ((C : (a : R) → R[X]) (1 - a)) ≤ (↑0 : WithBot ℕ)
Tactic: rw [hn, pow_zero, ← C_1, ← map_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ (nthRoots n a).card ≤ n
have rw : LE.le (α := WithBot ℕ) (↑(nthRoots n a).card : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [← Nat.cast_le (α := WithBot ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ LE.le (α := WithBot ℕ) (↑(nthRoots n a).card : WithBot ℕ) (↑n : WithBot ℕ)
have rw : (↑(nthRoots n a).card : WithBot ℕ) ≤
  (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree
Tactic: rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r
have simp_rw : nthRoots 2 r = 0 ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
Tactic: simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_notMem, mem_nthRoots (by simp : 0 < 2),
    ← not_exists, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
simp_rw : nthRoots 2 r = 0 ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r
have simp_rw₁ : (∀ (a : R), a ∉ nthRoots 2 r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
Tactic: simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_notMem, mem_nthRoots (by simp : 0 < 2),
    ← not_exists, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
simp_rw : nthRoots 2 r = 0 ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
simp_rw₁ : (∀ (a : R), a ∉ nthRoots 2 r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r
have simp_rw₂ : (∀ (a : R), ¬HPow.hPow (β := ℕ) a 2 = r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
Tactic: simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_notMem, mem_nthRoots (by simp : 0 < 2),
    ← not_exists, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
simp_rw : nthRoots 2 r = 0 ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
simp_rw₁ : (∀ (a : R), a ∉ nthRoots 2 r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
simp_rw₂ : (∀ (a : R), ¬HPow.hPow (β := ℕ) a 2 = r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r
have simp_rw₃ : (¬∃ (x : R), HPow.hPow (β := ℕ) x 2 = r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
Tactic: simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_notMem, mem_nthRoots (by simp : 0 < 2),
    ← not_exists, eq_comm]
-- 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 x : R
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a
have rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
Tactic: rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots 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 x : R
rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a
have rw₁ : x ∈ nthRoots n a ↔ x ^ n = a
Tactic: rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots 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 x : R
rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
rw₁ : x ∈ nthRoots n a ↔ x ^ n = a
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a
have rw₂ : x ^ n = a ↔ x ^ n = a
Tactic: rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots 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 x : R
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a
have rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
Tactic: classical
  rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots 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 x : R
rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a
have rw₁ : x ∈ nthRoots n a ↔ x ^ n = a
Tactic: classical
  rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots 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 x : R
rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
rw₁ : x ∈ nthRoots n a ↔ x ^ n = a
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a
have rw₂ : x ^ n = a ↔ x ^ n = a
Tactic: classical
  rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
have pos : ∀ (hn : n = 0),
  Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
pos :
  ∀ (hn : n = 0),
    Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
      ((f : (a : R) → S) x : S)
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
have neg : ∀ (hn : ¬n = 0),
  Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
have neg : HPow.hPow (α := S) ((f : (a : R) → S) x : S) n = (f : (a : R) → S) a
Tactic: rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
neg : HPow.hPow (α := S) ((f : (a : R) → S) x : S) n = (f : (a : R) → S) a
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
have neg₁ : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (x ^ n) : S) ((f : (a : R) → S) a : S)
Tactic: rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
neg : HPow.hPow (α := S) ((f : (a : R) → S) x : S) n = (f : (a : R) → S) a
neg₁ : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (x ^ n) : S) ((f : (a : R) → S) a : S)
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)
have neg₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) a : S)
Tactic: rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
x : R
hx : Membership.mem (γ := Finset R) (nthRootsFinset n 1) x
f : F
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n 1) ((f : (a : R) → S) x : S)
have rw : Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) 1) : Finset S)
  ((f : (a : R) → S) x : S)
Tactic: rw [← (map_one f)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ∈ nthRootsFinset (n + 1) a₁
hη₂ : η₂ ∈ nthRootsFinset (n + 1) a₂
⊢ η₁ * η₂ ∈ nthRootsFinset (n + 1) (a₁ * a₂)
have succ : ∀ (hη₁ : η₁ ^ n.succ = a₁) (hη₂ : η₂ ^ n.succ = a₂), (η₁ * η₂) ^ n.succ = a₁ * a₂
Tactic: rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
Cleared hypotheses: hη₁, hη₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂
have succ : η₁ ^ n.succ * η₂ ^ n.succ = a₁ * a₂
Tactic: rw [mul_pow, hη₁, hη₂]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
succ : η₁ ^ n.succ * η₂ ^ n.succ = a₁ * a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂
have succ₁ : a₁ * η₂ ^ n.succ = a₁ * a₂
Tactic: rw [mul_pow, hη₁, hη₂]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
succ : η₁ ^ n.succ * η₂ ^ n.succ = a₁ * a₂
succ₁ : a₁ * η₂ ^ n.succ = a₁ * a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂
have succ₂ : a₁ * a₂ = a₁ * a₂
Tactic: rw [mul_pow, hη₁, hη₂]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset n a₁
hη₂ : η₂ ∈ nthRootsFinset n a₂
⊢ η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂)
have zero : ∀ (hη₁ : η₁ ∈ nthRootsFinset 0 a₁) (hη₂ : η₂ ∈ nthRootsFinset 0 a₂), η₁ * η₂ ∈ nthRootsFinset 0 (a₁ * a₂)
Tactic: cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]
Cleared hypotheses: n, hη₁, hη₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset n a₁
hη₂ : η₂ ∈ nthRootsFinset n a₂
zero : ∀ (hη₁ : η₁ ∈ nthRootsFinset 0 a₁) (hη₂ : η₂ ∈ nthRootsFinset 0 a₂), η₁ * η₂ ∈ nthRootsFinset 0 (a₁ * a₂)
⊢ η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂)
have succ : ∀ (n : ℕ) (hη₁ : η₁ ∈ nthRootsFinset (n + 1) a₁) (hη₂ : η₂ ∈ nthRootsFinset (n + 1) a₂),
  η₁ * η₂ ∈ nthRootsFinset (n + 1) (a₁ * a₂)
Tactic: cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]
Cleared hypotheses: n, hη₁, hη₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
n : ℕ
hη : 0 ∈ nthRootsFinset (n + 1) a
⊢ False
have hη₁ : 0 = a
Tactic: rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
Cleared hypotheses: hη
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset n a
⊢ False
have zero : ∀ (hη : 0 ∈ nthRootsFinset 0 a), False
Tactic: cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
    exact ha hη.symm
Cleared hypotheses: n, hη
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset n a
zero : ∀ (hη : 0 ∈ nthRootsFinset 0 a), False
⊢ False
have succ : ∀ (n : ℕ) (hη : 0 ∈ nthRootsFinset (n + 1) a), False
Tactic: cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
    exact ha hη.symm
Cleared hypotheses: n, hη
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
hn : 0 < n
⊢ Membership.mem (γ := Finset R) (nthRootsFinset n 1) 1
have rw : HPow.hPow (α := R) 1 n = 1
Tactic: rw [mem_nthRootsFinset hn, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
hn : 0 < n
rw : HPow.hPow (α := R) 1 n = 1
⊢ Membership.mem (γ := Finset R) (nthRootsFinset n 1) 1
have rw₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [mem_nthRootsFinset hn, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq (α := Multiset R) (nthRoots 2 1) {-1, 1}
have h₁ : HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
  HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)
Tactic: have h₁ : (X ^ 2 - C 1 : R[X]) = (X + C 1) * (X - C 1) := by simp [← sq_sub_sq]