-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
pos :
  ∀ (hb : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)),
    Eq (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                  Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) ⋯) ⋯) :
              WithZero ↥(valueGroup Valued.v))) :
        WithZero ↥(valueGroup v))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ v)
neg :
  ∀ (hb : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)),
    Eq (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                  Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) ⋯) ⋯) :
              WithZero ↥(valueGroup Valued.v))) :
        WithZero ↥(valueGroup v))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ v)
⊢ Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)

Tactic:
by_cases hb : v b.ofVal = 0

Premises used: WithVal.ofVal, DFunLike.coe