-- 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
l : ↥L
⊢ IsGalois k
    ↥(IntermediateField.lift
        (IntermediateField.fixedField
          (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))

Tactic:
let _ := IsGalois.of_fixedField_normal_subgroup (Subgroup.map (restrictNormalHom
  (adjoin k {l.1})) L.fixingSubgroup)

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 : 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
l : ↥L
x✝ : IsGalois k
  ↥(IntermediateField.fixedField
      (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)) :=
  IsGalois.of_fixedField_normal_subgroup
    (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)
⊢ IsGalois k
    ↥(IntermediateField.lift
        (IntermediateField.fixedField
          (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))

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

Tactic:
apply iSup_le

Result:
case a.h
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)
⊢ ∀ (i : ↥L), f i ≤ L

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

Tactic:
intro l hl

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 : K
hl : l ∈ 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
⊢ IsGalois k ↥L

Tactic:
let f : L → IntermediateField k K := fun x => IntermediateField.lift <|
  IntermediateField.fixedField <| Subgroup.map (restrictNormalHom (adjoin k {x.1}))
  L.fixingSubgroup

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))
⊢ IsGalois k ↥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)))
n : Normal k ↥L
this : ⨆ l, f l = L
⊢ IsGalois k ↥L

Tactic:
let _ : Algebra.IsSeparable k L := Algebra.isSeparable_tower_bot_of_isSeparable k L K

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
this : ⨆ l, f l = L
x✝ : Algebra.IsSeparable k ↥L := Algebra.isSeparable_tower_bot_of_isSeparable k (↥L) K
⊢ IsGalois k ↥L