awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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_1 : 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) : Γ₀)
hr : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑s : R) : Γ₀) (1 : Γ₀)
⊢ False

Tactic:
simp [h, hr] at hγ'
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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_1 : 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) : Γ₀)
hr : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
⊢ v.IsNontrivial

Tactic:
exact ⟨s, by simp, fun h ↦ by simp [h, hr] at hγ'⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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_1 : 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) : Γ₀)
hr : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)

Tactic:
simpa using hγ
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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_1 : 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) : Γ₀)
hr : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
⊢ v.IsNontrivial

Tactic:
exact ⟨r, by simpa using hγ, hr⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
hr : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hr' : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
⊢ Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) r : ValueGroupWithZero R)
    (1 : ValueGroupWithZero R)

Tactic:
simpa [(isEquiv v (valuation R)).eq_one_iff_eq_one] using hr'

Premises used: ValuativeRel.isEquiv, Valuation.IsEquiv.eq_one_iff_eq_one, ValuativeRel.valuation
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
hr : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hr' : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)
⊢ IsNontrivial R

Tactic:
exact ⟨valuation R r, (isEquiv v (valuation R)).eq_zero.ne.mp hr,
      by simpa [(isEquiv v (valuation R)).eq_one_iff_eq_one] using hr'⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : IsNontrivial R
v : Valuation R Γ₀
inst_4 : v.Compatible
rwa rwa₁ rwa₂ rwa₃ : IsNontrivial R
⊢ v.IsNontrivial

Tactic:
rwa [← isNontrivial_iff_isNontrivial]

Premises used: ValuativeRel.isNontrivial_iff_isNontrivial
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
rw₁ 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)
⊢ ValueGroupWithZero.mk x y = (valuation K : (a : K) → ValueGroupWithZero K) (x / (↑y : K))

Tactic:
rw [Valuation.map_div, ValueGroupWithZero.mk_eq_div]

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_div, Valuation.map_div
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
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
⊢ ∃ (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) =
      γ

Tactic:
induction γ using ValueGroupWithZero.ind with | mk a b

Premises used: ValuativeRel.ValueGroupWithZero.ind, ValuativeRel.mk
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
a : R
b : ↥(posSubmonoid R)
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
⊢ ∃ (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:
use a, b
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel 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) =
    ValueGroupWithZero.mk a b

Tactic:
simp [valuation, div_eq_mul_inv, ValueGroupWithZero.inv_mk (b : R) 1 b.prop]

Premises used: ValuativeRel.ValueGroupWithZero.inv_mk, div_eq_mul_inv, Subtype.prop, ValuativeRel.valuation, OfNat.ofNat, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
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)
⊢ ∃ (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

Premises used: Units.val, ValuativeRel.exists_valuation_div_valuation_eq
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ Membership.mem (γ := Submonoid R) (posSubmonoid R) a

Tactic:
contrapose! hab
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab : a ∉ posSubmonoid R
⊢ 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

Premises used: ValuativeRel.valuation_eq_zero_iff, ValuativeRel.not_vlt, ValuativeRel.posSubmonoid_def
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab :
  Eq (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
    (0 : ValueGroupWithZero 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:
simp [hab, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ ∃ (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]

Premises used: ValuativeRel.posSubmonoid
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
b 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)
w w₁ : ↥(posSubmonoid R)
h :
  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:
use a, b
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
⊢ Function.Surjective (α := K) (β := ValueGroupWithZero K) (⇑(valuation K) : (a : K) → ValueGroupWithZero K)

Tactic:
ValueGroupWithZero.ind (ValueGroupWithZero.mk_eq_valuation · · ▸ ⟨_, rfl⟩)

Premises used: Eq.rec, HDiv.hDiv, ValuativeRel.ValueGroupWithZero.ind, Exists.intro, Eq.symm, Subtype.val, Function.Surjective, ValuativeRel.ValueGroupWithZero.mk_eq_valuation, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
⊢ LT.lt (α := ValueGroupWithZero R) (uniformizer R) 1

Tactic:
IsDiscrete.has_maximal_element.choose_spec.1

Premises used: Exists.choose_spec, ValuativeRel.IsDiscrete.has_maximal_element, And.left, ValuativeRel.uniformizer
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
a : ValueGroupWithZero R
⊢ a ≤ uniformizer R ↔ a < 1

Tactic:
⟨fun h ↦ h.trans_lt uniformizer_lt_one,
    IsDiscrete.has_maximal_element.choose_spec.2 a⟩

Premises used: Exists.choose_spec, ValuativeRel.IsDiscrete.has_maximal_element, And.right, Iff.intro, LE.le.trans_lt, ValuativeRel.uniformizer_lt_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
obtain : ∀ (γ : ValueGroupWithZero R) (hγ : 0 < γ) (hγ' : γ < 1), LT.lt (α := ValueGroupWithZero R) 0 (uniformizer R)
⊢ LT.lt (α := ValueGroupWithZero R) 0 (uniformizer R)

Tactic:
obtain ⟨γ, hγ, hγ'⟩ := IsNontrivial.exists_lt_one (R := R)

Premises used: ValuativeRel.IsNontrivial.exists_lt_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
γ : ValueGroupWithZero R
hγ : 0 < γ
hγ' : γ < 1
⊢ LT.lt (α := ValueGroupWithZero R) 0 (uniformizer R)

Tactic:
hγ.trans_le (le_uniformizer_iff.mpr hγ')

Premises used: Iff.mpr, ValuativeRel.le_uniformizer_iff, LT.lt.trans_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
γ : ValueGroupWithZero R
hγ : 0 < γ
hγ' : γ < 1
⊢ LT.lt (α := ValueGroupWithZero R) 0 (uniformizer R)

Tactic:
exact hγ.trans_le (le_uniformizer_iff.mpr hγ')

Premises used: Iff.mpr, ValuativeRel.le_uniformizer_iff, LT.lt.trans_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsDiscrete R
inst_3 : IsNontrivial R
⊢ Ne (α := ValueGroupWithZero R) (uniformizer R) 0

Tactic:
uniformizer_pos.ne'

Premises used: LT.lt.ne', ValuativeRel.uniformizer_pos
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
neg : ∀ (ha : ¬a = 0), (uniformizer R)⁻¹ ≤ a ↔ 1 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
⊢ 0 < a

Tactic:
replace ha : 0 < a := bot_lt_iff_ne_bot.mpr ha
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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
neg₂ neg₃ : 1 < a ↔ 1 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

Tactic:
rw [inv_le_comm₀ uniformizer_pos ha, le_uniformizer_iff, inv_lt_one₀ ha]

Premises used: inv_lt_one₀, ValuativeRel.le_uniformizer_iff, inv_le_comm₀, ValuativeRel.uniformizer_pos
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ @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)

Tactic:
simp only [Valuation.Compatible.vle_iff_le (v := v), map_mul, ← and_imp, ← le_antisymm_iff]

Premises used: and_imp, map_mul, le_antisymm_iff, Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
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)
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)
⊢ 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:
rw [div_eq_div_iff]

Premises used: div_eq_div_iff