-- 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 Γ₀'
h : v.IsEquiv w
h_val : IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
u : ↥(valueGroup (F := Valuation R Γ₀) Valued.v) := WithZero.unzero ⋯
a : R
ha : Ne.{u_5 + 1} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
y_1 : R
hu : HMul.hMul (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (Valued.v : (a : R) → Γ₀) y_1
y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_def : y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_ne_zero : y₀ ≠ 0
y : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) b < (↑y : ValueGroup₀ Valued.v)
h₁ :
  ∀
    (hb :
      (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
          ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
        (↑y : ValueGroup₀ Valued.v)),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
h₂ :
  ∀
    (hb :
      (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
          ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
        (↑(Units.mk0 y₀ hy₀_ne_zero) : ValueGroup₀ Valued.v)),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
h₃ :
  ∀
    (hb :
      (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
          ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
        y₀),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
h₄ :
  ∀
    (hb :
      LT.lt.{u_6} (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
        ((h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
            ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) :
          ValueGroup₀ (F := Valuation R Γ₀') Valued.v)
        ((h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v) :
          ValueGroup₀ (F := Valuation R Γ₀') Valued.v)),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
h₅ h₆ h₇ h₈ :
  ∀ (hb : (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
⊢ (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)

Tactic:
rwa [← h_val.orderMonoidIso_spec, hy_def, Units.val_mk0, hy₀_def,
    h_val.orderMonoidIso.strictMono.lt_iff_lt] at hb

Premises used: Valuation.IsEquiv.orderMonoidIso, StrictMono.lt_iff_lt, OrderMonoidIso.strictMono, Units.val_mk0, Valuation.IsEquiv.orderMonoidIso_spec