-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem prime_degree_dvd_card [CharZero F] (p_irr : Irreducible p) (p_deg : p.natDegree.Prime) :
    p.natDegree ∣ Fintype.card p.Gal

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
⊢ (minpoly F α).natDegree = p.natDegree

Tactic:
have key := (minpoly.irreducible hα).dvd_symm p_irr this

Result:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ (minpoly F α).natDegree = p.natDegree

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
have hα : IsIntegral F α := .of_finite F α

Result:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ p.natDegree ∣ finrank F p.SplittingField

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ minpoly F α ∣ p

Tactic:
apply minpoly.dvd F α

Result:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ (aeval α) p = 0

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ Fintype.card p.Gal

Tactic:
rw [Gal.card_of_separable p_irr.separable]

Result:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ finrank F p.SplittingField

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField

Tactic:
suffices (minpoly F α).natDegree = p.natDegree by
  letI _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
  rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
    IntermediateField.adjoin.finrank hα, this]

Result:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ (minpoly F α).natDegree = p.natDegree

Proof state:
case a
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ (minpoly F α).natDegree ≤ p.natDegree

Tactic:
exact natDegree_le_of_dvd this p_irr.ne_zero

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ (minpoly F α).natDegree = p.natDegree

Tactic:
apply le_antisymm

Result:
case a
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ (minpoly F α).natDegree ≤ p.natDegree

case a
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ (minpoly F α).natDegree

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ (aeval α) p = 0

Tactic:
rw [aeval_def, map_rootOfSplits _ (SplittingField.splits p) hp]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
have hp : p.degree ≠ 0 := fun h =>
  Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))

Result:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
⊢ p.natDegree ∣ finrank F p.SplittingField

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
use Module.finrank F⟮α⟯ p.SplittingField

Result:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : (minpoly F α).natDegree = p.natDegree
x✝ : AddCommGroup ↥F⟮α⟯ := Ring.toAddCommGroup
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField

Tactic:
rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
  IntermediateField.adjoin.finrank hα, this]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
let α : p.SplittingField :=
  rootOfSplits (algebraMap F p.SplittingField) (SplittingField.splits p) hp

Result:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
⊢ p.natDegree ∣ finrank F p.SplittingField

Proof state:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : (minpoly F α).natDegree = p.natDegree
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField

Tactic:
letI _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup

Result:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : (minpoly F α).natDegree = p.natDegree
x✝ : AddCommGroup ↥F⟮α⟯ := Ring.toAddCommGroup
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField