-- 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 : Γ'₀)
⊢ 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))

Tactic:
have c_spec := H.choose_spec