-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable,
then $[K:F]_s = [K:E]_s$.
It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it. -/
lemma sepDegree_eq_of_isPurelyInseparable [IsPurelyInseparable F E] :
    sepDegree F K = sepDegree E K

Proof state:
case h.e'_2
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)

Tactic:
haveI : IsScalarTower F (separableClosure E K) K := IsScalarTower.of_algebraMap_eq (congrFun rfl)

Result:
case h.e'_2
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)

Proof state:
case h.e'_2
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)

Tactic:
rw [sepDegree, ← separableClosure.map_eq_of_separableClosure_eq_bot F
  (separableClosure.separableClosure_eq_bot E K)]

Result:
case h.e'_2
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ Module.rank F
      ↥(IntermediateField.map (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K)
          (separableClosure F ↥(separableClosure E K))) =
    sepDegree F ↥(separableClosure E K)

Proof state:
case h.e'_2
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ Module.rank F
      ↥(IntermediateField.map (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K)
          (separableClosure F ↥(separableClosure E K))) =
    sepDegree F ↥(separableClosure E K)

Tactic:
exact (separableClosure F (separableClosure E K)).equivMap
  (IsScalarTower.toAlgHom F (separableClosure E K) K) |>.symm.toLinearEquiv.rank_eq

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
⊢ sepDegree F K = sepDegree E K

Tactic:
convert sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K)

Result:
case h.e'_2
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)