awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
          ValueGroup₀ v) =
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) y : ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
          ValueGroup₀ v)
have simp : HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
  Eq.{u_3 + 1} (α := ValueGroup₀ v)
    (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) then 0
    else
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) x) sorry) sorry) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) (↑r : R)) sorry) sorry) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)))
    (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ) then 0
    else
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) y) sorry) sorry) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) sorry) sorry) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)))
Tactic: simp only [ValueGroup₀.restrict₀_apply, Valuation.apply_posSubmonoid_ne_zero, ↓reduceDIte,
        dite_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    Eq.{u_3 + 1} (α := ValueGroup₀ v)
      (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) then 0
      else
        HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) x) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) (↑r : R)) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)))
      (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ) then 0
      else
        HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) y) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)))
have pos : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) →
  Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ) →
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
        HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
      Eq.{u_3 + 1} (α := ValueGroup₀ v) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
pos :
  Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) →
    Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ) →
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
          HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
        Eq.{u_3 + 1} (α := ValueGroup₀ v) 0 0
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    Eq.{u_3 + 1} (α := ValueGroup₀ v)
      (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) then 0
      else
        HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) x) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) (↑r : R)) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)))
      (if h : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ) then 0
      else
        HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) y) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) ⋯) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)))
have neg : Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) x : Γ) (0 : Γ) →
  ∀ (h : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : R) → Γ) y : Γ) (0 : Γ)),
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
        HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
      0 =
        HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) y) sorry) sorry) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          ((↑(Subtype.mk (p := fun (x : Γˣ) ↦ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ) (↑s : R)) sorry) sorry) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
x x_1 : ValueGroupWithZero R
⊢ ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r : ValueGroup₀ v)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v))
      ⋯ (x * x_1) =
    ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r :
              ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
              ValueGroup₀ v))
        ⋯ x *
      ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) r :
              ValueGroup₀ v)
            (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
              ValueGroup₀ v))
        ⋯ x_1
have hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)),
  HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (a * b) :
        ValueGroup₀ v)
      (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑(r * s) : R) :
        ValueGroup₀ v) =
    HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
          ValueGroup₀ v) *
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) b : ValueGroup₀ v)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
          ValueGroup₀ v)
Tactic: apply lift_mul
-- 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
x : R
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        ((valuation R : (a : R) → ValueGroupWithZero R) x) :
      ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
have h : ((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x =
  HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑1 : R) :
      ValueGroup₀ v)
Tactic: convert! embed_mk v x 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
⊢ (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      ((embed (valuation R) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R)) γ) =
    γ
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)),
  (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      ((embed (valuation R) : (a : ValueGroupWithZero R) → ValueGroup₀ (valuation R)) (ValueGroupWithZero.mk x y)) =
    ValueGroupWithZero.mk x y
Tactic: induction γ using ValueGroupWithZero.ind
Cleared hypotheses: γ
-- 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 b : ValueGroupWithZero R
h : a < b
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        a :
      ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        b :
      ValueGroup₀ v)
have obtain : ∀ (a : R) (r : ↥(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) <
      b),
  LT.lt.{u_3} (α := ValueGroup₀ v)
    (((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)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        b :
      ValueGroup₀ v)
Tactic: obtain ⟨a, r, rfl⟩ := exists_valuation_div_valuation_eq a
Cleared hypotheses: a, h
-- 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
b : ValueGroupWithZero R
a : R
r : ↥(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) <
    b
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
    (((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)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        b :
      ValueGroup₀ v)
have obtain : ∀ (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)),
  LT.lt.{u_3} (α := ValueGroup₀ v)
    (((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)
    (((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: obtain ⟨b, s, rfl⟩ := exists_valuation_div_valuation_eq b
Cleared hypotheses: b, h
-- 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)
⊢ LT.lt.{u_3} (α := ValueGroup₀ v)
    (((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)
    (((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)
have rw : 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: rw [← embedding_strictMono.lt_iff_lt]
-- 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)
⊢ 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) :
      Γ)
have 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) :
      Γ)
Tactic: simp only [map_div₀]
-- 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 :
  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) :
      Γ)
have hb : ¬Eq (α := Γ)
    ((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) :
      Γ)
    (0 : Γ)
Tactic: simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]