-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
simp :
  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) :
        Γ)
⊢ LT.lt (α := Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            (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)) :
          ValueGroup₀ v) :
      Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            (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)) :
          ValueGroup₀ v) :
      Γ)

Tactic:
simp only [map_div₀]

Premises used: map_div₀