awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw : Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
  LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [zero_lt_iff, zero_lt_iff, h.eq_zero.ne]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw₁ : Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
  Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀)
Tactic: rw [zero_lt_iff, zero_lt_iff, h.eq_zero.ne]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ :
  Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw₂ : Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀) ↔
  Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀)
Tactic: rw [zero_lt_iff, zero_lt_iff, h.eq_zero.ne]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← le_iff_le_iff_lt_iff_lt, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀)
have rw₁ : LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← le_iff_le_iff_lt_iff_lt, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw₁ : LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₁ :
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw₂ : LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ LE.le.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
  LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← v₁.map_one, h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw₁ : LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
  LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← v₁.map_one, h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ :
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw₂ : LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
  LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← v₁.map_one, h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h.eq_iff, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw₁ : Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h.eq_iff, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₁ :
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw₂ : Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h.eq_iff, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw : LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h.lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw₁ : LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h.lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₁ :
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have rw₂ : LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [← v₁.map_one, h.lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw : LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
  LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← v₁.map_one, h.lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw₁ : LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
  LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← v₁.map_one, h.lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ :
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
have rw₂ : LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
  LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
Tactic: rw [← v₁.map_one, h.lt_iff_lt, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
⊢ v.IsEquiv v' ↔
    ∀ {x y : R},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) ((v' : (a : R) → Γ'₀) y : Γ'₀)
have simp : (∀ (r s : R),
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) s : Γ'₀) ((v' : (a : R) → Γ'₀) r : Γ'₀)) ↔
  ∀ {x y : R},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) ((v' : (a : R) → Γ'₀) y : Γ'₀)
Tactic: simp only [IsEquiv, le_iff_le_iff_lt_iff_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
h : v.IsEquiv v'
hv : v.IsNontrivial
⊢ v'.IsNontrivial
have obtain : ∀ (x : R)
  (hx :
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)),
  v'.IsNontrivial
Tactic: obtain ⟨x, hx⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
h : v.IsEquiv v'
x : R
hx :
  Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ v'.IsNontrivial
have h₁ : Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀) ∧
  Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: use x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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
r s : R
hr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hs : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀)
⊢ h.valueGroup₀Fun (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v)) =
    (↑(valueGroup.mk w r s ⋯ ⋯) : WithZero ↥(valueGroup w))
have rw : Eq (α := ValueGroup₀ w)
  (have c :=
    sorry.choose (p :=
      fun
        (d :
          { xy : R × R //
            Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
              Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
      Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
        (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)));
  (↑(valueGroup.mk w (↑c : R × R).1 (↑c : R × R).2 sorry sorry) : WithZero ↥(valueGroup w)))
  (↑(valueGroup.mk w r s sorry sorry) : WithZero ↥(valueGroup w))
Tactic: rw [valueGroup₀Fun, dif_neg (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ v
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x
have inl : x = 0 → sorry.valueGroup₀Fun (h.valueGroup₀Fun x) = x
Tactic: obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ v
inl : x = 0 → ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x
have inr : ∀ (r₁ s₁ : R) (hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀))
  (hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)),
  sorry.valueGroup₀Fun (h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))) =
    (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))
Tactic: obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ w
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x
have inl : x = 0 → h.valueGroup₀Fun (sorry.valueGroup₀Fun x) = x
Tactic: obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ w
inl : x = 0 → h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x
have inr : ∀ (r₁ s₁ : R) (hr₁ : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) r₁ : Γ'₀) (0 : Γ'₀))
  (hs₁ : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) s₁ : Γ'₀) (0 : Γ'₀)),
  h.valueGroup₀Fun (sorry.valueGroup₀Fun (↑(valueGroup.mk w r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup w))) =
    (↑(valueGroup.mk w r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup w))
Tactic: obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
⊢ h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y
have inl : x = 0 → h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y
Tactic: obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
inl : x = 0 → h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y
⊢ h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y
have inr : ∀ (r₁ s₁ : R) (hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀))
  (hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)),
  h.valueGroup₀Fun ((↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * y) =
    h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * h.valueGroup₀Fun y
Tactic: obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
Cleared hypotheses: x