awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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)
⊢ 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

Premises used: IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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)
h₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) = minpoly R x
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
rw [IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj _ hf] at h

Premises used: IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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)
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)
⊢ x ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).aroots S

Tactic:
rw [mem_aroots]

Premises used: Polynomial.mem_aroots
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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)
⊢ 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:
simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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

Tactic:
have : x ∈ (X - C r).aroots S := by
    rw [mem_aroots]
    simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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)
this : x ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).aroots S
⊢ x = (algebraMap R S : (a : R) → S) r

Tactic:
simpa [aroots_X_sub_C] using this

Premises used: Polynomial.aroots_X_sub_C
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
r : K
x : S
h : IsConjRoot K ((algebraMap K S : (a : K) → S) r) x
⊢ x = (algebraMap K S : (a : K) → S) r

Tactic:
eq_algebraMap_of_injective h (algebraMap K S).injective

Premises used: Algebra.algebraMap, RingHom.injective, IsConjRoot.eq_algebraMap_of_injective
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
x : S
h : IsConjRoot R 0 x
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ x = 0

Tactic:
(algebraMap R S).map_zero ▸ (eq_algebraMap_of_injective ((algebraMap R S).map_zero ▸ h) hf)

Premises used: Algebra.algebraMap, Eq.rec, RingHom.map_zero, IsConjRoot.eq_algebraMap_of_injective, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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 : S
h : IsConjRoot K 0 x
⊢ x = 0

Tactic:
eq_zero_of_injective h (algebraMap K S).injective

Premises used: Algebra.algebraMap, IsConjRoot.eq_zero_of_injective, RingHom.injective
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsConjRoot R ((algebraMap R S : (a : R) → S) r) x ↔ x = (algebraMap R S : (a : R) → S) r

Tactic:
⟨fun h => eq_algebraMap_of_injective h hf, fun h => h.symm ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, IsConjRoot.eq_algebraMap_of_injective, Eq.symm, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
r : K
x : S
⊢ IsConjRoot K ((algebraMap K S : (a : K) → S) r) x ↔ x = (algebraMap K S : (a : K) → S) r

Tactic:
isConjRoot_iff_eq_algebraMap_of_injective (algebraMap K S).injective

Premises used: Algebra.algebraMap, isConjRoot_iff_eq_algebraMap_of_injective, RingHom.injective
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
r : K
x : S
⊢ IsConjRoot K x ((algebraMap K S : (a : K) → S) r) ↔ x = (algebraMap K S : (a : K) → S) r

Tactic:
eq_comm.trans <| isConjRoot_iff_eq_algebraMap_of_injective (algebraMap K S).injective

Premises used: Algebra.algebraMap, isConjRoot_iff_eq_algebraMap_of_injective, IsConjRoot, eq_comm, RingHom.injective, Iff.trans
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
x : S
inst_5 : IsTorsionFree R S
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsConjRoot R 0 x ↔ x = 0

Tactic:
⟨fun h => eq_zero_of_injective h hf, fun h => h.symm ▸ rfl⟩

Premises used: IsConjRoot.eq_zero_of_injective, Eq.rec, Iff.intro, Eq.symm, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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 : S
⊢ IsConjRoot K 0 x ↔ x = 0

Tactic:
isConjRoot_zero_iff_eq_zero_of_injective (algebraMap K S).injective

Premises used: Algebra.algebraMap, isConjRoot_zero_iff_eq_zero_of_injective, RingHom.injective
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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 : S
⊢ IsConjRoot K x 0 ↔ x = 0

Tactic:
eq_comm.trans <| isConjRoot_zero_iff_eq_zero_of_injective (algebraMap K S).injective

Premises used: Algebra.algebraMap, isConjRoot_zero_iff_eq_zero_of_injective, IsConjRoot, eq_comm, RingHom.injective, Iff.trans
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
x y : S
hx : x ≠ 0
h : IsConjRoot R x y
hf : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ y ≠ 0

Tactic:
fun g => hx (eq_zero_of_injective (g ▸ h.symm) hf)

Premises used: IsConjRoot.eq_zero_of_injective, Not
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
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
hx : x ≠ 0
h : IsConjRoot K x y
⊢ y ≠ 0

Tactic:
ne_zero_of_injective hx h (algebraMap K S).injective

Premises used: Algebra.algebraMap, IsConjRoot.ne_zero_of_injective, RingHom.injective
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
⊢ x ∉ RingHom.range.{u_2, u_3} (R := K) (algebraMap K L) ↔ 2 ≤ natDegree (minpoly K x)

Tactic:
(minpoly.two_le_natDegree_iff h.isIntegral).symm

Premises used: minpoly.two_le_natDegree_iff, Iff.symm, IsSeparable.isIntegral
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
⊢ 2 ≤ natDegree (minpoly K x) ↔ 2 ≤ Fintype.card.{u_3} (↑(rootSet (minpoly K x) L) : Type u_3)

Tactic:
(Polynomial.card_rootSet_eq_natDegree h sp) ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, Polynomial.card_rootSet_eq_natDegree
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
⊢ 2 ≤ Fintype.card.{u_3} (↑(rootSet (minpoly K x) L) : Type u_3) ↔
    Nontrivial.{u_3} (↑(rootSet (minpoly K x) L) : Type u_3)

Tactic:
Fintype.one_lt_card_iff_nontrivial

Premises used: Fintype.one_lt_card_iff_nontrivial, Nat.lt
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
⊢ Nontrivial.{u_3} (↑(rootSet (minpoly K x) L) : Type u_3) ↔
    ∃ (y : (↑(rootSet (minpoly K x) L) : Type u_3)), (↑y : L) ≠ x

Tactic:
(nontrivial_iff_exists_ne ⟨x, mem_rootSet.mpr ⟨minpoly.ne_zero h.isIntegral,
          minpoly.aeval K x⟩⟩).trans ⟨fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mpr hy⟩,
          fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mp hy⟩⟩

Premises used: Iff.mpr, Exists, Ne, minpoly.aeval, nontrivial_iff_exists_ne, Subtype.mk, And.intro, Iff.intro, Exists.intro, Iff.mp, Iff.trans, Polynomial.mem_rootSet, _private.0.notMem_iff_exists_ne_and_isConjRoot.match_2, _private.0.notMem_iff_exists_ne_and_isConjRoot.match_1, Subtype.val, minpoly.ne_zero, Subtype.coe_ne_coe, IsSeparable.isIntegral
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
⊢ (∃ (y : (↑(rootSet (minpoly K x) L) : Type u_3)), (↑y : L) ≠ x) ↔ ∃ (y : L), x ≠ y ∧ IsConjRoot K x y

Tactic:
⟨fun ⟨⟨y, hy⟩, hne⟩ => ⟨y, ⟨hne.symm,
          (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mpr hy⟩⟩,
          fun ⟨y, hne, hy⟩ => ⟨⟨y,
          (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mp hy⟩, hne.symm⟩⟩

Premises used: Iff.intro
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
⊢ x ∉ ⊥ ↔ ∃ (y : L), x ≠ y ∧ IsConjRoot K x y

Tactic:
calc
    _ ↔ 2 ≤ (minpoly K x).natDegree := (minpoly.two_le_natDegree_iff h.isIntegral).symm
    _ ↔ 2 ≤ Fintype.card ((minpoly K x).rootSet L) :=
      (Polynomial.card_rootSet_eq_natDegree h sp) ▸ Iff.rfl
    _ ↔ Nontrivial ((minpoly K x).rootSet L) := Fintype.one_lt_card_iff_nontrivial
    _ ↔ ∃ y : ((minpoly K x).rootSet L), ↑y ≠ x :=
      (nontrivial_iff_exists_ne ⟨x, mem_rootSet.mpr ⟨minpoly.ne_zero h.isIntegral,
          minpoly.aeval K x⟩⟩).trans ⟨fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mpr hy⟩,
          fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mp hy⟩⟩
    _ ↔ _ :=
      ⟨fun ⟨⟨y, hy⟩, hne⟩ => ⟨y, ⟨hne.symm,
          (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mpr hy⟩⟩,
          fun ⟨y, hne, hy⟩ => ⟨⟨y,
          (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mp hy⟩, hne.symm⟩⟩

Premises used: Nontrivial, Polynomial.rootSet, minpoly.two_le_natDegree_iff, Set.Elem, Fintype.card, nontrivial_iff_exists_ne, Fintype.one_lt_card_iff_nontrivial, minpoly, Iff.intro, Iff.trans, Polynomial.natDegree, Iff.symm, IsSeparable.isIntegral
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
rw₄ rw₅ : Eq.{u_1 + 1} (α := S) 0 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)

Tactic:
rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]

Premises used: Polynomial.mul_divByMonic_eq_iff_isRoot, Polynomial.IsRoot, minpoly.aeval, mul_comm, Polynomial.eval_map_algebraMap
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
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
⊢ 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)

Tactic:
rw [← coeff_map, ← minpolyDiv_spec R x]

Premises used: Polynomial.coeff_map, minpolyDiv_spec
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 =
    (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:
simp [mul_sub]

Premises used: mul_sub
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := S[X]) 0 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

Tactic:
rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]

Premises used: Polynomial.zero_divByMonic, dif_neg, Polynomial.map_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
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])))
⊢ eval x (minpolyDiv R x) = (aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X])

Tactic:
rw [← eval_map_algebraMap, ← derivative_map, ← minpolyDiv_spec R x]

Premises used: minpolyDiv_spec, Polynomial.eval_map_algebraMap, Polynomial.derivative_map
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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) =
    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:
simp
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 * 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

Premises used: minpolyDiv_spec, Polynomial.eval_map_algebraMap
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 ∨ y - x = 0

Tactic:
simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_mul, mul_eq_zero, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
rwa rwa₁ rwa₂ rwa₃ : ¬y = x
⊢ ¬y - x = 0

Tactic:
rwa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
⊢ eval y (minpolyDiv R x) = 0

Tactic:
exact hy.resolve_right (by rwa [sub_eq_zero])

Premises used: Or.resolve_right
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
neg : ∀ (h : ¬(σ : (a : S) → T) x = y), eval₂ σ y (minpolyDiv 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

Tactic:
split_ifs with h
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
pos₂ 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)
⊢ 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:
rw [← h, eval₂_hom, eval_minpolyDiv_self]

Premises used: eval_minpolyDiv_self, Polynomial.eval₂_hom
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) = 0

Tactic:
rw [← eval₂_map, ← minpolyDiv_spec] at hy

Premises used: Polynomial.eval₂_map, minpolyDiv_spec
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
hy₁ : eval₂ σ y (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) = 0
⊢ ¬(σ : (a : S) → T) x = y

Tactic:
rw [← eval₂_map, ← minpolyDiv_spec] at hy

Premises used: Polynomial.eval₂_map, minpolyDiv_spec
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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₂ σ y (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) = 0
h : ¬(σ : (a : S) → T) x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0

Tactic:
simpa [sub_eq_zero, Ne.symm h] using hy

Premises used: sub_eq_zero, Ne.symm
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
⊢ 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

Tactic:
apply eval₂_minpolyDiv_of_eval₂_eq_zero

Premises used: eval₂_minpolyDiv_of_eval₂_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
hy₅ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) ((aeval x : (a : R[X]) → S) (minpoly R x) : S) : T) (0 : T)
hy₆ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) 0 : T) (0 : T)
hy₇ hy₈ : Eq.{u_1 + 1} (α := T) 0 0
⊢ 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]

Premises used: AlgHom.comp_algebraMap, Polynomial.eval₂_hom, RingHom.coe_coe, map_zero, Polynomial.eval₂_map, minpoly.aeval, Polynomial.eval_map_algebraMap