-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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)
rw 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)))
                  ⋯,
              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)) =
    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))
⊢ 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))

Tactic:
rw [mul_comm]

Premises used: mul_comm