-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_separable_splitting_field_aux [hFE : FiniteDimensional F E] [sp : p.IsSplittingField F E]
    (hp : p.Separable) (K : Type*) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E]
    {x : E} (hx : x ∈ p.aroots E)
    -- these are both implied by `hFE`, but as they carry data this makes the lemma more general
    [Fintype (K →ₐ[F] E)]
    [Fintype (K⟮x⟯.restrictScalars F →ₐ[F] E)] :
    Fintype.card (K⟮x⟯.restrictScalars F →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K K⟮x⟯

Proof state:
case h₁.h_splits
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.Splits (algebraMap K E) (minpoly K x)

Tactic:
refine Polynomial.splits_of_splits_of_dvd _ (Polynomial.map_ne_zero h1) ?_ h2

Result:
case h₁.h_splits
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.Splits (algebraMap K E) (Polynomial.map (algebraMap F K) p)

Proof state:
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)
⊢ ∑ i : K →ₐ[F] E, Fintype.card (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * (minpoly K x).natDegree

Tactic:
apply Finset.sum_const_nat

Result:
case h₁
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)
⊢ ∀ x_1 ∈ Finset.univ, Fintype.card (↥K⟮x⟯ →ₐ[K] E) = (minpoly K x).natDegree

Proof state:
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ (↥K⟮x⟯ →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)

Tactic:
exact algHomEquivSigma

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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp✝ : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ 0
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
hp : p = 0
⊢ False

Tactic:
exact Multiset.not_mem_zero x hx

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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
⊢ Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯

Tactic:
haveI : ∀ f : K →ₐ[F] E, Fintype (@AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f)) := fun f => by
  have := Fintype.ofEquiv _ key_equiv
  apply Fintype.ofInjective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2

Result:
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)
⊢ Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯