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

Tactic:
apply le_iSup f ⟨l,hl⟩

Result:
case a.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 ∈ f ⟨l, hl⟩

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

Tactic:
apply IsGalois.mk

Result:
no goals

Proof state:
case a.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 ∈ f ⟨l, hl⟩

Tactic:
simpa only [f, ← restrict_fixedField L.fixingSubgroup (adjoin k {l}),
  fixedField_fixingSubgroup L, IntermediateField.mem_inf, hl, true_and]
  using adjoin_simple_le_iff.mp le_rfl

Result:
no goals

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

Tactic:
exact IsGalois.of_algEquiv <| IntermediateField.liftAlgEquiv (IntermediateField.fixedField cH)

Result:
no goals

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
⊢ L.fixingSubgroup.Normal ↔ IsGalois k ↥L

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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

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

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

Tactic:
let cH := (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)
cH : Subgroup (↥(adjoin k {↑l}).toIntermediateField ≃ₐ[k] ↥(adjoin k {↑l}).toIntermediateField) :=
  Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup
⊢ IsGalois k
    ↥(IntermediateField.lift
        (IntermediateField.fixedField
          (Subgroup.map (restrictNormalHom ↥(adjoin k {↑l}).toIntermediateField) L.fixingSubgroup)))