-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R) <
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
rw :
  ∀
    (h :
      HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) <
        HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)),
    HMul.hMul (α := Γ) (β := Γ)
        ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
            (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                  (a : ValueGroupWithZero R) → ValueGroup₀ v)
                ((valuation R : (a : R) → ValueGroupWithZero R) a) :
              ValueGroup₀ v) :
          Γ)
        ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
            (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                  (a : ValueGroupWithZero R) → ValueGroup₀ v)
                ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
              ValueGroup₀ v) :
          Γ) <
      HMul.hMul (α := Γ) (β := Γ)
        ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
            (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                  (a : ValueGroupWithZero R) → ValueGroup₀ v)
                ((valuation R : (a : R) → ValueGroupWithZero R) b) :
              ValueGroup₀ v) :
          Γ)
        ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
            (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                  (a : ValueGroupWithZero R) → ValueGroup₀ v)
                ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
              ValueGroup₀ v) :
          Γ)
⊢ HDiv.hDiv (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) a) :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
            ValueGroup₀ v) :
        Γ) <
    HDiv.hDiv (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) b) :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
            ValueGroup₀ v) :
        Γ)
have hb : ∀
  (h :
    HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) <
      HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)),
  LT.lt (α := Γ) (0 : Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
          ValueGroup₀ v) :
      Γ)
Tactic: rw [div_lt_div_iff₀] at h ⊢
Cleared hypotheses: h