-- 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}
⊢ 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)
have h : ∀
  (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
Tactic: ext x