awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
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)
⊢ Eq (α := Multiset R) (nthRoots 2 1) {-1, 1}
have h₂ : HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 ≠ 0
Tactic: have h₂ : (X ^ 2 - C 1 : R[X]) ≠ 0 := fun h ↦ by simpa using congrArg (coeff · 0) h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
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)
h₂ : HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 ≠ 0
⊢ Eq (α := Multiset R) (nthRoots 2 1) {-1, 1}
have rw : HAdd.hAdd (α := Multiset R) {-1} {1} = {-1, 1}
Tactic: rw [nthRoots, h₁, roots_mul (h₁ ▸ h₂), roots_X_add_C, roots_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ 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
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ False
have refine : Fintype R
Tactic: refine @Fintype.false R _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ p = 0
have by_contra : ¬p = 0 → False
Tactic: classical
  by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
⊢ p = 0
have by_contra₃ : (hp : ¬p = 0) → Fintype R
Tactic: classical
  by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ 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
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ p - q = 0
have h : ∀ (x : R), eval x (p - q) = 0
Tactic: apply zero_of_eval_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x (p - q) = 0
have h : eval x p - eval x q = 0
Tactic: rw [eval_sub, sub_eq_zero, ext]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
h : eval x p - eval x q = 0
⊢ eval x (p - q) = 0
have h₁ : eval x p = eval x q
Tactic: rw [eval_sub, sub_eq_zero, ext]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
h : eval x p - eval x q = 0
h₁ : eval x p = eval x q
⊢ eval x (p - q) = 0
have h₂ : eval x q = eval x q
Tactic: rw [eval_sub, sub_eq_zero, ext]
-- 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
p : T[X]
a : S
⊢ a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ IsRoot (map (algebraMap T S) p) a ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]
-- 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
p : T[X]
a : S
rw :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ IsRoot (map (algebraMap T S) p) a ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₁ : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval a (map (algebraMap T S) p) = 0 ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]
-- 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
p : T[X]
a : S
rw :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ IsRoot (map (algebraMap T S) p) a ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval a (map (algebraMap T S) p) = 0 ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₂ : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0 ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
Tactic: rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]
-- 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
p : T[X]
a : S
rw :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ IsRoot (map (algebraMap T S) p) a ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval a (map (algebraMap T S) p) = 0 ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₂ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0 ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw₃ : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0 ↔
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0
Tactic: rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]
-- 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
p : T[X]
a : S
⊢ a ∈ p.aroots S ↔ p ≠ 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
have rw : Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)
Tactic: rw [mem_aroots', Polynomial.map_ne_zero_iff]
-- 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
p q : T[X]
hpq : p * q ≠ 0
this : HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S
have rw : roots (map (algebraMap T S) (p * q)) = p.aroots S + q.aroots S
Tactic: rw [aroots_def, Polynomial.map_mul, roots_mul this]
-- 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
p q : T[X]
hpq : p * q ≠ 0
this : HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
rw : roots (map (algebraMap T S) (p * q)) = p.aroots S + q.aroots S
⊢ (p * q).aroots S = p.aroots S + q.aroots S
have rw₁ : (HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q)).roots = p.aroots S + q.aroots S
Tactic: rw [aroots_def, Polynomial.map_mul, roots_mul this]
-- 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
p q : T[X]
hpq : p * q ≠ 0
this : HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
rw : roots (map (algebraMap T S) (p * q)) = p.aroots S + q.aroots S
rw₁ : (HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q)).roots = p.aroots S + q.aroots S
⊢ (p * q).aroots S = p.aroots S + q.aroots S
have rw₂ : roots (map (algebraMap T S) p) + roots (map (algebraMap T S) q) = p.aroots S + q.aroots S
Tactic: rw [aroots_def, Polynomial.map_mul, roots_mul this]
-- 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
p q : T[X]
hpq : p * q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S
have suffices : HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
Tactic: suffices map (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by
    rw [aroots_def, Polynomial.map_mul, roots_mul this]
-- 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
p q : T[X]
hpq : p * q ≠ 0
⊢ HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
have rwa : Ne (α := S[X]) (map (algebraMap T S) (p * q)) 0
Tactic: rwa [← Polynomial.map_mul, Polynomial.map_ne_zero_iff
    (FaithfulSMul.algebraMap_injective T S)]
-- 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
r : T
⊢ (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X])).aroots S =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
have rw : roots (map (algebraMap T S) (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X]))) =
  singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
Tactic: rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]
-- 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
r : T
rw :
  roots (map (algebraMap T S) (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X]))) =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
⊢ (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X])).aroots S =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
have rw₁ : (HSub.hSub (α := S[X]) (map (algebraMap T S : T →+* S) X)
      (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
  singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
Tactic: rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]
-- 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
r : T
rw :
  roots (map (algebraMap T S) (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X]))) =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₁ :
  (HSub.hSub (α := S[X]) (map (algebraMap T S : T →+* S) X)
        (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
⊢ (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X])).aroots S =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
have rw₂ : (HSub.hSub (α := S[X]) X (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
  singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
Tactic: rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]
-- 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
r : T
rw :
  roots (map (algebraMap T S) (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X]))) =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₁ :
  (HSub.hSub (α := S[X]) (map (algebraMap T S : T →+* S) X)
        (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₂ :
  (HSub.hSub (α := S[X]) X (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
⊢ (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X])).aroots S =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
have rw₃ : (HSub.hSub (α := S[X]) (β := S[X]) X
      ((C : (a : S) → S[X]) (((algebraMap T S : T →+* S) : (a : T) → S) r) : S[X])).roots =
  singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
Tactic: rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]
-- 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
r : T
rw :
  roots (map (algebraMap T S) (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X]))) =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₁ :
  (HSub.hSub (α := S[X]) (map (algebraMap T S : T →+* S) X)
        (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₂ :
  (HSub.hSub (α := S[X]) X (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₃ :
  (HSub.hSub (α := S[X]) (β := S[X]) X
        ((C : (a : S) → S[X]) (((algebraMap T S : T →+* S) : (a : T) → S) r) : S[X])).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
⊢ (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X])).aroots S =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
have rw₄ : Eq (α := Multiset S) (singleton (α := S) (((algebraMap T S : T →+* S) : (a : T) → S) r : S))
  (singleton (α := S) ((algebraMap T S : (a : T) → S) r : S))
Tactic: rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]
-- 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
⊢ aroots.{w, v} (T := T) X S = {0}
have rw : roots (map (algebraMap T S) X) = {0}
Tactic: rw [aroots_def, map_X, roots_X]
-- 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
rw : roots (map (algebraMap T S) X) = {0}
⊢ aroots.{w, v} (T := T) X S = {0}
have rw₁ : Eq (α := Multiset S) (roots X) {0}
Tactic: rw [aroots_def, map_X, roots_X]
-- 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
rw : roots (map (algebraMap T S) X) = {0}
rw₁ : Eq (α := Multiset S) (roots X) {0}
⊢ aroots.{w, v} (T := T) X S = {0}
have rw₂ : Eq (α := Multiset S) {0} {0}
Tactic: rw [aroots_def, map_X, roots_X]
-- 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
⊢ aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = 0
have rw : roots (map (algebraMap T S) ((C : (a : T) → T[X]) a)) = 0
Tactic: rw [aroots_def, map_C, roots_C]
-- 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 : roots (map (algebraMap T S) ((C : (a : T) → T[X]) a)) = 0
⊢ aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = 0
have rw₁ : Eq.{v + 1} (α := Multiset S) (roots ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a))) 0
Tactic: rw [aroots_def, map_C, roots_C]
-- 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 : roots (map (algebraMap T S) ((C : (a : T) → T[X]) a)) = 0
rw₁ : Eq.{v + 1} (α := Multiset S) (roots ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a))) 0
⊢ aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = 0
have rw₂ : Eq.{v + 1} (α := Multiset S) 0 0
Tactic: rw [aroots_def, map_C, roots_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
⊢ aroots.{w, u_1} (T := T) 0 S = 0
have rw : aroots.{w, u_1} (T := T) ((C : (a : T) → T[X]) 0) S = 0
Tactic: rw [← C_0, aroots_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 : aroots.{w, u_1} (T := T) ((C : (a : T) → T[X]) 0) S = 0
⊢ aroots.{w, u_1} (T := T) 0 S = 0
have rw₁ : Eq.{u_1 + 1} (α := Multiset S) 0 0
Tactic: rw [← C_0, aroots_C]
-- 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
p : T[X]
⊢ (-p).aroots S = p.aroots S
have rw : roots (map (algebraMap T S) (-p)) = p.aroots S
Tactic: rw [aroots, Polynomial.map_neg, roots_neg]
-- 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
p : T[X]
rw : roots (map (algebraMap T S) (-p)) = p.aroots S
⊢ (-p).aroots S = p.aroots S
have rw₁ : roots (-map (algebraMap T S) p) = p.aroots S
Tactic: rw [aroots, Polynomial.map_neg, roots_neg]
-- 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
p : T[X]
rw : roots (map (algebraMap T S) (-p)) = p.aroots S
rw₁ : roots (-map (algebraMap T S) p) = p.aroots S
⊢ (-p).aroots S = p.aroots S
have rw₂ : roots (map (algebraMap T S) p) = p.aroots S
Tactic: rw [aroots, Polynomial.map_neg, roots_neg]
-- 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
p : T[X]
ha : a ≠ 0
⊢ (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) p).aroots S = p.aroots S
have ha₁ : Ne.{v + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
Tactic: rw [aroots_def, Polynomial.map_mul, map_C, roots_C_mul]
-- 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
p : T[X]
ha : a ≠ 0
⊢ Ne.{v + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
have ha₁ : Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)
Tactic: rwa [map_ne_zero_iff]
-- 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
p : T[X]
ha : a ≠ 0
⊢ (a • p).aroots S = p.aroots S
have rw : (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) p).aroots S = p.aroots S
Tactic: rw [smul_eq_C_mul, aroots_C_mul _ 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
p : T[X]
ha : a ≠ 0
rw : (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) p).aroots S = p.aroots S
⊢ (a • p).aroots S = p.aroots S
have rw₁ : p.aroots S = p.aroots S
Tactic: rw [smul_eq_C_mul, aroots_C_mul _ ha]
-- 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
p : T[X]
n : ℕ
⊢ (p ^ n).aroots S = n • p.aroots S
have rw : roots (map (algebraMap T S) (p ^ n)) = n • p.aroots S
Tactic: rw [aroots_def, Polynomial.map_pow, roots_pow]
-- 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
p : T[X]
n : ℕ
rw : roots (map (algebraMap T S) (p ^ n)) = n • p.aroots S
⊢ (p ^ n).aroots S = n • p.aroots S
have rw₁ : (HPow.hPow (α := S[X]) (map (algebraMap T S) p) n).roots = n • p.aroots S
Tactic: rw [aroots_def, Polynomial.map_pow, roots_pow]
-- 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
p : T[X]
n : ℕ
rw : roots (map (algebraMap T S) (p ^ n)) = n • p.aroots S
rw₁ : (HPow.hPow (α := S[X]) (map (algebraMap T S) p) n).roots = n • p.aroots S
⊢ (p ^ n).aroots S = n • p.aroots S
have rw₂ : n • roots (map (algebraMap T S) p) = n • p.aroots S
Tactic: rw [aroots_def, Polynomial.map_pow, roots_pow]
-- 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
n : ℕ
⊢ (HPow.hPow (α := T[X]) X n).aroots S = HSMul.hSMul (β := Multiset S) n {0}
have rw : n • aroots.{w, v} (T := T) X S = HSMul.hSMul (β := Multiset S) n {0}
Tactic: rw [aroots_pow, aroots_X]
-- 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
n : ℕ
rw : n • aroots.{w, v} (T := T) X S = HSMul.hSMul (β := Multiset S) n {0}
⊢ (HPow.hPow (α := T[X]) X n).aroots S = HSMul.hSMul (β := Multiset S) n {0}
have rw₁ : HSMul.hSMul (β := Multiset S) n {0} = HSMul.hSMul (β := Multiset S) n {0}
Tactic: rw [aroots_pow, aroots_X]
-- 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 : ℕ
⊢ (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}
have rw : (HPow.hPow (α := T[X]) X n).aroots S = HSMul.hSMul (β := Multiset S) n {0}
Tactic: rw [aroots_C_mul _ ha, aroots_X_pow]
-- 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 : (HPow.hPow (α := T[X]) X n).aroots S = HSMul.hSMul (β := Multiset S) n {0}
⊢ (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}
have rw₁ : HSMul.hSMul (β := Multiset S) n {0} = HSMul.hSMul (β := Multiset S) n {0}
Tactic: rw [aroots_C_mul _ ha, aroots_X_pow]