-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
x y : Gal(K/k)
⊢ Subtype.mk (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)
      (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
        (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
            (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
          (x * y))
      ⋯ =
    HMul.hMul (α :=
      (↑((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.mk (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)
        (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
          (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
              (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
            x)
        ⋯)
      (Subtype.mk (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)
        (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
          (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
              (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
            y)
        ⋯)
have simp : Subtype.mk (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)
    (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
      HMul.hMul (α := Gal(↥(unop L).toIntermediateField/k)) (β := Gal(↥(unop L).toIntermediateField/k))
        ((AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
              (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
            x :
          Gal(↥(unop L).toIntermediateField/k))
        ((AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
              (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
            y :
          Gal(↥(unop L).toIntermediateField/k)))
    sorry =
  HMul.hMul (α := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
    (Subtype.mk (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)
      (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
        (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
            (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
          x)
      sorry)
    (Subtype.mk (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)
      (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
        (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
            (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
          y)
      sorry)
Tactic: simp only [map_mul]