awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
h₁ :
  Membership.mem (γ := IntermediateField k ↥L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))
    (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)
⊢ x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)

Tactic:
apply (mem_lift (⟨x, xL⟩ : L)).mpr

Premises used: Iff.mpr, IntermediateField.mem_lift, 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
h₁ :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
⊢ Membership.mem (γ := IntermediateField k ↥L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))
    (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)

Tactic:
simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂]

Premises used: and_imp, forall_exists_index, IntermediateField.mem_fixedField_iff, Subgroup.mem_map, forall_apply_eq_imp_iff₂
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
σ : Gal(K/k)
hσ : σ ∈ H
h₁ :
  (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) : K)
⊢ (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
      (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
    Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
σ : Gal(K/k)
hσ : σ ∈ H
h₁ :
  (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x
⊢ (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) : K)

Tactic:
dsimp only
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
σ : Gal(K/k)
hσ : σ ∈ H
h₁ :
  (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    Subtype.mk (p := fun (x : Gal(K/k)) ↦ x ∈ H) σ hσ • x
⊢ (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x

Tactic:
nth_rw 2 [← (h.out.1 ⟨σ, hσ⟩)]

Premises used: Membership.mem.out, Subtype.mk, And.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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
σ : Gal(K/k)
hσ : σ ∈ H
⊢ (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    Subtype.mk (p := fun (x : Gal(K/k)) ↦ x ∈ H) σ hσ • x

Tactic:
AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩

Premises used: Membership.mem, Subtype, Subtype.mk, AlgEquiv.restrictNormal_commutes
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
xL : Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x
σ : Gal(K/k)
hσ : σ ∈ H
⊢ (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    Subtype.mk (p := fun (x : Gal(K/k)) ↦ x ∈ H) σ hσ • x

Tactic:
exact AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩

Premises used: Membership.mem, Subtype, Subtype.mk, AlgEquiv.restrictNormal_commutes
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)
⊢ x ∈ L

Tactic:
have xL := lift_le _ 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)
xL : x ∈ L
⊢ Membership.mem (γ := IntermediateField k ↥L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))
    (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)

Tactic:
apply (mem_lift (⟨x, xL⟩ : L)).mp at h

Premises used: IntermediateField.mem_lift, Subtype.mk, Iff.mp
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  Membership.mem (γ := IntermediateField k ↥L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))
    (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)
⊢ ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL

Tactic:
simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at h

Premises used: and_imp, forall_exists_index, IntermediateField.mem_fixedField_iff, Subgroup.mem_map, forall_apply_eq_imp_iff₂
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
h₁ : ∀ f ∈ H, (f : (a : K) → K) x = x
⊢ x ∈ (↑(fixedField H ⊓ L) : Set K)

Tactic:
simp only [coe_inf, Set.mem_inter_iff, SetLike.mem_coe, mem_fixedField_iff, xL, and_true]

Premises used: and_true, Set.mem_inter_iff, IntermediateField.mem_fixedField_iff, IntermediateField.coe_inf, SetLike.mem_coe
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
σ : Gal(K/k)
hσ : σ ∈ H
rw rw₁ : (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) : K) = x
⊢ (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x

Tactic:
rw [h σ 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
σ : Gal(K/k)
hσ : σ ∈ H
⊢ (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x

Tactic:
have : ((restrictNormalHom L σ) ⟨x, xL⟩).1 = x := by rw [h σ 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
σ : Gal(K/k)
hσ : σ ∈ H
this :
  (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x
h₁ :
  Eq (α := K) ((σ : (a : K) → K) x : K)
    ((↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
        K) :
      K)
⊢ (σ : (a : K) → K) x = x

Tactic:
nth_rw 2 [← this]
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
σ : Gal(K/k)
hσ : σ ∈ H
this :
  (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x
⊢ Eq (α := K) ((σ : (a : K) → K) x : K)
    ((↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
        K) :
      K)

Tactic:
(AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩).symm

Premises used: Membership.mem, Subtype, Subtype.mk, AlgEquiv.restrictNormal_commutes, Eq.symm
-- 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
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
xL : x ∈ L
h :
  ∀ a ∈ H,
    (((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) a : Gal(↥L/k)) : (a : ↥L) → ↥L)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL) =
      Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL
σ : Gal(K/k)
hσ : σ ∈ H
this :
  (↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
      K) =
    x
⊢ Eq (α := K) ((σ : (a : K) → K) x : K)
    ((↑((((restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) σ : Gal(↥L/k)) : (a : ↥L) → ↥L)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ L) x xL)) :
        K) :
      K)

Tactic:
exact (AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩).symm

Premises used: Membership.mem, Subtype, Subtype.mk, AlgEquiv.restrictNormal_commutes, Eq.symm
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
apply : (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup ≤ (↑H : Subgroup Gal(K/k))
⊢ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup = (↑H : Subgroup Gal(K/k))

Tactic:
apply le_antisymm _ ((IntermediateField.le_iff_le H.toSubgroup
    (IntermediateField.fixedField H.toSubgroup)).mp le_rfl)

Premises used: ClosedSubgroup.toSubgroup, le_rfl, IntermediateField.fixedField, le_antisymm, Iff.mp, 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
by_contra : ∀ (h : σ ∉ (↑H : Subgroup Gal(K/k))), False
⊢ σ ∈ (↑H : Subgroup Gal(K/k))

Tactic:
by_contra 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
⊢ (↑H : Subgroup Gal(K/k)).carrierᶜ ∈ nhds σ

Tactic:
have nhds : H.carrierᶜ ∈ nhds σ := H.isClosed'.isOpen_compl.mem_nhds 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
nhds : (↑H : Subgroup Gal(K/k)).carrierᶜ ∈ _root_.nhds σ
⊢ (↑H : Subgroup Gal(K/k)).carrierᶜ ∈ GroupFilterBasis.N (galGroupBasis k K) σ

Tactic:
rw [GroupFilterBasis.nhds_eq (x₀ := σ) (galGroupBasis k K)] at nhds

Premises used: galGroupBasis, GroupFilterBasis.nhds_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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
nhds : (↑H : Subgroup Gal(K/k)).carrierᶜ ∈ GroupFilterBasis.N (galGroupBasis k K) σ
rcases :
  ∀ (b : Set Gal(K/k)) (sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ)
    (gp : Subgroup Gal(K/k)) (eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = b) (L : IntermediateField k K)
    (hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L) (eq' : L.fixingSubgroup = gp), False
⊢ False

Tactic:
rcases nhds with ⟨b, ⟨gp, ⟨L, hL, 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = b
L : IntermediateField k K
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
⊢ (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b

Tactic:
rw [← eq'] at 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = b
L : IntermediateField k K
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
eq₁ : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
⊢ Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L

Tactic:
rw [← eq'] at 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) gp = b
L : IntermediateField k K
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
eq₁ : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL₁ : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
⊢ L.fixingSubgroup = gp

Tactic:
rw [← eq'] at 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
⊢ FiniteDimensional.{u_1, u_2} k ↥L

Tactic:
have := hL.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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun (x : Gal(K/k)) ↦ σ • x) τ = φ
⊢ σ • b ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ

Tactic:
have sub' : σ • b ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun (x : Gal(K/k)) ↦ σ • x) τ = φ
sub' : σ • b ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
a : φ ∈ σ • b
⊢ φ ∈ (↑H : Subgroup Gal(K/k)).carrierᶜ

Tactic:
apply 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun (x : Gal(K/k)) ↦ σ • x) τ = φ
sub' : σ • b ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
a : σ • τ ∈ σ • L.fixingSubgroup.carrier
⊢ φ ∈ σ • b

Tactic:
simp only [← muleq, ← 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun (x : Gal(K/k)) ↦ σ • x) τ = φ
sub' : σ • b ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
a : τ ∈ L.fixingSubgroup.carrier
⊢ σ • τ ∈ σ • L.fixingSubgroup.carrier

Tactic:
apply Set.smul_mem_smul_set

Premises used: Set.smul_mem_smul_set
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun (x : Gal(K/k)) ↦ σ • x) τ = φ
sub' : σ • b ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
⊢ τ ∈ L.fixingSubgroup.carrier

Tactic:
(L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)

Premises used: Set.Mem, IntermediateField.fixingSubgroup_le, IntermediateField.le_normalClosure