-- Module: Mathlib.RingTheory.Valuation.Basic
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 (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
    (↑(valueGroup.mk v
          (↑(H.choose (p :=
                  fun
                    (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)))) :
              R × R).1
          (↑(H.choose (p :=
                  fun
                    (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)))) :
              R × R).2
          ⋯ ⋯) :
      WithZero ↥(valueGroup v))
simp :
  ∀
    (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) :
        Γ'₀)
⊢ Eq (α := ValueGroup₀ w)
    (have c :=
      H.choose (p :=
        fun
          (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)));
    (↑(valueGroup.mk w (↑c : R × R).1 (↑c : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup w)))
    (↑(valueGroup.mk w r s pf_6 pf_7) : WithZero ↥(valueGroup w))

Tactic:
simp only [ne_eq, WithZero.coe_inj, valueGroup.mk_inj] at c_spec ⊢

Premises used: WithZero.coe_inj, MonoidWithZeroHom.valueGroup.mk_inj, ne_eq