Existence of prime-power-index intermediate fields

We prove the existence of prime-power-index intermediate fields in a Galois extension using Sylow's first theorem.

theorem IsGalois.exists_intermediateField_finrank_pow_prime_le_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p : ℕ} (hp : Nat.Prime p) {n : ℕ} {M N : IntermediateField K L} (hM : Module.finrank (↥M) L ∣ p ^ n) (hN : p ^ n ∣ Module.finrank (↥N) L) (hMN : N ≤ M) : ∃ (O : IntermediateField K L), Module.finrank (↥O) L = p ^ n ∧ N ≤ O ∧ O ≤ M

theorem IsGalois.exists_intermediateField_finrank_pow_prime_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p : ℕ} (hp : Nat.Prime p) {n : ℕ} (h : p ^ n ∣ Module.finrank K L) (M : IntermediateField K L) (hM : Module.finrank (↥M) L ∣ p ^ n) : ∃ N ≤ M, Module.finrank (↥N) L = p ^ n

theorem IsGalois.exists_intermediateField_finrank_pow_prime_ge {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p : ℕ} (hp : Nat.Prime p) {n : ℕ} (M : IntermediateField K L) (hM : p ^ n ∣ Module.finrank (↥M) L) : ∃ N ≥ M, Module.finrank (↥N) L = p ^ n

theorem IsGalois.exists_intermediateField_finrank_pow_prime {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p : ℕ} (hp : Nat.Prime p) {n : ℕ} (h : p ^ n ∣ Module.finrank K L) : ∃ (N : IntermediateField K L), Module.finrank (↥N) L = p ^ n