-- Mathlib/FieldTheory/Galois/Infinite.lean
theorem normal_iff_isGalois (L : IntermediateField k K) [IsGalois k K] :
    L.fixingSubgroup.Normal ↔ 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))
⊢ IsGalois k ↥L

Tactic:
have h' (x : K) : (Subgroup.map (restrictNormalHom (adjoin k {x})) L.fixingSubgroup).Normal :=
  Subgroup.Normal.map h (restrictNormalHom (adjoin k {x})) (restrictNormalHom_surjective 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
⊢ IsGalois k ↥L

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

Tactic:
intro l

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)
l : ↥L
⊢ f l ≤ 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
⊢ IsGalois k ↥L

Tactic:
have n' (l : L) : IsGalois k (IntermediateField.fixedField <| Subgroup.map
  (restrictNormalHom (adjoin k {l.1})) L.fixingSubgroup) := by
  let _ := IsGalois.of_fixedField_normal_subgroup (Subgroup.map (restrictNormalHom
    (adjoin k {l.1})) L.fixingSubgroup)
  let cH := (Subgroup.map (restrictNormalHom (adjoin k {l.1})) L.fixingSubgroup)
  exact IsGalois.of_algEquiv <| IntermediateField.liftAlgEquiv (IntermediateField.fixedField cH)

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

Tactic:
rw [this] at n

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

Proof state:
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)
l : ↥L
⊢ f l ≤ L

Tactic:
simpa only [f, ← restrict_fixedField L.fixingSubgroup (adjoin k {l.1}),
  fixedField_fixingSubgroup L] using inf_le_left

Result:
no goals

Proof state:
case refine_2
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 : IsGalois k ↥L
⊢ L.fixingSubgroup.Normal

Tactic:
simpa only [IntermediateFieldEquivClosedSubgroup, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
  ← L.restrictNormalHom_ker] using MonoidHom.normal_ker (restrictNormalHom L)

Result:
no goals