-- 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}
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)
h :
  ∀ (σ : Gal(K/k)),
    Membership.mem (α :=
        (↑((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))
        (γ :=
        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)))
        ((mulEquivToLimit k K :
              (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
            σ :
          (↑((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)) ↔
      Membership.mem (α :=
        (↑((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))
        (γ :=
        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))
        (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)
        ((mulEquivToLimit k K :
              (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
            σ :
          (↑((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))
⊢ Membership.mem (γ :=
      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)))
      x ↔
    Membership.mem (γ :=
      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))
      (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)
      x

Tactic:
obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x

Premises used: MulEquiv.surjective, rfl, InfiniteGalois.mulEquivToLimit