-- 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)
x : WithVal v
hx :
  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
y : R := (equiv v : (a : WithVal v) → R) x
hy : toVal v y = x
hs0' :
  LT.lt.{u_5} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
    (0 : 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 →*₀ Γ₀)) (toVal v s) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
h' : v.restrict.IsEquiv w.restrict
h₁ :
  LT.lt.{u_5} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (toVal v.restrict (y * s)).ofVal :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀))
        (ofVal.{u_4, u_5} (Γ₀ := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (v := v.restrict)
          ((h'.orderRingIso.symm : (a : WithVal w.restrict) → WithVal v.restrict) (toVal w.restrict r))) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ 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:
rw [← hr, equiv_apply, Set.mem_setOf_eq, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), hv,
    ← map_mul, ← lt_def, ← ofVal_mul,
    ← hy, ← toVal_mul, ← h'.orderRingIso_apply, ← h'.orderRingIso.lt_symm_apply, lt_def]

Premises used: Iff.mpr, Valuation.IsEquiv.orderRingIso_apply, WithVal.ofVal_mul, lt_div_iff₀, Valued.v, WithVal.toVal_mul, WithVal.equiv_apply, Set.mem_setOf_eq, WithVal.lt_def, Valuation.restrict_pos_iff, map_mul, OrderRingIso.lt_symm_apply, Valuation.IsEquiv.orderRingIso