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 : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (-x) : Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (1 + -x) : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (1 - x) : Γ₀) (1 : Γ₀)

Tactic:
rw [sub_eq_add_neg 1 x]

Premises used: sub_eq_add_neg, 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 : 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, v.map_neg] using v.map_add_eq_of_lt_left h

Premises used: Valuation.map_add_eq_of_lt_left, Valuation.map_one, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
ν : Valuation R Γ₀
h :
  ∀ (r : R),
    Eq.{u_4 + 1} (α := Γ₀) ((map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ (map (↑f : Γ₀ →*₀ Γ'₀) ⋯ ν) : (a : R) → Γ₀) r : Γ₀)
      ((ν : (a : R) → Γ₀) r : Γ₀)
⊢ map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ (map (↑f : Γ₀ →*₀ Γ'₀) ⋯ ν) = ν

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
ν : Valuation R Γ₀
r : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ (map (↑f : Γ₀ →*₀ Γ'₀) ⋯ ν) : (a : R) → Γ₀) r : Γ₀)
    ((ν : (a : R) → Γ₀) r : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
ν : Valuation R Γ'₀
h :
  ∀ (r : R),
    Eq.{u_5 + 1} (α := Γ'₀) ((map (↑f : Γ₀ →*₀ Γ'₀) ⋯ (map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ ν) : (a : R) → Γ'₀) r : Γ'₀)
      ((ν : (a : R) → Γ'₀) r : Γ'₀)
⊢ map (↑f : Γ₀ →*₀ Γ'₀) ⋯ (map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ ν) = ν

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
ν : Valuation R Γ'₀
r : R
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((map (↑f : Γ₀ →*₀ Γ'₀) ⋯ (map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ ν) : (a : R) → Γ'₀) r : Γ'₀)
    ((ν : (a : R) → Γ'₀) r : Γ'₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
simp :
  LE.le.{u_4} (α := Γ₀) (if x + y = 0 then 0 else 1) (if x = 0 then 0 else 1) ∨
    LE.le.{u_4} (α := Γ₀) (if x + y = 0 then 0 else 1) (if y = 0 then 0 else 1)
⊢ LE.le.{u_4} (α := Γ₀) (ZeroHom.toFun (↑1 : ZeroHom R Γ₀) (x + y))
    (max (ZeroHom.toFun (↑1 : ZeroHom R Γ₀) x) (ZeroHom.toFun (↑1 : ZeroHom R Γ₀) y))

Tactic:
simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe,
        MonoidWithZeroHom.one_apply_def, le_sup_iff]

Premises used: MonoidWithZeroHom.toZeroHom_coe, MonoidWithZeroHom.one_apply_def, le_sup_iff, ZeroHom.toFun_eq_coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
pos : x + y = 0 → x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 0 0 ∨ LE.le.{u_4} (α := Γ₀) 0 0
neg : x + y = 0 → x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 0 ∨ LE.le.{u_4} (α := Γ₀) 0 1
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 1
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 0
neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 1
pos₃ : ¬x + y = 0 → ¬x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 0
neg₃ : ¬x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 1
⊢ LE.le.{u_4} (α := Γ₀) (if x + y = 0 then 0 else 1) (if x = 0 then 0 else 1) ∨
    LE.le.{u_4} (α := Γ₀) (if x + y = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : x + y = 0
h_1 : x = 0
h_2 : y = 0
⊢ LE.le.{u_4} (α := Γ₀) 0 0 ∨ LE.le.{u_4} (α := Γ₀) 0 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : x + y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ LE.le.{u_4} (α := Γ₀) 0 0 ∨ LE.le.{u_4} (α := Γ₀) 0 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : x + y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : ¬x + y = 0
h_1 : x = 0
h_2 : y = 0
⊢ LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : ¬x + y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ LE.le.{u_4} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x_1 y_1 : R
inst_5 : Nontrivial R
inst_6 : NoZeroDivisors R
inst_7 : DecidablePred fun (x : R) ↦ x = 0
x y : R
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ LE.le.{u_4} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (if x = 0 then 0 else 1 : Γ₀)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
⊢ Eq (α := R →*₀ Γ₀) (toMonoidWithZeroHom 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
hx : x ≠ 0
⊢ Eq.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
if_neg hx

Premises used: if_neg, ite
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0

Tactic:
MonoidWithZeroHom.one_apply_eq_zero_iff

Premises used: MonoidWithZeroHom.one_apply_eq_zero_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
rw : LE.le.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1
⊢ LE.le.{u_4} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [one_apply_def]

Premises used: Valuation.one_apply_def
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
pos : x = 0 → LE.le.{u_4} (α := Γ₀) 0 1
neg : ¬x = 0 → LE.le.{u_4} (α := Γ₀) 1 1
⊢ LE.le.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
h : x = 0
⊢ LE.le.{u_4} (α := Γ₀) 0 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
h : ¬x = 0
⊢ LE.le.{u_4} (α := Γ₀) 1 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
rw : LT.lt.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1 ↔ x = 0
⊢ LT.lt.{u_4} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔ x = 0

Tactic:
rw [one_apply_def]

Premises used: Valuation.one_apply_def
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
pos : x = 0 → (LT.lt.{u_4} (α := Γ₀) 0 1 ↔ x = 0)
neg : ¬x = 0 → (LT.lt.{u_4} (α := Γ₀) 1 1 ↔ x = 0)
⊢ LT.lt.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1 ↔ x = 0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
h : x = 0
⊢ LT.lt.{u_4} (α := Γ₀) 0 1 ↔ x = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
h : ¬x = 0
⊢ LT.lt.{u_4} (α := Γ₀) 1 1 ↔ x = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔ x ≠ 0

Tactic:
MonoidWithZeroHom.one_apply_eq_one_iff

Premises used: MonoidWithZeroHom.one_apply_eq_one_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_7
inst_1 : DivisionRing R
v : Valuation R Γ₀
⊢ ∀ (x : R), Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x⁻¹ : Γ₀) (((v : (a : R) → Γ₀) x)⁻¹ : Γ₀)

Tactic:
map_inv₀ _

Premises used: map_inv₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_7
inst_1 : DivisionRing R
v : Valuation R Γ₀
⊢ ∀ (x y : R),
    (v : (a : R) → Γ₀) (x / y) = HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
map_div₀ _

Premises used: map_div₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp [inv_lt_one₀ (v.pos_iff.2 h)]

Premises used: Iff.mpr, inv_lt_one₀, Valuation.pos_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ LE.le.{u_4} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp [inv_le_one₀ (v.pos_iff.2 h)]

Premises used: Iff.mpr, inv_le_one₀, Valuation.pos_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀)

Tactic:
simp [one_lt_inv₀ (v.pos_iff.2 h)]

Premises used: Iff.mpr, Valuation.pos_iff, one_lt_inv₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀)

Tactic:
simp [one_le_inv₀ (v.pos_iff.2 h)]

Premises used: Iff.mpr, one_le_inv₀, Valuation.pos_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
pos :
  ∀ (h : x = 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
neg :
  ∀ (h : ¬x = 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
by_cases h : x = 0
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp only [h, map_zero, zero_le', inv_zero, zero_lt_one, or_self]

Premises used: inv_zero, map_zero, zero_lt_one, or_self, zero_le'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp only [← one_lt_val_iff v h, le_or_gt]

Premises used: Valuation.one_lt_val_iff, le_or_gt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
pos :
  ∀ (h : x = 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
neg :
  ∀ (h : ¬x = 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
by_cases h : x = 0
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp only [h, map_zero, zero_le', inv_zero, or_self]

Premises used: inv_zero, map_zero, or_self, zero_le'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp only [← one_le_val_iff v h, le_total]

Premises used: le_total, Valuation.one_le_val_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x_1 : R
x_in : Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} x_1
rwa : (v : (a : R) → Γ₀) (-x_1) ≤ γ
rwa₁ rwa₂ rwa₃ rwa₄ : (v : (a : R) → Γ₀) x_1 ≤ γ
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} (-x_1)

Tactic:
rwa [Set.mem_setOf, map_neg]

Premises used: Set.mem_setOf, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
x : R
⊢ x ∈ v.leAddSubgroup γ ↔ (v : (a : R) → Γ₀) x ≤ γ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Monotone v.leAddSubgroup

Tactic:
fun _ _ h _ ↦ h.trans'

Premises used: Set.Mem, Monotone, setOf, LE.le.trans'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
pos :
  ∀
    (H :
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
      (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
        (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
neg :
  ∀
    (H :
      ¬(Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀))),
    LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
      (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
        (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))

Tactic:
by_cases H : v x ≠ 0 ∨ v y ≠ 0

Premises used: DFunLike.coe