awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)

Tactic:
rw [h] at this
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ x = -1 + (1 + x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
mpr : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (-1 + (1 + x)) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
rw [show x = -1 + (1 + x) by simp]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (-1 + (1 + x)) : Γ'₀) (1 : Γ'₀)

Tactic:
le_trans (v'.map_add _ _) ?_

Premises used: Valuation.map_add, le_trans
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
mpr : LE.le.{u_5} (α := Γ'₀) (max ((v' : (a : K) → Γ'₀) (-1)) ((v' : (a : K) → Γ'₀) (1 + x)) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (-1 + (1 + x)) : Γ'₀) (1 : Γ'₀)

Tactic:
refine le_trans (v'.map_add _ _) ?_

Premises used: Valuation.map_add, le_trans
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) (max ((v' : (a : K) → Γ'₀) (-1)) ((v' : (a : K) → Γ'₀) (1 + x)) : Γ'₀) (1 : Γ'₀)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
rw [h] at hx'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
le_of_eq hx'

Premises used: le_of_eq
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
exact le_of_eq hx'

Premises used: le_of_eq
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
mpr :
  ∀ (hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
mpr₁ :
  ∀ (hx' : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rcases lt_or_eq_of_le hx with hx' | hx'

Premises used: lt_or_eq_of_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)

Tactic:
rw [← v'.map_one]

Premises used: Valuation.map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
h₁ : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)

Tactic:
apply map_add_eq_of_lt_left

Premises used: Valuation.map_add_eq_of_lt_left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)

Tactic:
have : v' (1 + x) = 1 := by
          rw [← v'.map_one]
          apply map_add_eq_of_lt_left
          simpa
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)

Tactic:
rw [← h] at this
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
⊢ x = -1 + (1 + x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
mpr : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (-1 + (1 + x)) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [show x = -1 + (1 + x) by simp]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (-1 + (1 + x)) : Γ₀) (1 : Γ₀)

Tactic:
le_trans (v.map_add _ _) ?_

Premises used: Valuation.map_add, le_trans
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
mpr : LE.le.{u_4} (α := Γ₀) (max ((v : (a : K) → Γ₀) (-1)) ((v : (a : K) → Γ₀) (1 + x)) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (-1 + (1 + x)) : Γ₀) (1 : Γ₀)

Tactic:
refine le_trans (v.map_add _ _) ?_

Premises used: Valuation.map_add, le_trans
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) (max ((v : (a : K) → Γ₀) (-1)) ((v : (a : K) → Γ₀) (1 + x)) : Γ₀) (1 : Γ₀)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [← h] at hx'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
le_of_eq hx'

Premises used: le_of_eq
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
exact le_of_eq hx'

Premises used: le_of_eq
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
mp :
  v.IsEquiv v' →
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
mpr :
  (∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) →
    v.IsEquiv v'
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : v.IsEquiv v'
x : K
mp mp₁ :
  LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
rw [h.lt_one_iff_lt_one]

Premises used: Valuation.IsEquiv.lt_one_iff_lt_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
mpr :
  (∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) →
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ (∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) →
    v.IsEquiv v'

Tactic:
rw [isEquiv_iff_val_eq_one]

Premises used: Valuation.isEquiv_iff_val_eq_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
pos :
  ∀ (hx : x = 0),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
neg :
  ∀ (hx : ¬x = 0),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : x = 0
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
simp only [(zero_iff _).2 hx, zero_ne_one]

Premises used: Iff.mpr, zero_ne_one, Valuation.zero_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : ¬x = 0
neg :
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) →
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
neg₁ :
  Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) →
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : ¬x = 0
hh : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
neg : ∀ (h_1 : ¬Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)), False
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
by_contra h_1
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : ¬x = 0
hh : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h_1 : ¬Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
h_2 : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ False

Tactic:
simpa [hh, lt_self_iff_false] using h.2 h_2

Premises used: Iff.mpr, lt_self_iff_false
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h :
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : ¬x = 0
hh : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h_1 : ¬Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
h_2 : LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh

Premises used: inv_one, map_inv₀, inv_eq_iff_eq_inv