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
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
⊢ False
have inr : ∀
  (this :
    ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
      (h' :
        LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)
          (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
      (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False)
  (vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
Tactic: wlog vyx : v y < v x generalizing x y
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
inr :
  ∀
    (this :
      ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
        (h' :
          LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)
            (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
        (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False)
    (vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
⊢ False
have wlog : ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
  (h' :
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
  (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
Tactic: wlog vyx : v y < v x generalizing x y
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
this :
  ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
    (h' :
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
    (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ False
have inr : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) (max ((v : (a : R) → Γ₀) y) ((v : (a : R) → Γ₀) x) : Γ₀)
Tactic: refine this h.symm ?_ (h.lt_or_gt.resolve_right vyx)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
this :
  ∀ {x y : R} (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
    (h' :
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀))
    (vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)), False
vyx : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) (max ((v : (a : R) → Γ₀) y) ((v : (a : R) → Γ₀) x) : Γ₀)
have inr : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) y) ((v : (a : R) → Γ₀) x) : Γ₀)
Tactic: rwa [add_comm, max_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ False
have h'₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [max_eq_left_of_lt vyx] at h'
Cleared hypotheses: h', vyx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ False
have apply : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: apply lt_irrefl (v x)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h' : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
vyx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have v₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (x + y - y) : Γ₀)
Tactic: calc
    v x = v (x + y - y) := by simp
    _ ≤ max (v <| x + y) (v y) := map_sub _ _ _
    _ < v x := max_lt h' vyx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀)
Tactic: rw [sub_eq_add_neg, map_add_eq_of_lt_right, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
have inl : ∀ (h0 : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
Tactic: rcases eq_or_ne (v (f j)) 0 with h0 | h0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
inl :
  ∀ (h0 : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
have inr : ∀ (h0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
Tactic: rcases eq_or_ne (v (f j)) 0 with h0 | h0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst_2 : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
h0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (∑ i ∈ s, f i) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
have inr : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (f j + ∑ x ∈ s \ {j}, f x) : Γ₀) ((v : (a : R) → Γ₀) (f j) : Γ₀)
Tactic: rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hj]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [sub_eq_add_neg, map_add_eq_of_lt_left]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀)
  (max ((v : (a : R) → Γ₀) (y - x)) ((v : (a : R) → Γ₀) x) : Γ₀)
Tactic: have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
this :
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀)
    (max ((v : (a : R) → Γ₀) (y - x)) ((v : (a : R) → Γ₀) x) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have this₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [max_eq_right (le_of_lt h)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have pos : ∀ (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: by_cases hy : v y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
pos :
  ∀ (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have neg : ∀ (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: by_cases hy : v y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [map_sub_swap, map_sub_of_left_eq_zero v hy]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [map_sub_swap, map_sub_of_left_eq_zero v hy]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - -y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: rw [← sub_neg_eq_add, map_sub_of_left_eq_zero v hx, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - -y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: rw [← sub_neg_eq_add, map_sub_of_left_eq_zero v hx, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - -y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have rw₂ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: rw [← sub_neg_eq_add, map_sub_of_left_eq_zero v hx, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [add_comm, map_add_of_left_eq_zero v hy]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (y + x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [add_comm, map_add_of_left_eq_zero v hy]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
have h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀)
Tactic: rw [← v.map_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (1 - x) : Γ₀) (1 : Γ₀)
have h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (-x) : Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀)
Tactic: rw [← v.map_one, ← v.map_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (1 + -x) : Γ₀) (1 : Γ₀)
Tactic: rw [sub_eq_add_neg 1 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 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
ν : Valuation R Γ₀
⊢ map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ (map (↑f : Γ₀ →*₀ Γ'₀) ⋯ ν) = ν
have h : ∀ (r : R),
  Eq.{u_4 + 1} (α := Γ₀) ((map (↑f.symm : Γ'₀ →*₀ Γ₀) sorry (map (↑f : Γ₀ →*₀ Γ'₀) sorry ν) : (a : R) → Γ₀) r : Γ₀)
    ((ν : (a : R) → Γ₀) r : Γ₀)
Tactic: ext
-- 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 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
ν : Valuation R Γ'₀
⊢ map (↑f : Γ₀ →*₀ Γ'₀) ⋯ (map (↑f.symm : Γ'₀ →*₀ Γ₀) ⋯ ν) = ν
have h : ∀ (r : R),
  Eq.{u_5 + 1} (α := Γ'₀) ((map (↑f : Γ₀ →*₀ Γ'₀) sorry (map (↑f.symm : Γ'₀ →*₀ Γ₀) sorry ν) : (a : R) → Γ'₀) r : Γ'₀)
    ((ν : (a : R) → Γ'₀) r : Γ'₀)
Tactic: ext
-- 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 : 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
⊢ LE.le.{u_4} (α := Γ₀) (ZeroHom.toFun (↑1 : ZeroHom R Γ₀) (x + y))
    (max (ZeroHom.toFun (↑1 : ZeroHom R Γ₀) x) (ZeroHom.toFun (↑1 : ZeroHom R Γ₀) y))
have 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)
Tactic: simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe,
        MonoidWithZeroHom.one_apply_def, le_sup_iff]
-- 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 : 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
⊢ 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)
have pos : x + y = 0 → x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 0 0 ∨ LE.le.{u_4} (α := Γ₀) 0 0
Tactic: split_ifs
-- 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 : 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
⊢ 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)
have neg : x + y = 0 → x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 0 ∨ LE.le.{u_4} (α := Γ₀) 0 1
Tactic: split_ifs
-- 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 : 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
⊢ 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)
have pos₁ : x + y = 0 → ¬x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 0
Tactic: split_ifs
-- 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 : 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
⊢ 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)
have neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 1
Tactic: split_ifs