Le maximal Unramified iff

theorem le_maximalUnramified_iff : E ≤ maximalUnramified K L ↔ IsUnramified K E := by  refine ⟨fun h ↦ .comap <| show E →ₐ[K] maximalUnramified K L from Subalgebra.inclusion h,    fun _ ↦ ?_⟩  obtain ⟨φ₁⟩ := nonempty_unramifiedExtension_algEquiv_of_isUnramified K E  have h₁ : Module.finrank K E ∣ f K L := .trans (IsUnramified.n_dvd_f K E) <| f_dvd_f_top ..  obtain ⟨φ₂⟩ := nonempty_unramifiedExtension_alghom_of_dvd_f K (UnramifiedExtension K (f K L))    (Module.finrank K E) (by simpa [f_unramifiedExtension _ (f_pos _ _).ne'])  unfold maximalUnramified  generalize Nonempty.some _ = φ₃  rw [← IntermediateField.toSubalgebra_le_toSubalgebra, AlgHom.fieldRange_toSubalgebra,    ← AlgHom.fieldRange_of_normal (E := E) (φ₃.comp (φ₂.comp φ₁.symm)),    AlgHom.fieldRange_toSubalgebra]  exact AlgHom.range_comp_le_range ..