-- 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
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    (if h :
        Eq.{u_2 + 1} (α := Γ₀)
          ((extensionValuation : (a : hat K) → Γ₀)
              (↑(Exists.choose (p := fun (a_1 : K) ↦
                    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a_1 : Γ₀) (0 : Γ₀) then 0
                      else
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                              (Units.mk0 ((v : (a : K) → Γ₀) a_1) h) ⋯) :
                          WithZero ↥(valueGroup v))) =
                      a * b)
                    ⋯) :
                hat K) :
            Γ₀)
          (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
              ((v : (a : K) → Γ₀)
                (Exists.choose (p := fun (a_1 : K) ↦
                  (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a_1 : Γ₀) (0 : Γ₀) then 0
                    else
                      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                            Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                            (Units.mk0 ((v : (a : K) → Γ₀) a_1) h) ⋯) :
                        WithZero ↥(valueGroup v))) =
                    a * b)
                  ⋯))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup extensionValuation)))
    (if h :
        Eq.{u_2 + 1} (α := Γ₀)
          ((extensionValuation : (a : hat K) → Γ₀)
              (↑(Exists.choose (p := fun (a : K) ↦
                    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a : Γ₀) (0 : Γ₀) then 0
                      else
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                              (Units.mk0 ((v : (a : K) → Γ₀) a) h) ⋯) :
                          WithZero ↥(valueGroup v))) =
                      b)
                    ⋯) :
                hat K) :
            Γ₀)
          (0 : Γ₀) then
      0
    else
      if h :
          Eq.{u_2 + 1} (α := Γ₀)
            ((extensionValuation : (a : hat K) → Γ₀)
                (↑(Exists.choose (p := fun (a_1 : K) ↦
                      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a_1 : Γ₀) (0 : Γ₀) then 0
                        else
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                                Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                                (Units.mk0 ((v : (a : K) → Γ₀) a_1) h) ⋯) :
                            WithZero ↥(valueGroup v))) =
                        a)
                      ⋯) :
                  hat K) :
              Γ₀)
            (0 : Γ₀) then
        0
      else
        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) → Γ₀)
                      (Exists.choose (p := fun (a_1 : K) ↦
                        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a_1 : Γ₀) (0 : Γ₀) then 0
                          else
                            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                                  Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                                  (Units.mk0 ((v : (a : K) → Γ₀) a_1) h) ⋯) :
                              WithZero ↥(valueGroup v))) =
                          a)
                        ⋯))
                    ⋯)
                  ⋯) :
              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) → Γ₀)
                      (Exists.choose (p := fun (a : K) ↦
                        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a : Γ₀) (0 : Γ₀) then 0
                          else
                            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                                  Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                                  (Units.mk0 ((v : (a : K) → Γ₀) a) h) ⋯) :
                              WithZero ↥(valueGroup v))) =
                          b)
                        ⋯))
                    ⋯)
                  ⋯) :
              WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
            WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)))
have set : let 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)
    sorry;
∀
  (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)
        sorry),
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    (if h :
        Eq.{u_2 + 1} (α := Γ₀)
          ((extensionValuation : (a : hat K) → Γ₀)
              (↑(Exists.choose (p := fun (a_1 : K) ↦
                    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a_1 : Γ₀) (0 : Γ₀) then 0
                      else
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                              (Units.mk0 ((v : (a : K) → Γ₀) a_1) h) sorry) :
                          WithZero ↥(valueGroup v))) =
                      a * b)
                    sorry) :
                hat K) :
            Γ₀)
          (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
              ((v : (a : K) → Γ₀)
                (Exists.choose (p := fun (a_1 : K) ↦
                  (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a_1 : Γ₀) (0 : Γ₀) then 0
                    else
                      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                            Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                            (Units.mk0 ((v : (a : K) → Γ₀) a_1) h) sorry) :
                        WithZero ↥(valueGroup v))) =
                    a * b)
                  sorry))
              sorry)
            sorry) :
        WithZero ↥(valueGroup extensionValuation)))
    (if h :
        Eq.{u_2 + 1} (α := Γ₀)
          ((extensionValuation : (a : hat K) → Γ₀)
              (↑(Exists.choose (p := fun (a : K) ↦
                    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a : Γ₀) (0 : Γ₀) then 0
                      else
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                              (Units.mk0 ((v : (a : K) → Γ₀) a) h) sorry) :
                          WithZero ↥(valueGroup v))) =
                      b)
                    sorry) :
                hat K) :
            Γ₀)
          (0 : Γ₀) then
      0
    else
      if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) (0 : Γ₀) then 0
      else
        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) sorry) sorry) :
              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) → Γ₀)
                      (Exists.choose (p := fun (a : K) ↦
                        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) a : Γ₀) (0 : Γ₀) then 0
                          else
                            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                                  Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                                  (Units.mk0 ((v : (a : K) → Γ₀) a) h) sorry) :
                              WithZero ↥(valueGroup v))) =
                          b)
                        sorry))
                    sorry)
                  sorry) :
              WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
            WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)))
Tactic: set x := (restrict₀_surjective hv.v a).choose with hx_def