-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : ValueGroup₀ (F := Valuation K Γ₀) v
hab :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
        (↑(⋯.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 →*₀ Γ₀))
        (↑(⋯.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 →*₀ Γ₀))
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)
    (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)
      ⋯) =
  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)
    (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)
      ⋯) =
  b :=
  ⋯
ha0 : a = 0
h0 : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0
this : y = 0
pos :
  ∀ (hy : 0 = b) (ha0 : a = 0)
    (h0 : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0)
    (this : y = 0), a = b
pos₁ :
  ∀
    (hy :
      (if h :
            Eq.{u_2 + 1} (α := Γ₀)
              ((v : (a : 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)
                    ⋯) :
                Γ₀)
              (0 : Γ₀) then
          0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation K Γ₀) v) x)
                (Units.mk0
                  ((v : (a : 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)
                      ⋯))
                  h)
                ⋯) :
            WithZero ↥(valueGroup v))) =
        b)
    (ha0 : a = 0)
    (h0 : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0)
    (this : y = 0),
    Eq.{u_2 + 1} (α := Γ₀)
      ((v : (a : 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)
            ⋯) :
        Γ₀)
      (0 : Γ₀)
⊢ a = b

Tactic:
rw [restrict₀_apply, dif_pos] at hy

Premises used: dif_pos, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply