awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
h : IsConjRoot K x y
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
have obtain : ∀ (σ : L →ₐ[K] L) (hσ : (σ : (a : L) → L) y = x), ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
Tactic: obtain ⟨σ, hσ⟩ :=
    exists_algHom_of_splits_of_aeval (normal_iff.mp inferInstance) (h ▸ minpoly.aeval K x)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
⊢ IsConjRoot K x y ↔ y ∈ aroots (minpoly K x) S
have rw : Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) ↔
  Ne (α := K[X]) (minpoly K x) 0 ∧
    Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S)
Tactic: rw [Polynomial.mem_aroots, isConjRoot_iff_aeval_eq_zero h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
⊢ Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) ↔
    Ne (α := K[X]) (minpoly K x) 0 ∧
      Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S)
have simp : Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) → Ne (α := K[X]) (minpoly K x) 0
Tactic: simp only [iff_and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : IsDomain R
inst_5 : IsTorsionFree R S
r : R
x : S
h : IsConjRoot R ((algebraMap R S : (a : R) → S) r) x
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ x = (algebraMap R S : (a : R) → S) r
have h₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) = minpoly R x
Tactic: rw [IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj _ hf] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : IsDomain R
inst_5 : IsTorsionFree R S
r : R
x : S
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) = minpoly R x
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ x ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).aroots S
have rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ≠ 0 ∧
  Eq.{u_4 + 1} (α := S)
    ((Polynomial.aeval x : (a : R[X]) → S) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : S)
    (0 : S)
Tactic: rw [mem_aroots]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : IsDomain R
inst_5 : IsTorsionFree R S
r : R
x : S
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) = minpoly R x
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ x = (algebraMap R S : (a : R) → S) r
have this : x ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).aroots S
Tactic: have : x ∈ (X - C r).aroots S := by
    rw [mem_aroots]
    simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)
have rw : HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
    (map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) =
  map (algebraMap R S) (minpoly R x)
Tactic: rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
rw :
  HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      (map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) =
    map (algebraMap R S) (minpoly R x)
⊢ map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)
have rw₁ : IsRoot (map (algebraMap R S) (minpoly R x)) x
Tactic: rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
rw :
  HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      (map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) =
    map (algebraMap R S) (minpoly R x)
rw₁ : IsRoot (map (algebraMap R S) (minpoly R x)) x
⊢ map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)
have rw₂ : eval x (map (algebraMap R S) (minpoly R x)) = 0
Tactic: rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
rw :
  HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      (map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) =
    map (algebraMap R S) (minpoly R x)
rw₁ : IsRoot (map (algebraMap R S) (minpoly R x)) x
rw₂ : eval x (map (algebraMap R S) (minpoly R x)) = 0
⊢ map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)
have rw₃ : Eq.{u_1 + 1} (α := S) ((aeval x : (a : R[X]) → S) (minpoly R x) : S) (0 : S)
Tactic: rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
rw :
  HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      (map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) =
    map (algebraMap R S) (minpoly R x)
rw₁ : IsRoot (map (algebraMap R S) (minpoly R x)) x
rw₂ : eval x (map (algebraMap R S) (minpoly R x)) = 0
rw₃ : Eq.{u_1 + 1} (α := S) ((aeval x : (a : R[X]) → S) (minpoly R x) : S) (0 : S)
⊢ map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)
have rw₄ : Eq.{u_1 + 1} (α := S) 0 0
Tactic: rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
⊢ coeff (minpolyDiv R x) i =
    HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + 1)) : S)
      (coeff (minpolyDiv R x) (i + 1) * x)
have rw : coeff (minpolyDiv R x) i =
  (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).coeff (i + 1) +
    coeff (minpolyDiv R x) (i + 1) * x
Tactic: rw [← coeff_map, ← minpolyDiv_spec R x]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : ¬IsIntegral R x
⊢ map (algebraMap R S)
        (if hx : IsIntegral R x then
          WellFounded.min (r := fun (p q : R[X]) ↦ p.degree < q.degree) ⋯
            (fun (x_1 : R[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap R S) x x_1 = 0) hx
        else 0) /ₘ
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    0
have rw : map (algebraMap R S) 0 /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) = 0
Tactic: rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : ¬IsIntegral R x
rw : map (algebraMap R S) 0 /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) = 0
⊢ map (algebraMap R S)
        (if hx : IsIntegral R x then
          WellFounded.min (r := fun (p q : R[X]) ↦ p.degree < q.degree) ⋯
            (fun (x_1 : R[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap R S) x x_1 = 0) hx
        else 0) /ₘ
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    0
have rw₁ : 0 /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) = 0
Tactic: rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : ¬IsIntegral R x
rw : map (algebraMap R S) 0 /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) = 0
rw₁ : 0 /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) = 0
⊢ map (algebraMap R S)
        (if hx : IsIntegral R x then
          WellFounded.min (r := fun (p q : R[X]) ↦ p.degree < q.degree) ⋯
            (fun (x_1 : R[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap R S) x x_1 = 0) hx
        else 0) /ₘ
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    0
have rw₂ : Eq.{u_2 + 1} (α := S[X]) 0 0
Tactic: rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ eval x (minpolyDiv R x) = (aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X])
have rw : eval x (minpolyDiv R x) =
  eval x
    ((derivative : (a : S[X]) → S[X])
      (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])))
Tactic: rw [← eval_map_algebraMap, ← derivative_map, ← minpolyDiv_spec R x]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : IsDomain S
y : S
hxy : y ≠ x
hy : Eq.{u_1 + 1} (α := S) ((aeval y : (a : R[X]) → S) (minpoly R x) : S) (0 : S)
⊢ eval y (minpolyDiv R x) = 0
have hy₁ : eval y (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) = 0
Tactic: rw [← eval_map_algebraMap, ← minpolyDiv_spec R x] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) = 0
⊢ eval y (minpolyDiv R x) = 0
have hy₁ : eval y (minpolyDiv R x) = 0 ∨ y - x = 0
Tactic: simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x) = 0 ∨ y - x = 0
⊢ ¬y - x = 0
have rwa : ¬y = x
Tactic: rwa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : IsDomain T
inst_5 : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
⊢ eval₂ σ y (minpolyDiv R x) =
    if (σ : (a : S) → T) x = y then
      (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
    else 0
have pos : ∀ (h : (σ : (a : S) → T) x = y),
  eval₂ σ y (minpolyDiv R x) =
    (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : IsDomain T
inst_5 : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
pos :
  ∀ (h : (σ : (a : S) → T) x = y),
    eval₂ σ y (minpolyDiv R x) =
      (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
⊢ eval₂ σ y (minpolyDiv R x) =
    if (σ : (a : S) → T) x = y then
      (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
    else 0
have neg : ∀ (h : ¬(σ : (a : S) → T) x = y), eval₂ σ y (minpolyDiv R x) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : IsDomain T
inst_5 : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : (σ : (a : S) → T) x = y
⊢ eval₂ σ y (minpolyDiv R x) =
    (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
have pos : eval₂ σ ((σ : (a : S) → T) x) (minpolyDiv R x) =
  (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
Tactic: rw [← h, eval₂_hom, eval_minpolyDiv_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : IsDomain T
inst_5 : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : (σ : (a : S) → T) x = y
pos :
  eval₂ σ ((σ : (a : S) → T) x) (minpolyDiv R x) =
    (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
⊢ eval₂ σ y (minpolyDiv R x) =
    (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
have pos₁ : Eq.{u_1 + 1} (α := T) ((σ : (a : S) → T) (eval x (minpolyDiv R x)) : T)
  ((σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S) : T)
Tactic: rw [← h, eval₂_hom, eval_minpolyDiv_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : IsDomain T
inst_5 : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : (σ : (a : S) → T) x = y
pos :
  eval₂ σ ((σ : (a : S) → T) x) (minpolyDiv R x) =
    (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
pos₁ :
  Eq.{u_1 + 1} (α := T) ((σ : (a : S) → T) (eval x (minpolyDiv R x)) : T)
    ((σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S) : T)
⊢ eval₂ σ y (minpolyDiv R x) =
    (σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
have pos₂ : Eq.{u_1 + 1} (α := T)
  ((σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S) : T)
  ((σ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S) : T)
Tactic: rw [← h, eval₂_hom, eval_minpolyDiv_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
Goal:
R : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : IsDomain T
inst_5 : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : ¬(σ : (a : S) → T) x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0
have hy₁ : eval₂ σ y (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) = 0
Tactic: rw [← eval₂_map, ← minpolyDiv_spec] at hy
Cleared hypotheses: hy, h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ (↑σ₁ : S →+* T) ((σ₂ : (a : S) → T) x) (minpolyDiv R x) =
    if Eq.{u_1 + 1} (α := T) ((σ₁ : (a : S) → T) x : T) ((σ₂ : (a : S) → T) x : T) then
      (σ₁ : (a : S) → T) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) : S)
    else 0
have hy : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
    (minpoly R x) =
  0
Tactic: apply eval₂_minpolyDiv_of_eval₂_eq_zero
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₁ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
    (minpoly R x) =
  0
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
hy₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₂ : eval₂ (↑σ₂ : S →+* T) ((σ₂ : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
hy₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
hy₂ : eval₂ (↑σ₂ : S →+* T) ((σ₂ : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₃ : eval₂ (↑σ₂ : S →+* T) (((↑σ₂ : S →+* T) : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
hy₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
hy₂ : eval₂ (↑σ₂ : S →+* T) ((σ₂ : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₃ : eval₂ (↑σ₂ : S →+* T) (((↑σ₂ : S →+* T) : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₄ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) (eval x (map (algebraMap R S) (minpoly R x))) : T) (0 : T)
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
hy₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
hy₂ : eval₂ (↑σ₂ : S →+* T) ((σ₂ : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₃ : eval₂ (↑σ₂ : S →+* T) (((↑σ₂ : S →+* T) : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₄ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) (eval x (map (algebraMap R S) (minpoly R x))) : T) (0 : T)
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₅ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) ((aeval x : (a : R[X]) → S) (minpoly R x) : S) : T) (0 : T)
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]