-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : ↥(adicCompletionIntegers K v)
⊢ HMul.hMul (α := ↥(adicCompletionIntegers K v))
      (({
              toFun := fun (r : R) ↦
                Subtype.mk (p := fun (x : adicCompletion K v) ↦
                  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                  (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                        ((algebraMap R K : (a : R) → K) r)) :
                    UniformSpace.Completion (WithVal (valuation K v)))
                  ⋯,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
              RingHom.{u_1, u_2} R ↥(adicCompletionIntegers K v) } :
            (a : R) → ↥(adicCompletionIntegers K v))
          r :
        ↥(adicCompletionIntegers K v))
      x =
    HMul.hMul (β := ↥(adicCompletionIntegers K v)) x
      (({
              toFun := fun (r : R) ↦
                Subtype.mk (p := fun (x : adicCompletion K v) ↦
                  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                  (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                        ((algebraMap R K : (a : R) → K) r)) :
                    UniformSpace.Completion (WithVal (valuation K v)))
                  ⋯,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R) → ↥(adicCompletionIntegers K v))
          r :
        ↥(adicCompletionIntegers K v))
have rw : HMul.hMul (β := ↥(adicCompletionIntegers K v)) x
    (({
            toFun := fun (r : R) ↦
              Subtype.mk (p := fun (x : adicCompletion K v) ↦
                Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                      ((algebraMap R K : (a : R) → K) r)) :
                  UniformSpace.Completion (WithVal (valuation K v)))
                sorry,
            map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
            RingHom.{u_1, u_2} R ↥(adicCompletionIntegers K v) } :
          (a : R) → ↥(adicCompletionIntegers K v))
        r :
      ↥(adicCompletionIntegers K v)) =
  HMul.hMul (β := ↥(adicCompletionIntegers K v)) x
    (({
            toFun := fun (r : R) ↦
              Subtype.mk (p := fun (x : adicCompletion K v) ↦
                Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                      ((algebraMap R K : (a : R) → K) r)) :
                  UniformSpace.Completion (WithVal (valuation K v)))
                sorry,
            map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry } :
          (a : R) → ↥(adicCompletionIntegers K v))
        r :
      ↥(adicCompletionIntegers K v))
Tactic: rw [mul_comm]