-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) :
    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
⊢ IsGalois F E

Tactic:
suffices P (IntermediateField.adjoin F s) by
  rw [adjoin_root] at this
  apply of_card_aut_eq_finrank
  rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
  exact Fintype.card_congr ((algEquivEquivAlgHom F E).toEquiv.trans
    (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))

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
⊢ P (adjoin F s)

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) = finrank F ↥⊥.toSubalgebra
⊢ Fintype.card (↥⊥ →ₐ[F] E) = Fintype.card (↥F⟮0⟯ →ₐ[F] E)

Tactic:
apply @Fintype.card_congr _ _ _ (_) _

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
key : Fintype.card (↥F⟮0⟯ →ₐ[F] E) = finrank F ↥⊥.toSubalgebra
⊢ (↥⊥ →ₐ[F] E) ≃ (↥F⟮0⟯ →ₐ[F] E)

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
⊢ P ⊥

Tactic:
have key := IntermediateField.card_algHom_adjoin_integral F (K := E)
  (show IsIntegral F (0 : E) from isIntegral_zero)

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 :
  IsSeparable F 0 →
    Polynomial.Splits (algebraMap F E) (minpoly F 0) → Fintype.card (↥F⟮0⟯ →ₐ[F] E) = (minpoly F 0).natDegree
⊢ P ⊥

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
⊢ ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) ≃ₗ[F] ↥(↥K)⟮x⟯

Tactic:
rfl

Result:
no goals

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 ∈ (p.aroots E).toFinset, P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)

Tactic:
intro K x hx hK

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 : P K
⊢ P (IntermediateField.restrictScalars F (↥K)⟮x⟯)

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 ⊤
⊢ IsGalois F E

Tactic:
apply of_card_aut_eq_finrank

Result:
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) = finrank 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
⊢ IsGalois F E

Tactic:
have adjoin_root : IntermediateField.adjoin F s = ⊤ := by
  apply IntermediateField.toSubalgebra_injective
  rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
  apply IntermediateField.algebra_adjoin_le_adjoin

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 = ⊤
⊢ IsGalois F E

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) = finrank F ↥⊥.toSubalgebra
⊢ P ⊥

Tactic:
refine Eq.trans ?_ 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
⊢ Fintype.card (↥⊥ →ₐ[F] E) = Fintype.card (↥F⟮0⟯ →ₐ[F] E)