-- Mathlib/FieldTheory/Galois/Infinite.lean
theorem isOpen_iff_finite (L : IntermediateField k K) [IsGalois k K] :
    IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k L

Proof state:
case intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set (K ≃ₐ[k] K)
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
sub : (fun g => g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  FiniteGaloisIntermediateField.mk __src
⊢ FiniteDimensional k ↥L

Tactic:
have : L ≤ L'.1 := by
  apply le_trans _ (IntermediateField.le_normalClosure M)
  rw [←  fixedField_fixingSubgroup M, IntermediateField.le_iff_le]
  exact sub

Result:
case intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set (K ≃ₐ[k] K)
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
sub : (fun g => g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  FiniteGaloisIntermediateField.mk __src
this : L ≤ L'.toIntermediateField
⊢ FiniteDimensional k ↥L

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set (K ≃ₐ[k] K)
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
sub : (fun g => g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  FiniteGaloisIntermediateField.mk __src
⊢ L ≤ L'.toIntermediateField

Tactic:
apply le_trans _ (IntermediateField.le_normalClosure M)

Result:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set (K ≃ₐ[k] K)
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
sub : (fun g => g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  FiniteGaloisIntermediateField.mk __src
⊢ L ≤ M

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set (K ≃ₐ[k] K)
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
sub : (fun g => g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  FiniteGaloisIntermediateField.mk __src
⊢ L ≤ M

Tactic:
rw [←  fixedField_fixingSubgroup M, IntermediateField.le_iff_le]

Result:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set (K ≃ₐ[k] K)
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
sub : (fun g => g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  FiniteGaloisIntermediateField.mk __src
⊢ M.fixingSubgroup ≤ L.fixingSubgroup

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this : (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier ∈ nhds 1
⊢ FiniteDimensional k ↥L

Tactic:
rw [GroupFilterBasis.nhds_one_eq] at this

Result:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this : (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier ∈ GroupFilterBasis.toFilterBasis.filter
⊢ FiniteDimensional k ↥L

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
⊢ FiniteDimensional k ↥L

Tactic:
have : (IntermediateFieldEquivClosedSubgroup.toFun L).carrier ∈ nhds 1 :=
  IsOpen.mem_nhds h (congrFun rfl)

Result:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this : (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier ∈ nhds 1
⊢ FiniteDimensional k ↥L