-- 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 Γ₀
a b : ValueGroup₀ (F := Valuation K Γ₀) v
x : K :=
  Exists.choose (p := fun (a_1 : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        a_1 =
      a)
    ⋯
hx_def :
  x =
    Exists.choose (p := fun (a_1 : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a_1 =
        a)
      ⋯
hx :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x = a
y : K :=
  Exists.choose (p := fun (a : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) a =
      b)
    ⋯
hy_def :
  y =
    Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        b)
      ⋯
hy :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y = b
xy : K :=
  Exists.choose (p := fun (a_1 : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        a_1 =
      a * b)
    ⋯
hxy_def :
  xy =
    Exists.choose (p := fun (a_1 : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a_1 =
        a * b)
      ⋯
hxy :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) xy =
    a * b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
          Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
          (Units.mk0 ((v : (a : K) → Γ₀) xy) ⋯) ⋯) :
      WithZero ↥(valueGroup extensionValuation)) =
    HMul.hMul (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) (β :=
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
                x)
              (Units.mk0 ((v : (a : K) → Γ₀) x) ⋯) ⋯) :
          WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
                x)
              (Units.mk0 ((v : (a : K) → Γ₀) y) ⋯) ⋯) :
          WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation))
have neg : Units.mk0 ((v : (a : K) → Γ₀) xy) sorry =
  HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) sorry : Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) y) sorry : Γ₀ˣ)
Tactic: simp only [← WithZero.coe_mul, MulMemClass.mk_mul_mk, WithZero.coe_inj, Subtype.mk.injEq]