-- 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
⊢ (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat 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)
            ⋯) :
        hat K) =
    HMul.hMul (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) (β :=
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat 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)
                ⋯) :
            hat K) :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat 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)
                ⋯) :
            hat K) :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
have simp : 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) → Γ₀)
              (↑(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)
                    sorry) :
                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) sorry) :
                            WithZero ↥(valueGroup v))) =
                        a)
                      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))
        ((↑(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: simp only [restrict₀_apply, map_eq_zero, Valuation.restrict_def, extensionValuation_apply_coe,
      mul_dite, mul_zero, dite_mul, zero_mul]