awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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) → Γ₀) x : Γ₀) (1 : Γ₀)
have mpr : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (-1 + (1 + x)) : Γ₀) (1 : Γ₀)
Tactic: rw [show x = -1 + (1 + x) by simp]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ₀)
have mpr : LE.le.{u_4} (α := Γ₀) (max ((v : (a : K) → Γ₀) (-1)) ((v : (a : K) → Γ₀) (1 + x)) : Γ₀) (1 : Γ₀)
Tactic: refine le_trans (v.map_add _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have hx'₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [← h] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mp : 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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr : (∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) →
  v.IsEquiv v'
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mp : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
  LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [h.lt_one_iff_lt_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 Γ'₀
⊢ (∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) →
    v.IsEquiv v'
have 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 : Γ'₀)
Tactic: rw [isEquiv_iff_val_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have pos : ∀ (hx : x = 0),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have neg : ∀ (hx : ¬x = 0),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ'₀)
have neg : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) →
  Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have neg₁ : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) →
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 : Γ₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have neg : ∀ (h_1 : ¬Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)), False
Tactic: by_contra h_1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 : Γ'₀)
⊢ False
have hh₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
Tactic: rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
Cleared hypotheses: hh, h_1, h_2
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 : Γ'₀)
⊢ False
have x₁ : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ∨
  LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀)
Tactic: cases ne_iff_lt_or_gt.1 h_1 with
      | inl h_2 => simpa [hh, lt_self_iff_false] using h.2 h_2
      | inr h_2 =>
          rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
          exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have neg : ∀ (h_1 : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)), False
Tactic: by_contra h_1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
h_1 : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h_2 : LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ False
have hh₁ : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x⁻¹ : Γ'₀) (1 : Γ'₀)
Tactic: rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
Cleared hypotheses: hh, h_1, h_2
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
h_1 : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False
have x₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨ LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: cases ne_iff_lt_or_gt.1 h_1 with
      | inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
      | inr h_2 =>
        rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
        exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)
have rw : (∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)) ↔
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)
Tactic: rw [isEquiv_iff_val_lt_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 y : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀),
      ∀ {x : K},
        LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LE.le.{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 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)].TFAE
have tfae_1_iff_2 : v.IsEquiv v' ↔
  ∀ {x y : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
Tactic: tfae_have 1 ↔ 2 := isEquiv_iff_val_lt_val
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
⊢ [v.IsEquiv v',
      ∀ {x y : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀),
      ∀ {x : K},
        LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LE.le.{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 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)].TFAE
have tfae_1_iff_3 : v.IsEquiv v' ↔
  ∀ {x : K},
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: tfae_have 1 ↔ 3 := isEquiv_iff_val_le_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ [v.IsEquiv v',
      ∀ {x y : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀),
      ∀ {x : K},
        LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LE.le.{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 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)].TFAE
have tfae_1_iff_4 : v.IsEquiv v' ↔
  ∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: tfae_have 1 ↔ 4 := isEquiv_iff_val_eq_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ [v.IsEquiv v',
      ∀ {x y : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀),
      ∀ {x : K},
        LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LE.le.{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 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)].TFAE
have tfae_1_iff_5 : v.IsEquiv v' ↔
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: tfae_have 1 ↔ 5 := isEquiv_iff_val_lt_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_5 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ [v.IsEquiv v',
      ∀ {x y : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀),
      ∀ {x : K},
        LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LE.le.{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 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)].TFAE
have tfae_1_iff_6 : v.IsEquiv v' ↔
  ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)
Tactic: tfae_have 1 ↔ 6 := isEquiv_iff_val_sub_one_lt_one
-- 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 : CommRing R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : Nontrivial Γ₀
inst_4 : NoZeroDivisors Γ₀
h : v.supp = ⊤
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (0 : Γ₀)
have rw : Membership.mem (γ := Ideal R) ⊤ 1
Tactic: rw [← mem_supp_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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 : CommRing R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : Nontrivial Γ₀
inst_4 : NoZeroDivisors Γ₀
x y : R
hxy : x * y ∈ v.supp
⊢ x ∈ v.supp ∨ y ∈ v.supp
have hxy₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀) (0 : Γ₀)
Tactic: simp only [mem_supp_iff] at hxy ⊢
Cleared hypotheses: hxy