-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable and `K / E`
is separable, then the separable degree of `K / F` is equal to the degree of `K / E`.
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_of_isSeparable
    [IsPurelyInseparable F E] [Algebra.IsSeparable E K] : sepDegree F K = Module.rank E K

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
inst✝ : Algebra.IsSeparable E K
⊢ sepDegree F K = Module.rank E K

Tactic:
let S := separableClosure F K

Result:
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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
⊢ sepDegree F K = Module.rank E K

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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E K ≤ Module.rank F ↥S
⊢ sepDegree F K = Module.rank E K

Tactic:
obtain ⟨ι, ⟨b⟩⟩ := Basis.exists_basis F S

Result:
case intro.intro
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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E K ≤ Module.rank F ↥S
ι : Set ↥S
b : Basis (↑ι) F ↥S
⊢ sepDegree F K = Module.rank E K

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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E ↥(adjoin E ↑S) ≤ Module.rank F ↥S
⊢ sepDegree F K = Module.rank E K

Tactic:
rw [separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable K, rank_top'] at h

Result:
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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E K ≤ Module.rank F ↥S
⊢ sepDegree F K = Module.rank E K

Proof state:
case intro.intro
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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E K ≤ Module.rank F ↥S
ι : Set ↥S
b : Basis (↑ι) F ↥S
⊢ sepDegree F K = Module.rank E K

Tactic:
exact h.antisymm' (b.mk_eq_rank'' ▸ (b.linearIndependent.map' S.val.toLinearMap
  (LinearMap.ker_eq_bot_of_injective S.val.injective)
  |>.map_of_isPurelyInseparable_of_isSeparable E (fun i ↦
    by simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (b i))
  |>.cardinal_le_rank))

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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
⊢ sepDegree F K = Module.rank E K

Tactic:
have h := S.adjoin_rank_le_of_isAlgebraic_right E

Result:
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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E ↥(adjoin E ↑S) ≤ Module.rank F ↥S
⊢ sepDegree F K = Module.rank E K

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
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
h : Module.rank E K ≤ Module.rank F ↥S
ι : Set ↥S
b : Basis (↑ι) F ↥S
i : ↑ι
⊢ IsSeparable F ((⇑S.val.toLinearMap ∘ ⇑b) i)

Tactic:
simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (b i)

Result:
no goals