-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) :
    IsGalois F E

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
⊢ (adjoin F s).toSubalgebra = ⊤.toSubalgebra

Tactic:
rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
⊢ Algebra.adjoin F (p.rootSet E) ≤ (adjoin F s).toSubalgebra

Proof state:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
key :
  IsSeparable F 0 →
    Polynomial.Splits (algebraMap F E) (minpoly F 0) → Fintype.card (↥F⟮0⟯ →ₐ[F] E) = (minpoly F 0).natDegree
⊢ P ⊥

Tactic:
rw [IsSeparable, minpoly.zero, Polynomial.natDegree_X] at key

Result:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
key : Polynomial.X.Separable → Polynomial.Splits (algebraMap F E) Polynomial.X → Fintype.card (↥F⟮0⟯ →ₐ[F] E) = 1
⊢ P ⊥

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
⊢ IsGalois F E

Tactic:
haveI hFE : FiniteDimensional F E := Polynomial.IsSplittingField.finiteDimensional E p

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
⊢ IsGalois F E

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
key : Fintype.card (↥F⟮0⟯ →ₐ[F] E) = finrank F ↥⊥.toSubalgebra
⊢ (↥⊥ →ₐ[F] E) ≃ (↥F⟮0⟯ →ₐ[F] E)

Tactic:
rw [IntermediateField.adjoin_zero]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
⊢ IsGalois F E

Tactic:
let s := p.rootSet E

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
⊢ IsGalois F E

Proof state:
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
⊢ Fintype.card (↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) →ₐ[F] E) =
    finrank F ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯)

Tactic:
rw [of_separable_splitting_field_aux hp K (Multiset.mem_toFinset.mp hx), hK, finrank_mul_finrank]

Result:
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
⊢ finrank F ↥(↥K)⟮x⟯ = finrank F ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯)

Proof state:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
this : P ⊤
⊢ Fintype.card (E ≃ₐ[F] E) = Fintype.card (↥⊤ →ₐ[F] E)

Tactic:
exact Fintype.card_congr ((algEquivEquivAlgHom F E).toEquiv.trans
  (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))

Result:
no goals

Proof state:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
key : Fintype.card (↥F⟮0⟯ →ₐ[F] E) = 1
⊢ P ⊥

Tactic:
rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key

Result:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
key : Fintype.card (↥F⟮0⟯ →ₐ[F] E) = finrank F ↥⊥.toSubalgebra
⊢ P ⊥

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
⊢ IsGalois F E

Tactic:
letI := Classical.decEq E

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
⊢ IsGalois F E

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
this : P (adjoin F s)
⊢ IsGalois F E

Tactic:
rw [adjoin_root] at this

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
this : P ⊤
⊢ IsGalois F E