awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
h :
  Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
⊢ Eq.{u_6 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)

Tactic:
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]

Premises used: map_zero, minpoly.aeval, Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
h :
  Eq (α := R →+* L) (algebraMap R L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
h₁ h₂ : Eq (α := R →+* L) (algebraMap R L) (algebraMap R L)
⊢ Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))

Tactic:
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
R : Type u_3
K : Type u_4
T : Type u_5
U : Type u_6
inst : CommRing R
inst_1 : Field K
inst_2 : CommRing T
inst_3 : Algebra R K
inst_4 : Algebra K T
inst_5 : Algebra R T
inst_6 : IsScalarTower R K T
inst_7 : CommSemiring U
inst_8 : Algebra K U
inst_9 : Algebra R U
inst_10 : IsScalarTower R K U
x : T
y : U
hy : Eq.{u_6 + 1} (α := U) ((Polynomial.aeval y : (a : K[X]) → U) (minpoly K x) : U) (0 : U)
⊢ Eq.{u_6 + 1} (α := U) ((Polynomial.aeval y : (a : R[X]) → U) (minpoly R x) : U) (0 : U)

Tactic:
aeval_map_algebraMap K y (minpoly R x) ▸
    eval₂_eq_zero_of_dvd_of_eval₂_eq_zero (algebraMap K U) y
      (minpoly.dvd_map_of_isScalarTower R K x) hy

Premises used: Polynomial.aeval_map_algebraMap, Algebra.algebraMap, Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero, Eq.rec, minpoly, minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : E[X]) → A) (map (algebraMap F E) (minpoly F a)) : A) (0 : A)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
refine : natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)
⊢ Eq (α := E[X]) (map (algebraMap F E) (minpoly F a)) (minpoly E a)

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
    ((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha)
    (minpoly.dvd E a (by simp)) ?_

Premises used: minpoly.monic, Algebra.algebraMap, Function.Injective.monic_map_iff, RingHom.injective, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, Iff.mp, minpoly.dvd, IsIntegral.tower_top
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
obtain :
  ∀ (g : F[X]) (hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a))
    (hgdeg : g.natDegree = natDegree (minpoly E a)) (hgmon : g.Monic),
    natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)
⊢ natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)

Tactic:
obtain ⟨g, hg, hgdeg, hgmon⟩ := lifts_and_natDegree_eq_and_monic h (minpoly.monic ha.tower_top)

Premises used: minpoly.monic, IsIntegral.tower_top, Polynomial.lifts_and_natDegree_eq_and_monic
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : natDegree (minpoly F a) ≤ g.natDegree
⊢ natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)

Tactic:
rw [natDegree_map, ← hgdeg]

Premises used: Polynomial.natDegree_map
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
⊢ natDegree (minpoly F a) ≤ g.natDegree

Tactic:
natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero

Premises used: Polynomial.natDegree_le_of_dvd, minpoly.dvd, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
refine : Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
⊢ natDegree (minpoly F a) ≤ g.natDegree

Tactic:
refine natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero

Premises used: Polynomial.natDegree_le_of_dvd, minpoly.dvd, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
rw₁ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) g) :
      A)
    (0 : A)
rw₂ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((mapRingHom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
rw₃ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((RingHom.comp (β := E[X]) (mapRingHom (algebraMap E A)) (mapRingHom (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
rw₄ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((mapRingHom (algebraMap E A) : RingHom.{u_4, u_5} E[X] A[X]) : (a : E[X]) → A[X])
            (((mapRingHom (algebraMap F E) : RingHom.{u_3, u_4} F[X] E[X]) : (a : F[X]) → E[X]) g) :
          A[X]) :
      A)
    (0 : A)
rw₅ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (map (algebraMap E A) (((mapRingHom (algebraMap F E) : RingHom.{u_3, u_4} F[X] E[X]) : (a : F[X]) → E[X]) g)) :
      A)
    (0 : A)
rw₆ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (map (algebraMap F E) g)) : A) (0 : A)
rw₇ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (minpoly E a)) : A) (0 : A)
rw₈ : Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : E[X]) → A) (minpoly E a) : A) (0 : A)
rw₉ rw₁₀ : Eq.{u_5 + 1} (α := A) 0 0
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)

Tactic:
rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]

Premises used: Polynomial.aeval_map_algebraMap, minpoly.aeval, Polynomial.coe_mapRingHom, IsScalarTower.algebraMap_eq, RingHom.comp_apply, Polynomial.mapRingHom_comp
-- 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 : B
h :
  ∀ (p : A[X]),
    Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
      Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
⊢ Eq (α := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) (A[X] ∙ minpoly A x)

Tactic:
ext p
-- 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 : B
p : A[X]
h :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₁ : minpoly A x ∣ p ↔ Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₂ : minpoly A x ∣ p ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
h₃ : (∃ (c : A[X]), p = c * minpoly A x) ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
h₄ : (∃ (c : A[X]), p = c * minpoly A x) ↔ ∃ (a : A[X]), a * minpoly A x = p
⊢ Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p

Tactic:
simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]

Premises used: RingHom.mem_ker, Submodule.mem_span_singleton, minpoly.dvd_iff, eq_comm, smul_eq_mul, dvd_iff_exists_eq_mul_left
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp3 : p.Monic
⊢ p = minpoly A x

Tactic:
let ⟨_, hq⟩ := dvd A x hp2
  eq_of_monic_of_associated hp3 (monic ⟨p, ⟨hp3, hp2⟩⟩) <|
    mul_one (minpoly A x) ▸ hq.symm ▸ Associated.mul_left _
      (associated_one_iff_isUnit.2 <| (hp1.isUnit_or_isUnit hq).resolve_left <| not_isUnit A x)

Premises used: Iff.mpr, minpoly.monic, associated_one_iff_isUnit, Eq.rec, _private.0.minpoly.dvd_iff.match_1, Or.resolve_left, minpoly, Irreducible.isUnit_or_isUnit, And.intro, Exists.intro, minpoly.not_isUnit, Associated.mul_left, minpoly.dvd, mul_one, Eq.symm, Polynomial.eq_of_monic_of_associated, Eq
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
irr : Irreducible p
monic : p.Monic
⊢ p = minpoly A x ↔ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)

Tactic:
⟨(· ▸ aeval A x), (eq_of_irreducible_of_monic irr · monic)⟩

Premises used: Eq.rec, minpoly.eq_of_irreducible_of_monic, minpoly.aeval, Iff.intro, Eq.symm
-- 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
inst_3 : IsDomain B
C : Type u_3
inst_4 : Ring C
inst_5 : Algebra A C
inst_6 : Nontrivial C
b : B
h : IsIntegral A b
c : C
⊢ Eq (α := A[X]) (minpoly A b) (minpoly A c) ↔
    Eq.{u_3 + 1} (α := C) ((Polynomial.aeval c : (a : A[X]) → C) (minpoly A b) : C) (0 : C)

Tactic:
eq_iff_aeval_eq_zero (irreducible h) (monic h)

Premises used: minpoly.monic, minpoly.eq_iff_aeval_eq_zero, minpoly.irreducible
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ p.leadingCoeff ≠ 0

Tactic:
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp1₁ : Irreducible (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
hp2₁ :
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)
hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic
⊢ HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) = minpoly A x

Tactic:
apply eq_of_irreducible_of_monic

Premises used: minpoly.eq_of_irreducible_of_monic
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X]) (1 : A[X])
rwa₁ : Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1
rwa₂ : p.leadingCoeff ≠ 0
rwa₃ : Eq.{u_1 + 1} (α := A[X]) 1 1
rwa₄ : p.leadingCoeff ≠ 0
rwa₅ : Eq.{u_1 + 1} (α := A[X]) 1 1
rwa₆ rwa₇ rwa₈ : p.leadingCoeff ≠ 0
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) =
    1

Tactic:
rwa [← C_mul, inv_mul_cancel₀, C_1]

Premises used: Polynomial.C_1, Polynomial.C_mul, inv_mul_cancel₀
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff * p.leadingCoeff⁻¹) : A[X]) (1 : A[X])
rwa₁ : Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1
rwa₂ : p.leadingCoeff ≠ 0
rwa₃ : Eq.{u_1 + 1} (α := A[X]) 1 1
rwa₄ : p.leadingCoeff ≠ 0
rwa₅ : Eq.{u_1 + 1} (α := A[X]) 1 1
rwa₆ rwa₇ rwa₈ : p.leadingCoeff ≠ 0
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) =
    1

Tactic:
rwa [← C_mul, mul_inv_cancel₀, C_1]

Premises used: Polynomial.C_1, mul_inv_cancel₀, Polynomial.C_mul
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
⊢ Irreducible (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))

Tactic:
exact Associated.irreducible ⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff,
      by rwa [← C_mul, inv_mul_cancel₀, C_1], by rwa [← C_mul, mul_inv_cancel₀, C_1]⟩, rfl⟩ hp1

Premises used: Polynomial.C, Associated.irreducible, Polynomial.leadingCoeff, Inv.inv, Units.mk, Exists.intro, DFunLike.coe, rfl
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp2₁ :
  HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B)
      ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
    0
hp2₂ :
  HMul.hMul (α := B) (β := B) (0 : B)
      ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
    0
hp2₃ hp2₄ : Eq.{u_2 + 1} (α := B) 0 0
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)

Tactic:
rw [aeval_mul, hp2, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.aeval_mul
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).leadingCoeff = 1
hp3₁ : p.leadingCoeff * leadingCoeff ((C : (a : A) → A[X]) p.leadingCoeff⁻¹) = 1
hp3₂ : p.leadingCoeff * p.leadingCoeff⁻¹ = 1
hp3₃ : Eq.{u_1 + 1} (α := A) 1 1
hp3₄ : p.leadingCoeff ≠ 0
hp3₅ : Eq.{u_1 + 1} (α := A) 1 1
hp3₆ hp3₇ hp3₈ : p.leadingCoeff ≠ 0
⊢ (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic

Tactic:
rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]

Premises used: mul_inv_cancel₀, Polynomial.leadingCoeff_mul, Polynomial.Monic, Polynomial.leadingCoeff_C
-- 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 : B
inst_3 : Nontrivial B
p : A[X]
hi : Irreducible p
hx : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
rw :
  p =
    HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
rw₁ :
  p =
    HMul.hMul (β := A[X]) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₂ :
  p =
    p *
      HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
        ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
rw₃ : p = HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X])
rw₄ : p = p * (C : (a : A) → A[X]) 1
rw₅ : p = p * 1
rw₆ rw₇ : p = p
⊢ p = HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) (minpoly A x)

Tactic:
rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
    inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]

Premises used: Iff.mpr, Polynomial.C_1, minpoly.eq_of_irreducible, mul_assoc, Polynomial.leadingCoeff_ne_zero, Polynomial.C_mul, mul_comm, Irreducible.ne_zero, mul_one, inv_mul_cancel₀
-- 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
pos :
  ∀ (hx : IsIntegral A x),
    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]))
neg :
  ∀ (hx : ¬IsIntegral A x),
    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]))
⊢ 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:
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 : CommRing B
inst_2 : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ 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:
(minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm

Premises used: minpoly.unique, minpoly.monic, Polynomial.Monic.comp_X_sub_C, Eq.symm
-- 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
pos :
  Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B)
        (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))) :
      B)
    (0 : B)
pos₁ :
  ∀ (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)),
    (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X]))).degree ≤
      q.degree
⊢ 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:
refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm

Premises used: minpoly.unique, minpoly.monic, Polynomial.Monic.comp_X_sub_C, Eq.symm
-- 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
⊢ Eq.{u_3 + 1} (α := B)
    ((Polynomial.aeval (HAdd.hAdd (β := B) x ((algebraMap A B : (a : A) → B) a : B)) : (a : A[X]) → B)
        (Polynomial.comp (minpoly A x) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[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 : 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)
⊢ 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)

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 : 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)
⊢ 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)

Tactic:
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq