-- 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:
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

Tactic:
exact sub

Result:
no goals

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
this : L ≤ L'.toIntermediateField
x✝ : Algebra ↥L ↥L'.toIntermediateField := (↑(inclusion this)).toAlgebra
⊢ FiniteDimensional k ↥L

Tactic:
exact FiniteDimensional.left k L L'.1

Result:
no goals

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
⊢ FiniteDimensional k ↥L

Tactic:
have := hM.out

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
⊢ 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
this : (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier ∈ GroupFilterBasis.toFilterBasis.filter
⊢ FiniteDimensional k ↥L

Tactic:
rcases this with ⟨S, ⟨gp, ⟨M, hM, eq'⟩, eq⟩, 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)
sub : S ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
⊢ 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
⊢ FiniteDimensional k ↥L

Tactic:
let L' : FiniteGaloisIntermediateField k K := {
  normalClosure k M K with
  finiteDimensional := normalClosure.is_finiteDimensional k M K
  isGalois := IsGalois.normalClosure k M K }

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
⊢ 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
this : L ≤ L'.toIntermediateField
⊢ FiniteDimensional k ↥L

Tactic:
let _ : Algebra L L'.1 := RingHom.toAlgebra (IntermediateField.inclusion this)

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
x✝ : Algebra ↥L ↥L'.toIntermediateField := (↑(inclusion this)).toAlgebra
⊢ 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
⊢ IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k ↥L

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.fixingSubgroup_isOpen L⟩

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
⊢ 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)
sub : S ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
gp : Subgroup (K ≃ₐ[k] K)
eq : (fun g => g.carrier) gp = S
M : IntermediateField k K
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
⊢ FiniteDimensional k ↥L

Tactic:
rw [← eq, ← eq'] at 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
⊢ FiniteDimensional k ↥L