-- 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
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)
⊢ toAlgEquivAux g (x * y) = toAlgEquivAux g x * toAlgEquivAux g y
have 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)
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]