awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K_1 : Type u_2
inst : Field k
inst_1 : Field K_1
inst_2 : Algebra k K_1
inst_3 : IsGalois k K_1
K L : IntermediateField k K_1
⊢ LE.le (α := (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
      (({ toFun := fun (L : IntermediateField k K_1) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
              invFun := fun (H : (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↦
                IntermediateField.fixedField (↑H : Subgroup Gal(K_1/k)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField k K_1) → (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
          K :
        (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
      (({ toFun := fun (L : IntermediateField k K_1) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
              invFun := fun (H : (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↦
                IntermediateField.fixedField (↑H : Subgroup Gal(K_1/k)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField k K_1) → (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
          L :
        (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
H : ClosedSubgroup Gal(K/k)
inst_4 : (↑H : Subgroup Gal(K/k)).Normal
σ : Gal(K/k)
⊢ Eq (α := Gal(↥(fixedField (↑H : Subgroup Gal(K/k)))/k))
    ((normalAutEquivQuotient H :
          (a : Gal(K/k) ⧸ (↑H : Subgroup Gal(K/k))) → Gal(↥(fixedField (↑H : Subgroup Gal(K/k)))/k))
        (↑σ : Gal(K/k) ⧸ (↑H : Subgroup Gal(K/k))) :
      Gal(↥(fixedField (↑H : Subgroup Gal(K/k)))/k))
    ((restrictNormalHom ↥(fixedField (↑H : Subgroup Gal(K/k))) :
          (a : Gal(K/k)) → Gal(↥(fixedField (↑H : Subgroup Gal(K/k)))/k))
        σ :
      Gal(↥(fixedField (↑H : Subgroup Gal(K/k)))/k))

Tactic:
rfl

Premises used: Quotient.liftOn', AlgEquiv.ofBijective, AlgEquiv.restrictNormal, Con.liftOn, AlgHom.restrictNormal', rfl
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
⊢ IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional.{u_1, u_2} k ↥L

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

Premises used: Iff.intro, IntermediateField.fixingSubgroup_isOpen
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
refine : ∀ (h : IsOpen L.fixingSubgroup.carrier), FiniteDimensional.{u_1, u_2} k ↥L
⊢ IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional.{u_1, u_2} k ↥L

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.fixingSubgroup_isOpen L⟩
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
⊢ Membership.mem (γ := Filter Gal(K/k)) (nhds 1)
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier

Tactic:
have : (IntermediateFieldEquivClosedSubgroup.toFun L).carrier ∈ nhds 1 :=
    IsOpen.mem_nhds h (congrFun rfl)
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this :
  Membership.mem (γ := Filter Gal(K/k)) (nhds 1)
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
⊢ Membership.mem (γ := Filter Gal(K/k)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ aut _))
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier

Tactic:
rw [GroupFilterBasis.nhds_one_eq] at this

Premises used: GroupFilterBasis.nhds_one_eq
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this :
  Membership.mem (γ := Filter Gal(K/k)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ aut _))
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
rcases :
  ∀ (S : Set Gal(K/k))
    (sub :
      S ⊆
        (↑(Equiv.toFun
                (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
                L) :
            Subgroup Gal(K/k)).carrier)
    (gp : Subgroup Gal(K/k)) (eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S) (M : IntermediateField k K)
    (hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M) (eq' : M.fixingSubgroup = gp),
    FiniteDimensional.{u_1, u_2} k ↥L
⊢ FiniteDimensional.{u_1, u_2} k ↥L

Tactic:
rcases this with ⟨S, ⟨gp, ⟨M, hM, eq'⟩, eq⟩, sub⟩
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
sub :
  S ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
rw :
  ∀ (eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S) (M : IntermediateField k K)
    (sub :
      (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
        (↑(Equiv.toFun
                (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
                L) :
            Subgroup Gal(K/k)).carrier)
    (hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M) (eq' : M.fixingSubgroup = gp),
    FiniteDimensional.{u_1, u_2} k ↥L
⊢ FiniteDimensional.{u_1, u_2} k ↥L

Tactic:
rw [← eq, ← eq'] at sub
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
⊢ FiniteDimensional.{u_1, u_2} k ↥M

Tactic:
have := hM.out
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
apply : L ≤ M
⊢ L ≤ L'.toIntermediateField

Tactic:
apply le_trans _ (IntermediateField.le_normalClosure M)

Premises used: IntermediateField.le_normalClosure, le_trans
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
rw : M.fixingSubgroup ≤ L.fixingSubgroup
⊢ L ≤ M

Tactic:
rw [← fixedField_fixingSubgroup M, IntermediateField.le_iff_le]

Premises used: InfiniteGalois.fixedField_fixingSubgroup, IntermediateField.le_iff_le
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ M.fixingSubgroup ≤ L.fixingSubgroup

Tactic:
sub

Premises used: Set.Mem, Set.Subset
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ M.fixingSubgroup ≤ L.fixingSubgroup

Tactic:
exact sub
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ L ≤ L'.toIntermediateField

Tactic:
have : L ≤ L'.1 := by
    apply le_trans _ (IntermediateField.le_normalClosure M)
    rw [← fixedField_fixingSubgroup M, IntermediateField.le_iff_le]
    exact sub
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
this : L ≤ L'.toIntermediateField
x : Algebra ↥L ↥L'.toIntermediateField := RingHom.toAlgebra (↑(inclusion this) : ↥L →+* ↥L'.toIntermediateField)
⊢ FiniteDimensional.{u_1, u_2} k ↥L

Tactic:
FiniteDimensional.left k L L'.1

Premises used: Membership.mem, Subtype, FiniteGaloisIntermediateField.toIntermediateField, FiniteDimensional.left
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = S
M : IntermediateField k K
sub :
  (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) M.fixingSubgroup ⊆
    (↑(Equiv.toFun
            (RelIso.toEquiv (r := fun (x1 x2 : IntermediateField k K) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ x1 ≤ x2) IntermediateFieldEquivClosedSubgroup)
            L) :
        Subgroup Gal(K/k)).carrier
hM : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) M
eq' : M.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
this : L ≤ L'.toIntermediateField
x : Algebra ↥L ↥L'.toIntermediateField := RingHom.toAlgebra (↑(inclusion this) : ↥L →+* ↥L'.toIntermediateField)
⊢ FiniteDimensional.{u_1, u_2} k ↥L

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

Premises used: Membership.mem, Subtype, FiniteGaloisIntermediateField.toIntermediateField, FiniteDimensional.left
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
⊢ L.fixingSubgroup.Normal ↔ IsGalois.{u_1, u_2} k ↥L

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

Premises used: Iff.intro
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
refine_1 : ∀ (h : L.fixingSubgroup.Normal), IsGalois.{u_1, u_2} k ↥L
refine_2 : ∀ (h : IsGalois.{u_1, u_2} k ↥L), L.fixingSubgroup.Normal
⊢ L.fixingSubgroup.Normal ↔ IsGalois.{u_1, u_2} k ↥L

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
⊢ ∀ (x : K), (g x).Normal

Tactic:
have (x : K) : (g x).Normal :=
      Subgroup.Normal.map h (restrictNormalHom (adjoin k {x})) (restrictNormalHom_surjective K)
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this : ∀ (x : K), (g x).Normal
⊢ ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)

Tactic:
have (l : L) : Normal k (f l) :=
      Normal.of_algEquiv <| IntermediateField.liftAlgEquiv <| IntermediateField.fixedField (g l.1)
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
⊢ Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)

Tactic:
have n : Normal k ↥(⨆ l : L, f l) := IntermediateField.normal_iSup k K f
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
a : ⨆ (l : ↥L), f l ≤ L
a₁ : L ≤ ⨆ (l : ↥L), f l
⊢ ⨆ (l : ↥L), f l = L

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
a : ∀ (i : ↥L), f i ≤ L
⊢ ⨆ (l : ↥L), f l ≤ L

Tactic:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
l : ↥L
⊢ f l ≤ L

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

Premises used: InfiniteGalois.fixedField_fixingSubgroup, IntermediateField.fixingSubgroup, InfiniteGalois.restrict_fixedField, FiniteGaloisIntermediateField.adjoin, FiniteGaloisIntermediateField.toIntermediateField, inf_le_left, Singleton.singleton, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
l : K
hl : l ∈ L
a : l ∈ f (Subtype.mk (p := fun (x : K) ↦ x ∈ L) l hl)
⊢ Membership.mem (γ := IntermediateField k K) (⨆ (l : ↥L), f l) l

Tactic:
apply le_iSup f ⟨l, hl⟩

Premises used: le_iSup, Subtype.mk
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
l : K
hl : l ∈ L
⊢ l ∈ f (Subtype.mk (p := fun (x : K) ↦ x ∈ L) l hl)

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

Premises used: le_rfl, InfiniteGalois.fixedField_fixingSubgroup, IntermediateField.fixingSubgroup, IntermediateField.mem_inf, InfiniteGalois.restrict_fixedField, FiniteGaloisIntermediateField.adjoin, Iff.mp, FiniteGaloisIntermediateField.toIntermediateField, Singleton.singleton, true_and, FiniteGaloisIntermediateField.adjoin_simple_le_iff