-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : R
pos :
  ∀ (hb : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀)),
    Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
      ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
            (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) b) h) ⋯) :
              WithZero ↥(valueGroup v))) :
        WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (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) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v)) :
        ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
⊢ Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
          (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (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) ⋯) ⋯) :
          WithZero ↥(valueGroup Valued.v)) :
      ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
have neg : ∀ (hb : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀)),
  Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
          (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b) h) sorry) :
            WithZero ↥(valueGroup v))) :
      WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (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) sorry) sorry) :
          WithZero ↥(valueGroup Valued.v)) :
      ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
Tactic: by_cases hb : v b = 0