-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
x : hat K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
pos :
  ∀ (hx0 : x = 0),
    LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                  Membership.mem (γ := Subgroup Γ₀ˣ)
                    (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                  (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) x) h) ⋯) :
              WithZero ↥(valueGroup extensionValuation)) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
        ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
            (↑γ : ValueGroup₀ v) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
      extension x < (↑γ : ValueGroup₀ v)
⊢ LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ)
                  (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) x) h) ⋯) :
            WithZero ↥(valueGroup extensionValuation)) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension x < (↑γ : ValueGroup₀ v)
have neg : ∀ (hx0 : ¬x = 0),
  LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ)
                  (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) x) h) sorry) :
            WithZero ↥(valueGroup extensionValuation)) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension x < (↑γ : ValueGroup₀ v)
Tactic: by_cases hx0 : x = 0