awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
⊢ degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree

Tactic:
have H := minpoly.min A x (qmo.comp_X_add_C _) this
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
pos : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree ≤
    q.degree

Tactic:
rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
        natDegree_X_sub_C, mul_one]

Premises used: minpoly.monic, Polynomial.degree_eq_natDegree, Polynomial.Monic.comp_X_sub_C, Polynomial.natDegree_comp, Polynomial.natDegree_X_sub_C, mul_one, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
H : degree (minpoly A x) ≤ (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree
pos :
  ∀
    (H :
      (↑(natDegree (minpoly A x)) : WithBot ℕ) ≤
        (q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₁ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.comp (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).natDegree : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₂ :
  ∀
    (H :
      LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ)
        (↑(q.natDegree * (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).natDegree) : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₃ :
  ∀ (H : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑(q.natDegree * 1) : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
pos₄ pos₅ pos₆ pos₇ :
  ∀ (H : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)),
    LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly A x)) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)

Tactic:
rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_comp, Polynomial.natDegree_X_add_C, Polynomial.Monic.comp_X_add_C, mul_one, minpoly.ne_zero, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
neg : ¬IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))
⊢ minpoly A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))

Tactic:
rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]

Premises used: Polynomial.zero_comp, minpoly.eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))

Tactic:
fun h ↦ hx ?_

Premises used: Not
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
neg : ∀ (h : IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))), IsIntegral A x
⊢ ¬IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))

Tactic:
refine fun h ↦ hx ?_
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
h : IsIntegral A (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B))
⊢ IsIntegral A x

Tactic:
simpa only [add_sub_cancel_right] using IsIntegral.sub h (isIntegral_algebraMap (x := a))

Premises used: IsIntegral.sub, isIntegral_algebraMap, add_sub_cancel_right
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : CommRing B
inst_2 : Algebra A B
x : B
a : A
⊢ minpoly A (HSub.hSub (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    Polynomial.comp (minpoly A x) (HAdd.hAdd (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))

Tactic:
simpa [sub_eq_add_neg] using add_algebraMap x (-a)

Premises used: sub_eq_add_neg, minpoly.add_algebraMap, Neg.neg
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
pos :
  ∀ (hx : IsIntegral A x),
    minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
neg₁ :
  ∀ (hx : ¬IsIntegral A x),
    minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)

Tactic:
by_cases hx : IsIntegral A x

Premises used: IsIntegral
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)

Tactic:
(minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
        ?_ fun q qmo hq => ?_).symm

Premises used: minpoly.unique, minpoly.monic, Eq.symm, Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
pos :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (-x) : (a : A[X]) → B)
        (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)) :
      B)
    (0 : B)
pos₁ :
  ∀ (q : A[X]) (qmo : q.Monic) (hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)),
    (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)).degree ≤ q.degree
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)

Tactic:
refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
        ?_ fun q qmo hq => ?_).symm

Premises used: minpoly.unique, minpoly.monic, Eq.symm, Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (-x) : (a : A[X]) → B)
        (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)) :
      B)
    (0 : B)

Tactic:
simp [aeval_comp]

Premises used: Polynomial.aeval_comp
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)
⊢ Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)) : B) (0 : B)

Tactic:
simpa [aeval_comp] using hq

Premises used: Polynomial.aeval_comp
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)
⊢ Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)) : B) (0 : B)

Tactic:
have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0 := by
        simpa [aeval_comp] using hq
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)) : B) (0 : B)
⊢ degree (minpoly A x) ≤ (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)).degree

Tactic:
have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X this
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : Eq.{u_3 + 1} (α := B) ((Polynomial.aeval (-x) : (a : A[X]) → B) q : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)) : B) (0 : B)
H : degree (minpoly A x) ≤ (HPow.hPow (α := A[X]) (-1) q.natDegree * q.comp (-X)).degree
⊢ (HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)).degree ≤ q.degree

Tactic:
simp_all
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
neg₁ : 0 = HPow.hPow (α := A[X]) (-1) (natDegree.{u_1} (R := A) 0) * 0
neg₂ : ¬IsIntegral A (-x)
⊢ minpoly A (-x) = HPow.hPow (α := A[X]) (-1) (natDegree (minpoly A x)) * Polynomial.comp (minpoly A x) (-X)

Tactic:
rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]

Premises used: Polynomial.zero_comp, minpoly.eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ 0 = HPow.hPow (α := A[X]) (-1) (natDegree.{u_1} (R := A) 0) * 0

Tactic:
simp only [natDegree_zero, pow_zero, mul_zero]

Premises used: Polynomial.natDegree_zero, pow_zero, MulZeroClass.mul_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (-x)

Tactic:
IsIntegral.neg_iff.not.mpr hx

Premises used: Iff.mpr, Iff.not, IsIntegral.neg_iff
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
B : Type u_3
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (-x)

Tactic:
exact IsIntegral.neg_iff.not.mpr hx

Premises used: Iff.mpr, Iff.not, IsIntegral.neg_iff
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Eq (α := A[X]) (map (↑f : R →+* A) (minpoly R x)) (minpoly.{u_1, u_5} A (B := T) ((g : (a : S) → T) x : T))

Tactic:
minpoly.eq_of_irreducible_of_monic ?_ ?_ ?_

Premises used: minpoly.eq_of_irreducible_of_monic
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
refine_1 : Irreducible (M := A[X]) (map (↑f : R →+* A) (minpoly R x))
refine_2 :
  Eq.{u_5 + 1} (α := T)
    (((Polynomial.aeval ((g : (a : S) → T) x) : A[X] →ₐ[A] T) : (a : A[X]) → T) (map (↑f : R →+* A) (minpoly R x)) : T)
    (0 : T)
refine_3 : Monic (map (↑f : R →+* A) (minpoly R x))
⊢ Eq (α := A[X]) (map (↑f : R →+* A) (minpoly R x)) (minpoly.{u_1, u_5} A (B := T) ((g : (a : S) → T) x : T))

Tactic:
refine minpoly.eq_of_irreducible_of_monic ?_ ?_ ?_

Premises used: minpoly.eq_of_irreducible_of_monic
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
refine_1 : Irreducible (M := R[X]) (minpoly R x)
⊢ Irreducible (M := A[X]) (map (↑f : R →+* A) (minpoly R x))

Tactic:
rw [← mapEquiv_apply, MulEquiv.irreducible_iff]

Premises used: MulEquiv.irreducible_iff, Polynomial.mapEquiv_apply
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Irreducible (M := R[X]) (minpoly R x)

Tactic:
minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.irreducible
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Irreducible (M := R[X]) (minpoly R x)

Tactic:
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.irreducible
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Eq.{u_5 + 1} (α := T)
    (((Polynomial.aeval ((g : (a : S) → T) x) : A[X] →ₐ[A] T) : (a : A[X]) → T) (map (↑f : R →+* A) (minpoly R x)) : T)
    (0 : T)

Tactic:
simpa using (map_aeval_eq_aeval_map hcomp (minpoly R x) x).symm

Premises used: minpoly, Eq.symm, Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Monic (map (↑f : R →+* A) (minpoly R x))

Tactic:
(monic (Algebra.IsIntegral.isIntegral x)).map _

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, Polynomial.Monic.map
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
inst : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Ring S
inst_4 : Ring T
inst_5 : IsDomain S
inst_6 : IsDomain T
inst_7 : Algebra R S
inst_8 : Algebra A T
inst_9 : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp :
  Eq (α := R →+* T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A T) (↑f : R →+* A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T) (algebraMap R S))
x : S
⊢ Monic (map (↑f : R →+* A) (minpoly R x))

Tactic:
exact (monic (Algebra.IsIntegral.isIntegral x)).map _

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, Polynomial.Monic.map
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x_1 : B
F : Type u_3
E : Type u_4
K : Type u_5
inst_3 : Field F
inst_4 : Ring E
inst_5 : CommRing K
inst_6 : IsDomain K
inst_7 : Algebra F E
inst_8 : Algebra F K
inst_9 : FiniteDimensional F E
φ : E →ₐ[F] K
x : (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) : Type u_4)
rw : eval₂ (algebraMap F K) ((φ : (a : E) → K) (↑x : E)) (minpoly F (↑x : E)) = 0
rw₁ :
  Eq.{u_5 + 1} (α := K)
    (((Polynomial.aeval ((φ : (a : E) → K) (↑x : E)) : F[X] →ₐ[F] K) : (a : F[X]) → K) (minpoly F (↑x : E)) : K) (0 : K)
rw₂ :
  Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) ((Polynomial.aeval (↑x : E) : (a : F[X]) → E) (minpoly F (↑x : E)) : E) : K)
    (0 : K)
rw₃ : Eq.{u_5 + 1} (α := K) ((φ : (a : E) → K) 0 : K) (0 : K)
rw₄ rw₅ : Eq.{u_5 + 1} (α := K) 0 0
⊢ Membership.mem (α := K) (aroots (minpoly F (↑x : E)) K) ((φ : (a : E) → K) (↑x : E) : K)

Tactic:
rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]

Premises used: map_zero, minpoly.ne_zero_of_finite, minpoly.aeval, Polynomial.aeval_def, Polynomial.mem_roots_map, Polynomial.aeval_algHom_apply, Subtype.val
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Ring E
inst_2 : CommRing K
inst_3 : IsDomain K
inst_4 : Algebra F E
inst_5 : Algebra F K
inst_6 : FiniteDimensional F E
f g : E →ₐ[F] K
h :
  Eq (α :=
    (x :
        (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
          Type u_4)) →
      { l : K // l ∈ aroots (minpoly F (↑x : E)) K })
    (rootsOfMinPolyPiType F E K f) (rootsOfMinPolyPiType F E K g)
this :
  Eq (α := E →ₗ[F] K)
    (↑f : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)
    (↑g : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Eq (α := (a : E) → K)
        (⇑(↑f : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K) :
          (a : E) → K)
        (⇑(↑g : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K) :
          (a : E) → K)),
    Eq (α := (a : E) → K) (⇑f : (a : E) → K) (⇑g : (a : E) → K)
⊢ f = g

Tactic:
rwa [DFunLike.ext'_iff] at this ⊢

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Ring E
inst_2 : CommRing K
inst_3 : IsDomain K
inst_4 : Algebra F E
inst_5 : Algebra F K
inst_6 : FiniteDimensional F E
f g : E →ₐ[F] K
h :
  Eq (α :=
    (x :
        (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
          Type u_4)) →
      { l : K // l ∈ aroots (minpoly F (↑x : E)) K })
    (rootsOfMinPolyPiType F E K f) (rootsOfMinPolyPiType F E K g)
suffices :
  Eq (α := E →ₗ[F] K)
    (↑f : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)
    (↑g : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)
⊢ f = g

Tactic:
suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Ring E
inst_2 : CommRing K
inst_3 : IsDomain K
inst_4 : Algebra F E
inst_5 : Algebra F K
inst_6 : FiniteDimensional F E
f g : E →ₐ[F] K
h :
  Eq (α :=
    (x :
        (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
          Type u_4)) →
      { l : K // l ∈ aroots (minpoly F (↑x : E)) K })
    (rootsOfMinPolyPiType F E K f) (rootsOfMinPolyPiType F E K g)
⊢ ∀
    (x :
      (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
        Type u_4)),
    Eq (α := { l : K // l ∈ aroots (minpoly F (↑x : E)) K }) (rootsOfMinPolyPiType F E K f x)
      (rootsOfMinPolyPiType F E K g x)

Tactic:
rw [funext_iff] at h

Premises used: funext_iff
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Ring E
inst_2 : CommRing K
inst_3 : IsDomain K
inst_4 : Algebra F E
inst_5 : Algebra F K
inst_6 : FiniteDimensional F E
f g : E →ₐ[F] K
h :
  ∀
    (x :
      (↑(range (ι := Fin (Module.finrank F E)) (⇑(Module.finBasis F E) : (a : Fin (Module.finrank F E)) → E)) :
        Type u_4)),
    Eq (α := { l : K // l ∈ aroots (minpoly F (↑x : E)) K }) (rootsOfMinPolyPiType F E K f x)
      (rootsOfMinPolyPiType F E K g x)
⊢ Eq (α := E →ₗ[F] K)
    (↑f : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)
    (↑g : [inst_7 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K)

Tactic:
LinearMap.ext_on (Module.finBasis F E).span_eq fun e he =>
    Subtype.ext_iff.mp (h ⟨e, he⟩)

Premises used: LinearMap.ext_on, Module.finBasis, Subtype.ext_iff, Subtype.mk, Iff.mp, Module.Basis.span_eq