-- 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 : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  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 →*₀ Γ₀)) 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 →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
h₁ :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        {x : R |
          (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
            (↑(Units.mk0
                  (HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
                    ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
                    ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀'))
                        ((equiv v : (a : WithVal v) → R) r) :
                      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
                    ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀'))
                        ((equiv v : (a : WithVal v) → R) s) :
                      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')))
                  ⋯) :
              ValueGroup₀ Valued.v)}
        x →
      Membership.mem (α := WithVal v) (γ := Set (WithVal v))
        {x : WithVal v |
          (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
            (↑γ : ValueGroup₀ Valued.v)}
        (((equiv v).symm : (a : R) → WithVal v) x : WithVal v)
⊢ ∃ (ia : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ),
    ∀ (x : R),
      Membership.mem (γ := Set R)
          {x : R |
            (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
              (↑ia : ValueGroup₀ Valued.v)}
          x →
        Membership.mem (α := WithVal v) (γ := Set (WithVal v))
          {x : WithVal v |
            (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
              (↑γ : ValueGroup₀ Valued.v)}
          (((equiv v).symm : (a : R) → WithVal v) x : WithVal v)

Tactic:
use .mk0 ((Valued.v.restrict ((WithVal.equiv v) r)) /
    (Valued.v.restrict ((WithVal.equiv v) s))) (by
    simp only [equiv_apply, restrict_def, restrict₀_eq_zero_iff, ne_eq, div_eq_zero_iff, not_or,
      hv, (eq_zero h (r := r.ofVal)).ne, (eq_zero h (r := s.ofVal)).ne]
    exact ⟨hr₀.ne', hs₀.ne'⟩)