awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
U : Set Gal(L/K)
hU : Membership.mem (γ := Set (Set Gal(L/K))) (FilterBasis.sets (galBasis K L)) U
rcases :
  ∀ (H : Subgroup Gal(L/K)),
    Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) H →
      Subset.{u_2} (α := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H)
        (Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ x⁻¹) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H))
⊢ U ⊆ (fun (x : Gal(L/K)) ↦ x⁻¹) ⁻¹' U

Tactic:
rcases hU with ⟨H, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : Subgroup Gal(L/K)
left : Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) H
⊢ Subset.{u_2} (α := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H)
    (Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ x⁻¹) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H))

Tactic:
fun _ => H.inv_mem'

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Subgroup.inv_mem'
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : Subgroup Gal(L/K)
left : Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) H
⊢ Subset.{u_2} (α := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H)
    (Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ x⁻¹) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H))

Tactic:
exact fun _ => H.inv_mem'

Premises used: Subgroup.inv_mem'
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
⊢ ∃ (V : Set Gal(L/K)),
    Membership.mem (γ := Set (Set Gal(L/K))) (FilterBasis.sets (galBasis K L)) V ∧
      V ⊆
        Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ σ * x * σ⁻¹)
          ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E.fixingSubgroup)

Tactic:
⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, ?_, rfl⟩, rfl⟩, fun g hg => ?_⟩⟩

Premises used: Submonoid.toSubsemigroup, IntermediateField.fixingSubgroup, And.intro, Exists.intro, Subsemigroup.carrier, rfl, Subgroup.toSubmonoid
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
refine_1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) F
refine_2 :
  ∀ (g : Gal(L/K)) (hg : g ∈ F.fixingSubgroup.carrier),
    Membership.mem (γ := Set Gal(L/K))
      (Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ σ * x * σ⁻¹)
        ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E.fixingSubgroup))
      g
⊢ ∃ (V : Set Gal(L/K)),
    Membership.mem (γ := Set (Set Gal(L/K))) (FilterBasis.sets (galBasis K L)) V ∧
      V ⊆
        Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ σ * x * σ⁻¹)
          ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E.fixingSubgroup)

Tactic:
refine ⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, ?_, rfl⟩, rfl⟩, fun g hg => ?_⟩⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
⊢ FiniteDimensional.{u_1, u_2} K ↥E

Tactic:
have : FiniteDimensional K E := hE
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
this : FiniteDimensional.{u_1, u_2} K ↥E
⊢ Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) F

Tactic:
IntermediateField.finiteDimensional_map σ.symm.toAlgHom

Premises used: finiteExts, AlgEquiv.toAlgHom, AlgEquiv.symm, Set.Mem, setOf, IntermediateField.finiteDimensional_map
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
this : FiniteDimensional.{u_1, u_2} K ↥E
⊢ Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) F

Tactic:
exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, IntermediateField.finiteDimensional_map
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
refine_2 : σ * g * σ⁻¹ ∈ E.fixingSubgroup
⊢ Membership.mem (γ := Set Gal(L/K))
    (Set.preimage (β := Gal(L/K)) (fun (x : Gal(L/K)) ↦ σ * x * σ⁻¹)
      ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E.fixingSubgroup))
    g

Tactic:
change σ * g * σ⁻¹ ∈ E.fixingSubgroup

Premises used: IntermediateField.fixingSubgroup
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
refine_2 : ∀ x ∈ E, (σ * g * σ⁻¹ : (a : L) → L) x = x
⊢ σ * g * σ⁻¹ ∈ E.fixingSubgroup

Tactic:
rw [IntermediateField.mem_fixingSubgroup_iff]

Premises used: IntermediateField.mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
refine_2 : (σ : (a : L) → L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) = x
⊢ (σ * g * σ⁻¹ : (a : L) → L) x = x

Tactic:
change σ (g (σ⁻¹ x)) = x

Premises used: Inv.inv, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
⊢ Eq (α := L) (((↑(↑σ.symm : L →ₐ[K] L) : L →+* L) : (a : L) → L) x : L) ((σ⁻¹ : (a : L) → L) x : L)

Tactic:
dsimp
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
⊢ Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)

Tactic:
have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
rw :
  ∀ (hg : ∀ x ∈ F, (g : (a : L) → L) x = x) (x : L) (hx : x ∈ E)
    (h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)),
    Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)
⊢ Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)

Tactic:
rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg

Premises used: Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : ∀ x ∈ F, (g : (a : L) → L) x = x
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
⊢ Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)

Tactic:
hg (σ⁻¹ x) h_in_F

Premises used: Inv.inv, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : ∀ x ∈ F, (g : (a : L) → L) x = x
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
⊢ Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)

Tactic:
exact hg (σ⁻¹ x) h_in_F

Premises used: Inv.inv, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
⊢ Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)

Tactic:
have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x := by
      rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
      exact hg (σ⁻¹ x) h_in_F
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
h_g_fix : Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)
refine_2 : (σ : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) = x
⊢ (σ : (a : L) → L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) = x

Tactic:
rw [h_g_fix]
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
h_g_fix : Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)
⊢ (σ : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) = x

Tactic:
AlgEquiv.apply_symm_apply σ x

Premises used: AlgEquiv.apply_symm_apply
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
F : IntermediateField K L := IntermediateField.map (↑σ.symm : L →ₐ[K] L) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
h_in_F : Membership.mem (α := L) F ((σ⁻¹ : (a : L) → L) x : L)
h_g_fix : Eq (α := L) ((g : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) : L) ((σ⁻¹ : (a : L) → L) x : L)
⊢ (σ : (a : L) → L) ((σ⁻¹ : (a : L) → L) x : L) = x

Tactic:
exact AlgEquiv.apply_symm_apply σ x

Premises used: AlgEquiv.apply_symm_apply
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ IsTopologicalGroup.{u_2} Gal(L/K)

Tactic:
GroupFilterBasis.isTopologicalGroup (galGroupBasis K L)

Premises used: galGroupBasis, GroupFilterBasis.isTopologicalGroup
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Set Gal(L/K)
rw :
  Membership.mem (γ := Filter Gal(L/K)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ AlgEquiv.aut _)) s ↔
    ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) s ↔
    ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
rw [GroupFilterBasis.nhds_one_eq]

Premises used: GroupFilterBasis.nhds_one_eq
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Set Gal(L/K)
mp :
  Membership.mem (γ := Filter Gal(L/K)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ AlgEquiv.aut _)) s →
    ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
mpr :
  (∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s) →
    Membership.mem (γ := Filter Gal(L/K)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ AlgEquiv.aut _)) s
⊢ Membership.mem (γ := Filter Gal(L/K)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ AlgEquiv.aut _)) s ↔
    ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
constructor
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Set Gal(L/K)
E : IntermediateField K L
fin : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
hE : (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E.fixingSubgroup ⊆ s
⊢ ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
⟨E, fin, hE⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Set Gal(L/K)
E : IntermediateField K L
fin : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E
hE : (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E.fixingSubgroup ⊆ s
⊢ ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
exact ⟨E, fin, hE⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Set Gal(L/K)
E : IntermediateField K L
fin : FiniteDimensional.{u_1, u_2} K ↥E
hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ Membership.mem (γ := Filter Gal(L/K)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ AlgEquiv.aut _)) s

Tactic:
⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩

Premises used: Set.Mem, setOf, IntermediateField.fixingSubgroup, SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Set Gal(L/K)
E : IntermediateField K L
fin : FiniteDimensional.{u_1, u_2} K ↥E
hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ Membership.mem (γ := Filter Gal(L/K)) (FilterBasis.filter (@GroupFilterBasis.toFilterBasis _ AlgEquiv.aut _)) s

Tactic:
exact ⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
rw :
  (∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s) ↔
    ∃ (E : IntermediateField K L),
      FiniteDimensional.{u_1, u_2} K ↥E ∧ Normal.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) s ↔
    ∃ (E : IntermediateField K L),
      FiniteDimensional.{u_1, u_2} K ↥E ∧ Normal.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
rw [krullTopology_mem_nhds_one_iff]

Premises used: krullTopology_mem_nhds_one_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
⊢ (∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s) ↔
    ∃ (E : IntermediateField K L),
      FiniteDimensional.{u_1, u_2} K ↥E ∧ Normal.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩

Premises used: _private.0.krullTopology_mem_nhds_one_iff_of_normal.match_2, Normal, Membership.mem, Exists, IntermediateField.fixingSubgroup, Subtype, HasSubset.Subset, And, FiniteDimensional, SetLike.coe, And.right, And.left, And.intro, Iff.intro, Exists.intro, _private.0.krullTopology_mem_nhds_one_iff_of_normal.match_1
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
refine :
  (∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s) →
    ∀ (E : IntermediateField K L),
      FiniteDimensional.{u_1, u_2} K ↥E →
        ∀ (hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s),
          ∃ (E : IntermediateField K L),
            FiniteDimensional.{u_1, u_2} K ↥E ∧ Normal.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ (∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s) ↔
    ∃ (E : IntermediateField K L),
      FiniteDimensional.{u_1, u_2} K ↥E ∧ Normal.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
h_1 : ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
E : IntermediateField K L
left : FiniteDimensional.{u_1, u_2} K ↥E
hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
h :
  FiniteDimensional.{u_1, u_2} K ↥(IntermediateField.normalClosure K (↥E) L) ∧
    Normal.{u_1, u_2} K ↥(IntermediateField.normalClosure K (↥E) L) ∧
      (↑(IntermediateField.fixingSubgroup (IntermediateField.normalClosure K (↥E) L)) : Set Gal(L/K)) ⊆ s
⊢ ∃ (E : IntermediateField K L),
    FiniteDimensional.{u_1, u_2} K ↥E ∧ Normal.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s

Tactic:
use (IntermediateField.normalClosure K E L)

Premises used: IntermediateField.normalClosure, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
h_1 : ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
E : IntermediateField K L
left : FiniteDimensional.{u_1, u_2} K ↥E
hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
h : (↑(IntermediateField.fixingSubgroup (IntermediateField.normalClosure K (↥E) L)) : Set Gal(L/K)) ⊆ s
⊢ FiniteDimensional.{u_1, u_2} K ↥(IntermediateField.normalClosure K (↥E) L) ∧
    Normal.{u_1, u_2} K ↥(IntermediateField.normalClosure K (↥E) L) ∧
      (↑(IntermediateField.fixingSubgroup (IntermediateField.normalClosure K (↥E) L)) : Set Gal(L/K)) ⊆ s

Tactic:
simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and]

Premises used: Membership.mem, Subtype, normalClosure.normal, normalClosure.is_finiteDimensional, true_and
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
h : ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
E : IntermediateField K L
left : FiniteDimensional.{u_1, u_2} K ↥E
hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ (↑(IntermediateField.fixingSubgroup (IntermediateField.normalClosure K (↥E) L)) : Set Gal(L/K)) ⊆ s

Tactic:
le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE

Premises used: IntermediateField.fixingSubgroup_antitone, IntermediateField.le_normalClosure, le_trans
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
s : Set Gal(L/K)
h : ∃ (E : IntermediateField K L), FiniteDimensional.{u_1, u_2} K ↥E ∧ (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
E : IntermediateField K L
left : FiniteDimensional.{u_1, u_2} K ↥E
hE : (↑E.fixingSubgroup : Set Gal(L/K)) ⊆ s
⊢ (↑(IntermediateField.fixingSubgroup (IntermediateField.normalClosure K (↥E) L)) : Set Gal(L/K)) ⊆ s

Tactic:
exact le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE

Premises used: IntermediateField.fixingSubgroup_antitone, IntermediateField.le_normalClosure, le_trans
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
⊢ Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) E.fixingSubgroup.carrier

Tactic:
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L :=
    ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) E.fixingSubgroup.carrier
⊢ Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) E.fixingSubgroup.carrier

Tactic:
have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) E.fixingSubgroup.carrier
h_nhds : Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) E.fixingSubgroup.carrier
⊢ IsOpen (↑E.fixingSubgroup : Set Gal(L/K))

Tactic:
Subgroup.isOpen_of_mem_nhds _ h_nhds

Premises used: Subgroup.isOpen_of_mem_nhds
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) E.fixingSubgroup.carrier
h_nhds : Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) E.fixingSubgroup.carrier
⊢ IsOpen (↑E.fixingSubgroup : Set Gal(L/K))

Tactic:
exact Subgroup.isOpen_of_mem_nhds _ h_nhds

Premises used: Subgroup.isOpen_of_mem_nhds