-- 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
x y : Gal(K/k)
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)))
      ⋯ =
    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)
        ⋯)
      (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)
        ⋯)
⊢ 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)
        ⋯)

Tactic:
simp only [map_mul]

Premises used: map_mul