-- 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
inst_6 : IsGalois k K
g :
  (↑((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)
x y : K
hx : Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) x
hy : Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) y
rw :
  toAlgEquivAux g (x * y) =
    HMul.hMul (α := K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          x :
        K)
      (toAlgEquivAux g y)
rw₁ :
  toAlgEquivAux g (x * y) =
    HMul.hMul (α := K) (β := K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          x :
        K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          y :
        K)
rw₂ :
  (AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ := ↥(toIntermediateField (adjoin k {x, y})))
          ((proj (adjoin k {x, y}) :
              (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                Gal(↥(adjoin k {x, y}).toIntermediateField/k))
            g)
          K :
        (a : K) → K)
      (x * y) =
    HMul.hMul (α := K) (β := K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          x :
        K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          y :
        K)
rw₃ rw₄ :
  HMul.hMul (α := K) (β := K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          x :
        K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          y :
        K) =
    HMul.hMul (α := K) (β := K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          x :
        K)
      ((AlgEquiv.liftNormal (K₁ := ↥(toIntermediateField (adjoin k {x, y}))) (K₂ :=
              ↥(toIntermediateField (adjoin k {x, y})))
              ((proj (adjoin k {x, y}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x, y}).toIntermediateField/k))
                g)
              K :
            (a : K) → K)
          y :
        K)
⊢ toAlgEquivAux g (x * y) = toAlgEquivAux g x * toAlgEquivAux g y

Tactic:
rw [toAlgEquivAux_eq_liftNormal g x (adjoin k {x, y}) hx,
      toAlgEquivAux_eq_liftNormal g y (adjoin k {x, y}) hy,
      toAlgEquivAux_eq_liftNormal g (x * y) (adjoin k {x, y}) (mul_mem hx hy), map_mul]

Premises used: HMul.hMul, Insert.insert, map_mul, InfiniteGalois.toAlgEquivAux_eq_liftNormal, FiniteGaloisIntermediateField.adjoin, Singleton.singleton, MulMemClass.mul_mem