-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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)
⊢ 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
have 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))
Tactic: obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x
Cleared hypotheses: x