-- 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 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
pos :
  ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (_ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      (max
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
            WithZero ↥(valueGroup v))
          0 :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
neg :
  ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (_ : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      (max
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
            WithZero ↥(valueGroup v))
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) _) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
pos₁ :
  ∀ (H : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) H) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      (max
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
            WithZero ↥(valueGroup v))
          0 :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
neg₁ :
  ∀ (H : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) H) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      (max
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
            WithZero ↥(valueGroup v))
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
          WithZero ↥(valueGroup v))
        (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
split_ifs with H _ hy