-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
theorem Polynomial.Separable.map_irreducible_of_isPurelyInseparable {f : F[X]} (hsep : f.Separable)
    (hirr : Irreducible f) [IsPurelyInseparable F E] : Irreducible (f.map (algebraMap F E))

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero K f
  (natDegree_pos_iff_degree_pos.1 hirr.natDegree_pos).ne'

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
have ha : Associated f (minpoly F x) := by
  have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv
  exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
rw [ha'.irreducible_iff, heq]

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
⊢ Irreducible (minpoly E x)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ Associated f (minpoly F x)

Tactic:
exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩

Result:
no goals

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
have heq := minpoly.map_eq_of_isSeparable_of_isPurelyInseparable E x (ha.separable hsep)

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
⊢ Irreducible (minpoly E x)

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

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ f * ↑this.unit = minpoly F x

Tactic:
rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
⊢ Associated f (minpoly F x)

Tactic:
have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ Associated f (minpoly F x)

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
have ha' : Associated (f.map (algebraMap F E)) ((minpoly F x).map (algebraMap F E)) :=
  ha.map (mapRingHom (algebraMap F E)).toMonoidHom

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
let K := AlgebraicClosure E

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
⊢ Irreducible (Polynomial.map (algebraMap F E) f)