-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ LE.le (α := ValueGroup₀ w)
      (↑(valueGroup.mk w
            (↑(⋯.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 : Γ₀) }) ↦
                    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(⋯.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 : Γ₀) }) ↦
                    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).2
            ⋯ ⋯) :
        WithZero ↥(valueGroup w))
      (↑(valueGroup.mk w
            (↑(⋯.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 : Γ₀) }) ↦
                    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(⋯.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 : Γ₀) }) ↦
                    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).2
            ⋯ ⋯) :
        WithZero ↥(valueGroup w)) ↔
    x ≤ y
have neg : ∀ (pf : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀) (pf_1 : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀)
  (pf_2 :
    ∀
      (d :
        { xy : R × R //
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
            ¬Eq.{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 //
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑d : R × R).2 : Γ₀) (0 : Γ₀))
  (hx :
    ∃ (d :
      { xy : R × R //
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))
  (pf_4 :
    Ne.{u_5 + 1} (α := Γ'₀)
      ((w : (a : R) → Γ'₀)
          (↑(hx.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 : Γ₀) }) ↦
                  x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
              R × R).1 :
        Γ'₀)
      (0 : Γ'₀))
  (pf_5 :
    Ne.{u_5 + 1} (α := Γ'₀)
      ((w : (a : R) → Γ'₀)
          (↑(hx.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 : Γ₀) }) ↦
                  x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
              R × R).2 :
        Γ'₀)
      (0 : Γ'₀))
  (hy :
    ∃ (d :
      { xy : R × R //
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))
  (pf_6 :
    Ne.{u_5 + 1} (α := Γ'₀)
      ((w : (a : R) → Γ'₀)
          (↑(hy.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 : Γ₀) }) ↦
                  y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
              R × R).1 :
        Γ'₀)
      (0 : Γ'₀))
  (pf_7 :
    Ne.{u_5 + 1} (α := Γ'₀)
      ((w : (a : R) → Γ'₀)
          (↑(hy.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 : Γ₀) }) ↦
                  y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
              R × R).2 :
        Γ'₀)
      (0 : Γ'₀)),
  LE.le (α := ValueGroup₀ w)
      (↑(valueGroup.mk w
            (↑(hx.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 : Γ₀) }) ↦
                    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(hx.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 : Γ₀) }) ↦
                    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).2
            pf_4 pf_5) :
        WithZero ↥(valueGroup w))
      (↑(valueGroup.mk w
            (↑(hy.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 : Γ₀) }) ↦
                    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(hy.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 : Γ₀) }) ↦
                    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).2
            pf_6 pf_7) :
        WithZero ↥(valueGroup w)) ↔
    x ≤ y
Tactic: generalize_proofs _ _ _ _ hx _ _ hy