-- Mathlib/FieldTheory/Galois/Infinite.lean
theorem normal_iff_isGalois (L : IntermediateField k K) [IsGalois k K] :
    L.fixingSubgroup.Normal ↔ IsGalois 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 : L.fixingSubgroup.Normal
f : ↥L → IntermediateField k K :=
  fun x =>
    IntermediateField.lift
      (IntermediateField.fixedField
        (Subgroup.map (restrictNormalHom ↥(adjoin k {↑x}).toIntermediateField) L.fixingSubgroup))
h' : ∀ (x : K), (Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup).Normal
n' :
  ∀ (l : ↥L),
    IsGalois k
      ↥(IntermediateField.lift
          (IntermediateField.fixedField
            (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))
n : Normal k ↥(⨆ l, f l)
⊢ ⨆ l, f l = L

Tactic:
apply le_antisymm

Result:
case a
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 : L.fixingSubgroup.Normal
f : ↥L → IntermediateField k K :=
  fun x =>
    IntermediateField.lift
      (IntermediateField.fixedField
        (Subgroup.map (restrictNormalHom ↥(adjoin k {↑x}).toIntermediateField) L.fixingSubgroup))
h' : ∀ (x : K), (Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup).Normal
n' :
  ∀ (l : ↥L),
    IsGalois k
      ↥(IntermediateField.lift
          (IntermediateField.fixedField
            (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))
n : Normal k ↥(⨆ l, f l)
⊢ ⨆ l, f l ≤ L

case a
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 : L.fixingSubgroup.Normal
f : ↥L → IntermediateField k K :=
  fun x =>
    IntermediateField.lift
      (IntermediateField.fixedField
        (Subgroup.map (restrictNormalHom ↥(adjoin k {↑x}).toIntermediateField) L.fixingSubgroup))
h' : ∀ (x : K), (Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup).Normal
n' :
  ∀ (l : ↥L),
    IsGalois k
      ↥(IntermediateField.lift
          (IntermediateField.fixedField
            (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))
n : Normal k ↥(⨆ l, f l)
⊢ L ≤ ⨆ l, f l

Proof state:
case refine_1
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 : L.fixingSubgroup.Normal
f : ↥L → IntermediateField k K :=
  fun x =>
    IntermediateField.lift
      (IntermediateField.fixedField
        (Subgroup.map (restrictNormalHom ↥(adjoin k {↑x}).toIntermediateField) L.fixingSubgroup))
h' : ∀ (x : K), (Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup).Normal
n' :
  ∀ (l : ↥L),
    IsGalois k
      ↥(IntermediateField.lift
          (IntermediateField.fixedField
            (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))
⊢ IsGalois k ↥L

Tactic:
have n : Normal k ↥(⨆ (l : L), f l) := IntermediateField.normal_iSup k K f

Result:
case refine_1
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 : L.fixingSubgroup.Normal
f : ↥L → IntermediateField k K :=
  fun x =>
    IntermediateField.lift
      (IntermediateField.fixedField
        (Subgroup.map (restrictNormalHom ↥(adjoin k {↑x}).toIntermediateField) L.fixingSubgroup))
h' : ∀ (x : K), (Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup).Normal
n' :
  ∀ (l : ↥L),
    IsGalois k
      ↥(IntermediateField.lift
          (IntermediateField.fixedField
            (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))
n : Normal k ↥(⨆ l, f l)
⊢ IsGalois k ↥L