-- Module: Mathlib.RingTheory.Valuation.Basic
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
pos : ∀ (hx0 : x = 0) (hy0 : y = 0), LE.le.{u_5} (α := ValueGroup₀ w) 0 0 ↔ x ≤ y
neg :
  ∀ (hx0 : x = 0) (hy0 : ¬y = 0),
    LE.le (α := ValueGroup₀ w) 0
        (↑(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
pos₁ :
  ∀ (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))
        0 ↔
      x ≤ y
neg₁ :
  ∀ (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
⊢ LE.le.{u_5} (α := ValueGroup₀ w)
      (if h : x = 0 then 0
      else
        (↑(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)))
      (if h : y = 0 then 0
      else
        (↑(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

Tactic:
split_ifs with hx0 hy0 hy0