awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
inst_6 : IsGalois k K
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
⊢ Eq (α := K)
    ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
    ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)

Tactic:
exact AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x

Premises used: Membership.mem, Subtype, AlgEquiv.restrictNormal_commutes, FiniteGaloisIntermediateField.toIntermediateField, InfiniteGalois.limitToAlgEquiv, Opposite.unop
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
inst_6 : IsGalois k K
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
⊢ Eq (α := K)
    ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
    ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)

Tactic:
have : ((limitToAlgEquiv g).restrictNormal L.unop) x = (limitToAlgEquiv g) x.1 := by
      exact AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
inst_6 : IsGalois k K
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
this :
  Eq (α := K)
    ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
    ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
a :
  Eq (α := K) ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
    ((↑(((↑g :
                  (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                    (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
                L :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
⊢ Eq.{u_4 + 1} (α := K)
    (↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K)
    (↑(((↑g :
                (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                  (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
              L :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K)

Tactic:
simp_rw [this]
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
inst_6 : IsGalois k K
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
this :
  Eq (α := K)
    ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
    ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
⊢ Eq (α := K) ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
    ((↑(((↑g :
                  (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                    (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
                L :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)

Tactic:
proj_adjoin_singleton_val _ _ _ _ x.2

Premises used: InfiniteGalois.proj_adjoin_singleton_val, _private.0.InfiniteGalois.toAlgEquivAux, Subtype.property
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
inst_6 : IsGalois k K
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
this :
  Eq (α := K)
    ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
    ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
⊢ Eq (α := K) ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
    ((↑(((↑g :
                  (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                    (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
                L :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)

Tactic:
exact proj_adjoin_singleton_val _ _ _ _ x.2

Premises used: InfiniteGalois.proj_adjoin_singleton_val, Subtype.property
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
A : Set Gal(K/k)
rw :
  (∃ (E : IntermediateField k K),
      FiniteDimensional.{u_3, u_4} k ↥E ∧ Normal.{u_3, u_4} k ↥E ∧ (↑E.fixingSubgroup : Set Gal(K/k)) ⊆ A) ↔
    ∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A
⊢ Membership.mem (γ := Filter Gal(K/k)) (𝓝 1) A ↔
    ∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A

Tactic:
rw [krullTopology_mem_nhds_one_iff_of_normal]

Premises used: krullTopology_mem_nhds_one_iff_of_normal
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
A : Set Gal(K/k)
⊢ (∃ (E : IntermediateField k K),
      FiniteDimensional.{u_3, u_4} k ↥E ∧ Normal.{u_3, u_4} k ↥E ∧ (↑E.fixingSubgroup : Set Gal(K/k)) ⊆ A) ↔
    ∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A

Tactic:
⟨fun ⟨L, _, hL, hsub⟩ ↦ ⟨{ toIntermediateField := L, isGalois := ⟨⟩ }, hsub⟩,
    fun ⟨L, hL⟩ ↦ ⟨L, inferInstance, inferInstance, hL⟩⟩

Premises used: Normal, Membership.mem, Exists, inferInstance, IntermediateField.fixingSubgroup, Subtype, HasSubset.Subset, _private.0.InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois.match_1, And, FiniteDimensional, SetLike.coe, And.intro, Iff.intro, Exists.intro, _private.0.InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois.match_2, FiniteGaloisIntermediateField.toIntermediateField, FiniteGaloisIntermediateField.mk
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
A : Set Gal(K/k)
⊢ (∃ (E : IntermediateField k K),
      FiniteDimensional.{u_3, u_4} k ↥E ∧ Normal.{u_3, u_4} k ↥E ∧ (↑E.fixingSubgroup : Set Gal(K/k)) ⊆ A) ↔
    ∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A

Tactic:
exact ⟨fun ⟨L, _, hL, hsub⟩ ↦ ⟨{ toIntermediateField := L, isGalois := ⟨⟩ }, hsub⟩,
    fun ⟨L, hL⟩ ↦ ⟨L, inferInstance, inferInstance, hL⟩⟩
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
    (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4)) :=
  {f :
    (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4) |
    Eq.{u_4 + 1} (α :=
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) (op L)).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
      (f (op L)) 1}
this :
  Eq (α :=
    Set
      (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
            (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
    ((⇑(mulEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
      (↑L.fixingSubgroup : Set Gal(K/k)))
    (Subtype.val (p :=
        fun
          (x :
            (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)) ↦
        Membership.mem (γ :=
          Subgroup
            ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)))
          (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x) ⁻¹'
      fix1)
⊢ IsOpen (X :=
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    (Subtype.val (p :=
        fun
          (x :
            (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)) ↦
        Membership.mem (γ :=
          Subgroup
            ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)))
          (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x) ⁻¹'
      fix1)

Tactic:
exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
    (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4)) :=
  {f :
    (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4) |
    Eq.{u_4 + 1} (α :=
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) (op L)).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
      (f (op L)) 1}
suffices :
  Eq (α :=
    Set
      (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
            (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
    ((⇑(mulEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
      (↑L.fixingSubgroup : Set Gal(K/k)))
    (Subtype.val (p :=
        fun
          (x :
            (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)) ↦
        Membership.mem (γ :=
          Subgroup
            ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)))
          (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x) ⁻¹'
      fix1)
⊢ IsOpen (X :=
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    ((⇑(mulEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
      (↑L.fixingSubgroup : Set Gal(K/k)))

Tactic:
suffices mulEquivToLimit k K '' L.1.fixingSubgroup = Set.preimage Subtype.val fix1 by
    rw [this]
    exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
apply :
  ∀ (A : Set Gal(K/k)),
    Membership.mem (γ := Filter Gal(K/k))
        (nhds
            ((MulEquiv.symm (mulEquivToLimit k K) :
                (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k))
              1) :
          Filter Gal(K/k))
        A →
      Membership.mem (γ :=
        Filter
          (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
                (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
            Type u_4))
        (nhds 1)
        ((⇑(MulEquiv.symm (mulEquivToLimit k K)) :
            (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k)) ⁻¹'
          A)
⊢ Continuous (X :=
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    (Y := Gal(K/k))
    (⇑(MulEquiv.symm (mulEquivToLimit k K)) :
      (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k))

Tactic:
apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _)

Premises used: Iff.mpr, continuous_of_continuousAt_one, continuousAt_def
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
simp :
  ∀ (A : Set Gal(K/k)),
    (∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A) →
      Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
        ((fun (a : Gal(K/k)) ↦
            (MulEquiv.toEquiv (mulEquivToLimit k K) :
                (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
              a) ''
          A)
⊢ ∀ (A : Set Gal(K/k)),
    Membership.mem (γ := Filter Gal(K/k))
        (nhds
            ((MulEquiv.symm (mulEquivToLimit k K) :
                (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k))
              1) :
          Filter Gal(K/k))
        A →
      Membership.mem (γ :=
        Filter
          (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
                (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
            Type u_4))
        (nhds 1)
        ((⇑(MulEquiv.symm (mulEquivToLimit k K)) :
            (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k)) ⁻¹'
          A)

Tactic:
simp only [map_one, krullTopology_mem_nhds_one_iff_of_isGalois, ← MulEquiv.coe_toEquiv_symm,
    ← MulEquiv.toEquiv_eq_coe, ← (mulEquivToLimit k K).image_eq_preimage_symm]

Premises used: InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois, MulEquiv.toEquiv, MulEquiv.toEquiv_eq_coe, Equiv.image_eq_preimage_symm, map_one, MulEquiv.coe_toEquiv_symm, InfiniteGalois.mulEquivToLimit
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
H : Set Gal(K/k)
this :
  ∀ (L : FiniteGaloisIntermediateField k K) (le : (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H),
    Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H)
⊢ (∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H) →
    Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H)

Tactic:
⟨L, le⟩
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H
rw :
  ∃
    t ⊆
      (fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H,
    IsOpen t ∧ 1 ∈ t
⊢ Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
    ((fun (a : Gal(K/k)) ↦
        (MulEquiv.toEquiv (mulEquivToLimit k K) :
            (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
          a) ''
      H)

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H
h :
  Subset (α := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
      ((⇑(mulEquivToLimit k K) :
          (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
        (↑L.fixingSubgroup : Set Gal(K/k)))
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H) ∧
    IsOpen (X := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((⇑(mulEquivToLimit k K) :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
          (↑L.fixingSubgroup : Set Gal(K/k))) ∧
      Membership.mem (γ := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((⇑(mulEquivToLimit k K) :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
          (↑L.fixingSubgroup : Set Gal(K/k)))
        1
⊢ ∃
    t ⊆
      (fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H,
    IsOpen t ∧ 1 ∈ t

Tactic:
use mulEquivToLimit k K '' L.1.fixingSubgroup

Premises used: IntermediateField.fixingSubgroup, FiniteGaloisIntermediateField.toIntermediateField, InfiniteGalois.mulEquivToLimit
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H
h :
  Subset (α := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
      ((fun (a : Gal(K/k)) ↦
          (mulEquivToLimit k K : (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) a) ''
        (↑L.fixingSubgroup : Set Gal(K/k)))
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H) ∧
    True ∧
      Membership.mem (γ := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((fun (a : Gal(K/k)) ↦
            (mulEquivToLimit k K : (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) a) ''
          (↑L.fixingSubgroup : Set Gal(K/k)))
        1
⊢ Subset (α := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
      ((⇑(mulEquivToLimit k K) :
          (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
        (↑L.fixingSubgroup : Set Gal(K/k)))
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H) ∧
    IsOpen (X := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((⇑(mulEquivToLimit k K) :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
          (↑L.fixingSubgroup : Set Gal(K/k))) ∧
      Membership.mem (γ := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((⇑(mulEquivToLimit k K) :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
          (↑L.fixingSubgroup : Set Gal(K/k)))
        1

Tactic:
simp only [isOpen_mulEquivToLimit_image_fixingSubgroup L]

Premises used: InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup