-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hs : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀)
pf : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf_1 : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf_2 :
  ∀
    (d :
      { xy : R × R //
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑d : R × R).1 : Γ₀) (0 : Γ₀)
pf_3 :
  ∀
    (d :
      { xy : R × R //
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑d : R × R).2 : Γ₀) (0 : Γ₀)
H :
  ∃ (d :
    { xy : R × R //
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
      (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v))
pf_4 :
  ∀
    (c :
      { xy : R × R //
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) (↑c : R × R).1 : Γ'₀) (0 : Γ'₀)
pf_5 :
  ∀
    (c :
      { xy : R × R //
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) (↑c : R × R).2 : Γ'₀) (0 : Γ'₀)
pf_6 : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
pf_7 : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) s : Γ'₀) (0 : Γ'₀)
c_spec :
  Eq.{u_4 + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (r *
          (↑(Exists.choose (p :=
                  fun
                    (d :
                      { xy : R × R //
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (r * (↑d : R × R).2) : Γ₀)
                    ((v : (a : R) → Γ₀) ((↑d : R × R).1 * s) : Γ₀))
                  ⋯) :
              R × R).2) :
      Γ₀)
    ((v : (a : R) → Γ₀)
        ((↑(Exists.choose (p :=
                  fun
                    (d :
                      { xy : R × R //
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (r * (↑d : R × R).2) : Γ₀)
                    ((v : (a : R) → Γ₀) ((↑d : R × R).1 * s) : Γ₀))
                  ⋯) :
              R × R).1 *
          s) :
      Γ₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀)
    ((w : (a : R) → Γ'₀)
        ((↑(Exists.choose (p :=
                  fun
                    (d :
                      { xy : R × R //
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (r * (↑d : R × R).2) : Γ₀)
                    ((v : (a : R) → Γ₀) ((↑d : R × R).1 * s) : Γ₀))
                  ⋯) :
              R × R).1 *
          s) :
      Γ'₀)
    ((w : (a : R) → Γ'₀)
        (r *
          (↑(Exists.choose (p :=
                  fun
                    (d :
                      { xy : R × R //
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (r * (↑d : R × R).2) : Γ₀)
                    ((v : (a : R) → Γ₀) ((↑d : R × R).1 * s) : Γ₀))
                  ⋯) :
              R × R).2) :
      Γ'₀)
have rwa : Eq.{u_4 + 1} (α := Γ₀)
  ((v : (a : R) → Γ₀)
      ((↑(Exists.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (r * (↑d : R × R).2) : Γ₀)
                  ((v : (a : R) → Γ₀) ((↑d : R × R).1 * s) : Γ₀))
                sorry) :
            R × R).1 *
        s) :
    Γ₀)
  ((v : (a : R) → Γ₀)
      (r *
        (↑(Exists.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (r * (↑d : R × R).2) : Γ₀)
                  ((v : (a : R) → Γ₀) ((↑d : R × R).1 * s) : Γ₀))
                sorry) :
            R × R).2) :
    Γ₀)
Tactic: rwa [← h.eq_iff, eq_comm]