awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha :
  Eq.{u_4 + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
pos :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₁ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) 0 : ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₂ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) (0 : ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₃ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
    (0 : ValueGroup₀ w)
pos₄ pos₅ pos₆ pos₇ :
  Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))

Tactic:
rwa [restrict_def, ha, map_zero, Eq.comm, ← h_res.eq_zero]

Premises used: map_zero, Valuation.restrict_def, Valuation.IsEquiv.eq_zero, Eq.comm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
neg :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) (↑(valueGroup.mk v 1 a ⋯ ha) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
⊢ Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))

Tactic:
rw [(v.restrict_eq_mk ha)]

Premises used: Valuation.restrict_eq_mk
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
⊢ Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (0 : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
h₁ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
    ((↑(valueGroup.mk w 1 a ⋯ ⋯) : WithZero ↥(valueGroup w)) : WithZero ↥(valueGroup w))
⊢ Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) (↑(valueGroup.mk v 1 a ⋯ ha) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))

Tactic:
convert! valueGroup₀Fun_spec (h := h) (hs := ha) (r := 1) (by simp)

Premises used: Valuation.IsEquiv.valueGroup₀Fun_spec
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
⊢ Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
    ((↑(valueGroup.mk w 1 a ⋯ ⋯) : WithZero ↥(valueGroup w)) : WithZero ↥(valueGroup w))

Tactic:
w.restrict_eq_mk ((eq_zero h.symm).ne.mpr ha)

Premises used: Iff.mpr, Set.Mem, Valuation.restrict_eq_mk, setOf, Valuation.IsEquiv.eq_zero, Iff.ne, Valuation.IsEquiv.symm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
⊢ Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
    ((↑(valueGroup.mk w 1 a ⋯ ⋯) : WithZero ↥(valueGroup w)) : WithZero ↥(valueGroup w))

Tactic:
exact w.restrict_eq_mk ((eq_zero h.symm).ne.mpr ha)

Premises used: Iff.mpr, Valuation.restrict_eq_mk, Valuation.IsEquiv.eq_zero, Iff.ne, Valuation.IsEquiv.symm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
h' : w.IsEquiv v
⊢ h.orderMonoidIso.symm = h'.orderMonoidIso

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
h₁ :
  ∀ (x : ValueGroup₀ v),
    Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
      ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
⊢ h.orderMonoidIso = OrderMonoidIso.refl (ValueGroup₀ v)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x : ValueGroup₀ v
h₁ :
  Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
h₂ :
  ∀ (x y : R) (w : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (w_1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    Eq (α := ValueGroup₀ v)
      ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v)
          (↑(valueGroup.mk v x y w w_1) : WithZero ↥(valueGroup v)) :
        ValueGroup₀ v)
      ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v)
          (↑(valueGroup.mk v x y w w_1) : WithZero ↥(valueGroup v)) :
        ValueGroup₀ v)
⊢ Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)

Tactic:
obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
⊢ Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x y : R
w : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
w_1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ Eq (α := ValueGroup₀ v)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v)
        (↑(valueGroup.mk v x y w w_1) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v)
        (↑(valueGroup.mk v x y w w_1) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)

Tactic:
simp [orderMonoidIso, valueGroup₀Fun_spec]

Premises used: Valuation.IsEquiv.orderMonoidIso, Valuation.IsEquiv.valueGroup₀Fun_spec
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : LinearOrderedCommGroupWithZero Γ''₀
inst_3 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
h₁ :
  ∀ (x : ValueGroup₀ v),
    Eq.{u_6 + 1} (α := ValueGroup₀ u)
      ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) x : ValueGroup₀ u)
      ((⋯.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) x : ValueGroup₀ u)
⊢ h.orderMonoidIso.trans h'.orderMonoidIso = ⋯.orderMonoidIso

Tactic:
ext x
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : LinearOrderedCommGroupWithZero Γ''₀
inst_3 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
x : ValueGroup₀ v
h₁ :
  Eq.{u_6 + 1} (α := ValueGroup₀ u) ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) 0)
    ((⋯.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) 0)
h₂ :
  ∀ (x y : R) (w_1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (w_2 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    Eq.{u_6 + 1} (α := ValueGroup₀ u)
      ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u)
          (↑(valueGroup.mk v x y w_1 w_2) : WithZero ↥(valueGroup v)) :
        ValueGroup₀ u)
      ((⋯.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u)
          (↑(valueGroup.mk v x y w_1 w_2) : WithZero ↥(valueGroup v)) :
        ValueGroup₀ u)
⊢ Eq.{u_6 + 1} (α := ValueGroup₀ u)
    ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) x : ValueGroup₀ u)
    ((⋯.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) x : ValueGroup₀ u)

Tactic:
obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : LinearOrderedCommGroupWithZero Γ''₀
inst_3 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
⊢ Eq.{u_6 + 1} (α := ValueGroup₀ u) ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) 0)
    ((⋯.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : LinearOrderedCommGroupWithZero Γ''₀
inst_3 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
x y : R
w_1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
w_2 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ Eq.{u_6 + 1} (α := ValueGroup₀ u)
    ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u)
        (↑(valueGroup.mk v x y w_1 w_2) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ u)
    ((⋯.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u)
        (↑(valueGroup.mk v x y w_1 w_2) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ u)

Tactic:
simp [orderMonoidIso, valueGroup₀Fun_spec]

Premises used: Valuation.IsEquiv.orderMonoidIso, Valuation.IsEquiv.valueGroup₀Fun_spec
-- 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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
inl :
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) 0 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) 0 : Γ'₀)
inr :
  ∀ (hy : y ≠ 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) 0 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) 0 : Γ'₀)

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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
hy : y ≠ 0
inr : LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
inr₁ : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)

Tactic:
rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_one₀]

Premises used: Valuation.map_div, div_le_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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
hy : y ≠ 0
inr : Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀) (0 : Γ'₀)
inr₁ inr₂ inr₃ inr₄ : y ≠ 0
⊢ LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)

Tactic:
rwa [zero_lt_iff, ne_zero_iff]

Premises used: Valuation.ne_zero_iff, zero_lt_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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
hy : y ≠ 0
inr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) (0 : Γ₀)
inr₁ inr₂ inr₃ inr₄ : y ≠ 0
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)

Tactic:
rwa [zero_lt_iff, ne_zero_iff]

Premises used: Valuation.ne_zero_iff, zero_lt_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 Γ'₀
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
⟨IsEquiv.le_one_iff_le_one, isEquiv_of_val_le_one⟩

Premises used: Valuation.isEquiv_of_val_le_one, Iff.intro, Valuation.IsEquiv.le_one_iff_le_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 Γ'₀
mp :
  v.IsEquiv v' →
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
mpr :
  (∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) →
    v.IsEquiv v'
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      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 : v.IsEquiv v'
x : K
mp mp₁ :
  Eq.{u_5 + 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:
rw [h.eq_one_iff_eq_one]

Premises used: Valuation.IsEquiv.eq_one_iff_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},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
mpr :
  ∀ (x : K),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v'

Tactic:
apply isEquiv_of_val_le_one

Premises used: Valuation.isEquiv_of_val_le_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
mpr :
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) →
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
mpr₁ :
  LE.le.{u_5} (α := Γ'₀) ((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_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 :
  ∀ {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 : Γ₀)
mpr :
  ∀ (hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
mpr₁ :
  ∀ (hx' : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)
⊢ Eq.{u_4 + 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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)
⊢ Eq.{u_4 + 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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 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