awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
⊢ IsNontrivial R ↔ v.IsNontrivial
have mp : IsNontrivial R → v.IsNontrivial
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
mp : IsNontrivial R → v.IsNontrivial
⊢ IsNontrivial R ↔ v.IsNontrivial
have mpr : v.IsNontrivial → IsNontrivial R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : ValueGroupWithZero R
hr : r ≠ 0
hr' : r ≠ 1
⊢ v.IsNontrivial
have mp : ∀ (r : R) (s : ↥(posSubmonoid R)) (hr : ValueGroupWithZero.mk r s ≠ 0) (hr' : ValueGroupWithZero.mk r s ≠ 1),
  v.IsNontrivial
Tactic: induction r using ValueGroupWithZero.ind with | mk r s
Cleared hypotheses: r, hr, hr'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
⊢ v.IsNontrivial
have hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
Tactic: have hγ : v r ≠ 0 := by simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
⊢ v.IsNontrivial
have hγ' : LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
  LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)
Tactic: have hγ' : v r ≤ v s → v r < v s := by
      simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hγ' :
  LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
    LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)
⊢ v.IsNontrivial
have pos : ∀ (hr : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)), v.IsNontrivial
Tactic: by_cases hr : v r = 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hγ' :
  LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) →
    LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀)
pos : ∀ (hr : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)), v.IsNontrivial
⊢ v.IsNontrivial
have neg : ∀ (hr : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)), v.IsNontrivial
Tactic: by_cases hr : v r = 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
x : K
y : ↥(posSubmonoid K)
⊢ ValueGroupWithZero.mk x y = (valuation K : (a : K) → ValueGroupWithZero K) (x / (↑y : K))
have rw : ValueGroupWithZero.mk x y =
  HDiv.hDiv (α := ValueGroupWithZero K) (β := ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) (↑y : K) : ValueGroupWithZero K)
Tactic: rw [Valuation.map_div, ValueGroupWithZero.mk_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
x : K
y : ↥(posSubmonoid K)
rw :
  ValueGroupWithZero.mk x y =
    HDiv.hDiv (α := ValueGroupWithZero K) (β := ValueGroupWithZero K)
      ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
      ((valuation K : (a : K) → ValueGroupWithZero K) (↑y : K) : ValueGroupWithZero K)
⊢ ValueGroupWithZero.mk x y = (valuation K : (a : K) → ValueGroupWithZero K) (x / (↑y : K))
have rw₁ : HDiv.hDiv (α := ValueGroupWithZero K) (β := ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) (↑y : K) : ValueGroupWithZero K) =
  HDiv.hDiv (α := ValueGroupWithZero K) (β := ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) (↑y : K) : ValueGroupWithZero K)
Tactic: rw [Valuation.map_div, ValueGroupWithZero.mk_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
⊢ ∃ (a : R) (b : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      γ
have mk : ∀ (a : R) (b : ↥(posSubmonoid R)),
  ∃ (a_1 : R) (b_1 : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) a_1 : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b_1 : R) : ValueGroupWithZero R) =
      ValueGroupWithZero.mk a b
Tactic: induction γ using ValueGroupWithZero.ind with | mk a b
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
a : R
b : ↥(posSubmonoid R)
⊢ ∃ (a_1 : R) (b_1 : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) a_1 : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b_1 : R) : ValueGroupWithZero R) =
      ValueGroupWithZero.mk a b
have h : HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
    ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
    ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
  ValueGroupWithZero.mk a b
Tactic: use a, b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
⊢ ∃ (a : ↥(posSubmonoid R)) (b : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑a : R) : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      (↑γ : ValueGroupWithZero R)
have obtain : ∀ (a : R) (b : ↥(posSubmonoid R))
  (hab :
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      (↑γ : ValueGroupWithZero R)),
  ∃ (a : ↥(posSubmonoid R)) (b : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑a : R) : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      (↑γ : ValueGroupWithZero R)
Tactic: obtain ⟨a, b, hab⟩ := exists_valuation_div_valuation_eq γ.val
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
    (↑γ : ValueGroupWithZero R)
⊢ Membership.mem (γ := Submonoid R) (posSubmonoid R) a
have contrapose! : ∀ (hab : a ∉ posSubmonoid R),
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) ≠
    (↑γ : ValueGroupWithZero R)
Tactic: contrapose! hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab : a ∉ posSubmonoid R
⊢ HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) ≠
    (↑γ : ValueGroupWithZero R)
have hab₁ : Eq (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
  (0 : ValueGroupWithZero R)
Tactic: rw [posSubmonoid_def, not_vlt, ← valuation_eq_zero_iff] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
    (↑γ : ValueGroupWithZero R)
⊢ ∃ (a : ↥(posSubmonoid R)) (b : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑a : R) : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      (↑γ : ValueGroupWithZero R)
have lift : ∀ (a : ↥(posSubmonoid R))
  (hab :
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑a : R) : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      (↑γ : ValueGroupWithZero R)),
  ∃ (a : ↥(posSubmonoid R)) (b : ↥(posSubmonoid R)),
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑a : R) : ValueGroupWithZero R)
        ((valuation R : (a : R) → ValueGroupWithZero R) (↑b : R) : ValueGroupWithZero R) =
      (↑γ : ValueGroupWithZero R)
Tactic: lift a to posSubmonoid R using by
    contrapose! hab
    rw [posSubmonoid_def, not_vlt, ← valuation_eq_zero_iff] at hab
    simp [hab, eq_comm]
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
⊢ LT.lt (α := ValueGroupWithZero R) 0 (uniformizer R)
have obtain : ∀ (γ : ValueGroupWithZero R) (hγ : 0 < γ) (hγ' : γ < 1), LT.lt (α := ValueGroupWithZero R) 0 (uniformizer R)
Tactic: obtain ⟨γ, hγ, hγ'⟩ := IsNontrivial.exists_lt_one (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
a : ValueGroupWithZero R
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
have pos : ∀ (ha : a = 0), (uniformizer R)⁻¹ ≤ a ↔ 1 < a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
a : ValueGroupWithZero R
pos : ∀ (ha : a = 0), (uniformizer R)⁻¹ ≤ a ↔ 1 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
have neg : ∀ (ha : ¬a = 0), (uniformizer R)⁻¹ ≤ a ↔ 1 < a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
a : ValueGroupWithZero R
ha : ¬a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
have ha₁ : 0 < a
Tactic: replace ha : 0 < a := bot_lt_iff_ne_bot.mpr ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
a : ValueGroupWithZero R
ha : 0 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
have neg : a⁻¹ ≤ uniformizer R ↔ 1 < a
Tactic: rw [inv_le_comm₀ uniformizer_pos ha, le_uniformizer_iff, inv_lt_one₀ ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
a : ValueGroupWithZero R
ha : 0 < a
neg : a⁻¹ ≤ uniformizer R ↔ 1 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
have neg₁ : a⁻¹ < 1 ↔ 1 < a
Tactic: rw [inv_le_comm₀ uniformizer_pos ha, le_uniformizer_iff, inv_lt_one₀ ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
a : ValueGroupWithZero R
ha : 0 < a
neg : a⁻¹ ≤ uniformizer R ↔ 1 < a
neg₁ : a⁻¹ < 1 ↔ 1 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
have neg₂ : 1 < a ↔ 1 < a
Tactic: rw [inv_le_comm₀ uniformizer_pos ha, le_uniformizer_iff, inv_lt_one₀ ha]
-- 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)
⊢ @vle _ inst_2 _ (x * (↑r : R)) (y * (↑s : R)) →
    @vle _ inst_2 _ (y * (↑s : R)) (x * (↑r : R)) →
      Eq.{u_3 + 1} (α := ValueGroup₀ v)
        ((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 s)
        ((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))
          y r)
have simp : HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
  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) (↑s : R) :
        ValueGroup₀ v) =
    HDiv.hDiv (α := 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) (↑r : R) :
        ValueGroup₀ v)
Tactic: simp only [Valuation.Compatible.vle_iff_le (v := v), map_mul, ← and_imp, ← le_antisymm_iff]
-- 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) : Γ) →
    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) (↑s : R) :
          ValueGroup₀ v) =
      HDiv.hDiv (α := 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) (↑r : R) :
          ValueGroup₀ v)
have rw : 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)
Tactic: rw [div_eq_div_iff]
-- 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)
rw :
  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)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    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) (↑s : R) :
          ValueGroup₀ v) =
      HDiv.hDiv (α := 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) (↑r : R) :
          ValueGroup₀ v)
have hb : Ne.{u_3 + 1} (α := ValueGroup₀ v)
  (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) : ValueGroup₀ v)
  (0 : ValueGroup₀ v)
Tactic: rw [div_eq_div_iff]
-- 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)
rw :
  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)
hb :
  Ne.{u_3 + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
      ValueGroup₀ v)
    (0 : ValueGroup₀ v)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) x : Γ) ((v : (a : R) → Γ) (↑r : R) : Γ) =
      HMul.hMul (α := Γ) (β := Γ) ((v : (a : R) → Γ) y : Γ) ((v : (a : R) → Γ) (↑s : R) : Γ) →
    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) (↑s : R) :
          ValueGroup₀ v) =
      HDiv.hDiv (α := 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) (↑r : R) :
          ValueGroup₀ v)
have hd : Ne.{u_3 + 1} (α := ValueGroup₀ v)
  (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) : ValueGroup₀ v)
  (0 : ValueGroup₀ v)
Tactic: rw [div_eq_div_iff]