-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ
r s : R
hr₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') r : Γ₀')
hs₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') s : Γ₀')
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) r :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) =
    (↑γ : ValueGroup₀ Valued.v)
h₁ :
  ∀ (x : WithVal v),
    Membership.mem (γ := Set (WithVal v))
        {x : WithVal v |
          (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
            (↑(Units.mk0
                  (HDiv.hDiv (α :=
                    ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
                    ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
                    ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀))
                        (((equiv v).symm : (a : R) → WithVal v) r) :
                      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
                    ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀))
                        (((equiv v).symm : (a : R) → WithVal v) s) :
                      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)))
                  ⋯) :
              ValueGroup₀ Valued.v)}
        x →
      Membership.mem (α := R) (γ := Set R)
        {x : R |
          (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x < (↑γ : ValueGroup₀ Valued.v)}
        ((equiv v : (a : WithVal v) → R) x : R)
⊢ ∃ (ia : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ),
    ∀ (x : WithVal v),
      Membership.mem (γ := Set (WithVal v))
          {x : WithVal v |
            (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
              (↑ia : ValueGroup₀ Valued.v)}
          x →
        Membership.mem (α := R) (γ := Set R)
          {x : R |
            (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
              (↑γ : ValueGroup₀ Valued.v)}
          ((equiv v : (a : WithVal v) → R) x : R)

Tactic:
use .mk0 ((instValued v).v.restrict ((WithVal.equiv v).symm r) /
    (instValued v).v.restrict ((WithVal.equiv v).symm s)) (by
    simp [Valuation.restrict_def, restrict₀_eq_zero_iff, (eq_zero h (r := r)).ne, ← hv,
      (eq_zero h (r := s)).ne, hr₀.ne', hs₀.ne'])