awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : (v : (a : R) → Γ₀) x < g
hy : (v : (a : R) → Γ₀) y < g
⊢ (v : (a : R) → Γ₀) (x + -y) < g

Tactic:
v.map_add_lt hx <| (v.map_neg y).trans_lt hy

Premises used: Valuation.map_add_lt, Valuation.map_neg, Eq.trans_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : (v : (a : R) → Γ₀) x < g
hy : (v : (a : R) → Γ₀) y < g
⊢ (v : (a : R) → Γ₀) (x + -y) < g

Tactic:
exact v.map_add_lt hx <| (v.map_neg y).trans_lt hy

Premises used: Valuation.map_add_lt, Valuation.map_neg, Eq.trans_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Subsingleton R
v : Valuation R Γ₀
x : R
rw : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)
rw₁ rw₂ : LE.le.{u_4} (α := Γ₀) 1 1
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [Subsingleton.elim x 1, Valuation.map_one]

Premises used: Valuation.map_one, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
suffices :
  ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)

Tactic:
suffices ¬v (x + y) < max (v x) (v y) from
    or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
inr :
  ∀
    (this :
      ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
        (h' :
          LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)
            (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
        (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False)
    (vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
wlog :
  ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
    (h' :
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
    (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
⊢ False

Tactic:
wlog vyx : v y < v x generalizing x y

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
this :
  ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
    (h' :
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
    (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ False

Tactic:
this h.symm ?_ (h.lt_or_gt.resolve_right vyx)

Premises used: Ne.symm, Or.resolve_right, Ne.lt_or_gt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
this :
  ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
    (h' :
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
    (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
inr : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) (max ((v : (a : R) → Γ₀) y) ((v : (a : R) → Γ₀) x) : Γ₀)
⊢ False

Tactic:
refine this h.symm ?_ (h.lt_or_gt.resolve_right vyx)

Premises used: Ne.symm, Or.resolve_right, Ne.lt_or_gt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
this :
  ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
    (h' :
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
    (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
inr : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) y) ((v : (a : R) → Γ₀) x) : Γ₀)
inr₁ inr₂ inr₃ inr₄ :
  LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) (max ((v : (a : R) → Γ₀) y) ((v : (a : R) → Γ₀) x) : Γ₀)

Tactic:
rwa [add_comm, max_comm]

Premises used: add_comm, max_comm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [max_eq_left_of_lt vyx] at h'

Premises used: max_eq_left_of_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
h'₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [max_eq_left_of_lt vyx] at h'

Premises used: max_eq_left_of_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
apply : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ False

Tactic:
apply lt_irrefl (v x)

Premises used: lt_irrefl, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (x + y - y) : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y - y) : Γ₀)
    (max ((v : (a : R) → Γ₀) (x + y)) ((v : (a : R) → Γ₀) y) : Γ₀)

Tactic:
map_sub _ _ _

Premises used: Valuation.map_sub
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) (max ((v : (a : R) → Γ₀) (x + y)) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
max_lt h' vyx

Premises used: max_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
v₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (x + y - y) : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
calc
    v x = v (x + y - y) := by simp
    _ ≤ max (v <| x + y) (v y) := map_sub _ _ _
    _ < v x := max_lt h' vyx

Premises used: HSub.hSub, Valuation.map_sub, max_lt, HAdd.hAdd, Max.max, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
(v.map_add_of_distinct_val h.ne).trans (max_eq_right_iff.mpr h.le)

Premises used: Iff.mpr, Valuation.map_add_of_distinct_val, LT.lt.le, max_eq_right_iff, Eq.trans, LT.lt.ne
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
map_add_eq_of_lt_right _ h

Premises used: Valuation.map_add_eq_of_lt_right
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
exact map_add_eq_of_lt_right _ h

Premises used: Valuation.map_add_eq_of_lt_right
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
rw [sub_eq_add_neg, map_add_eq_of_lt_right, map_neg]

Premises used: Valuation.map_add_eq_of_lt_right, sub_eq_add_neg, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h h₁ h₂ h₃ h₄ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀)

Tactic:
rwa [map_neg]

Premises used: Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
inl :
  ∀ (h0 : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
inr :
  ∀ (h0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)

Tactic:
rcases eq_or_ne (v (f j)) 0 with h0 | h0

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
h0 : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
h0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)
inr : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j + ∑ x ∈ s \ {j}, f x) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hj]

Premises used: Finset.sum_eq_add_sum_diff_singleton_of_mem
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
h0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j + ∑ x ∈ s \ {j}, f x) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)

Tactic:
map_add_eq_of_lt_left _ (map_sum_lt _ h0 hf)

Premises used: Valuation.map_sum_lt, Valuation.map_add_eq_of_lt_left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
h0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j + ∑ x ∈ s \ {j}, f x) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)

Tactic:
exact map_add_eq_of_lt_left _ (map_sum_lt _ h0 hf)

Premises used: Valuation.map_sum_lt, Valuation.map_add_eq_of_lt_left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [sub_eq_add_neg, map_add_eq_of_lt_left]

Premises used: sub_eq_add_neg, Valuation.map_add_eq_of_lt_left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h h₁ h₂ h₃ h₄ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rwa [map_neg]

Premises used: Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀)
    (max ((v : (a : R) → Γ₀) (y - x)) ((v : (a : R) → Γ₀) x) : Γ₀)

Tactic:
have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
this :
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀)
    (max ((v : (a : R) → Γ₀) (y - x)) ((v : (a : R) → Γ₀) x) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [max_eq_right (le_of_lt h)] at this

Premises used: le_of_lt, max_eq_right
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
pos :
  ∀ (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
neg :
  ∀ (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
by_cases hy : v y = 0

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simpa [*] using map_sub v x y

Premises used: Valuation.map_sub
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp [*, map_sub_eq_of_lt_right, zero_lt_iff]

Premises used: Valuation.map_sub_eq_of_lt_right, zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
rw₁ rw₂ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [map_sub_swap, map_sub_of_left_eq_zero v hy]

Premises used: Valuation.map_sub_swap, Valuation.map_sub_of_left_eq_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - -y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
rw₂ rw₃ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
rw [← sub_neg_eq_add, map_sub_of_left_eq_zero v hx, map_neg]

Premises used: Valuation.map_neg, Valuation.map_sub_of_left_eq_zero, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
rw₁ rw₂ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [add_comm, map_add_of_left_eq_zero v hy]

Premises used: add_comm, Valuation.map_add_of_left_eq_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀)

Tactic:
rw [← v.map_one] at h

Premises used: Valuation.map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)

Tactic:
simpa only [v.map_one] using v.map_add_eq_of_lt_left h

Premises used: Valuation.map_add_eq_of_lt_left, Valuation.map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (-x) : Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀)

Tactic:
rw [← v.map_one, ← v.map_neg] at h

Premises used: Valuation.map_one, Valuation.map_neg