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
Γ''₀ : 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.orderMonoidIso.trans h'.orderMonoidIso = ⋯.orderMonoidIso
have h₁ : ∀ (x : ValueGroup₀ v),
  Eq.{u_6 + 1} (α := ValueGroup₀ u)
    ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) x : ValueGroup₀ u)
    ((sorry.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) x : ValueGroup₀ u)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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
⊢ 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)
have h₁ : Eq.{u_6 + 1} (α := ValueGroup₀ u) ((h.orderMonoidIso.trans h'.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) 0)
  ((sorry.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u) 0)
Tactic: obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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)
⊢ 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)
have 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)
    ((sorry.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ u)
        (↑(valueGroup.mk v x y w_1 w_2) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ u)
Tactic: obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
Cleared hypotheses: x
-- 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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
have 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 : Γ'₀)
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- 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),
    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 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
have 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 : Γ'₀)
Tactic: obtain rfl | hy := eq_or_ne y 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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
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 : Γ'₀)
have inr : LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
Tactic: rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_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),
    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 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
have inr₁ : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
Tactic: rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
hy : y ≠ 0
⊢ LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
have inr : Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀) (0 : Γ'₀)
Tactic: rwa [zero_lt_iff, ne_zero_iff]
-- 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),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x y : K
hy : y ≠ 0
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
have inr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) (0 : Γ₀)
Tactic: rwa [zero_lt_iff, ne_zero_iff]
-- 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},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mp : 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
-- 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},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr : (∀ {x : K},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((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
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mp : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
  Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: rw [h.eq_one_iff_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},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v'
have mpr : ∀ (x : K),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
Tactic: apply isEquiv_of_val_le_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},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr : LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) →
  LE.le.{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 Γ'₀
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 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr₁ : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀) →
  LE.le.{u_4} (α := Γ₀) ((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},
    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 : Γ₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr : ∀ (hx' : LT.lt.{u_4} (α := Γ₀) ((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'
-- 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_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 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr₁ : ∀ (hx' : Eq.{u_4 + 1} (α := Γ₀) ((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'
-- 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_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 : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)
Tactic: rw [← v.map_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},
    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) : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)
have h₁ : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)
Tactic: apply map_add_eq_of_lt_left
-- 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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have this : 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
-- 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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have this₁ : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
Tactic: rw [h] at this
Cleared hypotheses: this
-- 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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have mpr : LE.le.{u_5} (α := Γ'₀) ((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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (-1 + (1 + x)) : Γ'₀) (1 : Γ'₀)
have mpr : LE.le.{u_5} (α := Γ'₀) (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_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
have hx'₁ : Eq.{u_5 + 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 Γ'₀
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 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have mpr : ∀ (hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases lt_or_eq_of_le hx with hx' | hx'
-- 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 : Γ'₀)
mpr :
  ∀ (hx' : LT.lt.{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 : Γ₀)
have mpr₁ : ∀ (hx' : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases lt_or_eq_of_le hx with hx' | hx'
-- 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 : Γ'₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
have rw : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)
Tactic: rw [← v'.map_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},
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
x : K
hx : LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
hx' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)
have h₁ : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) 1 : Γ'₀)
Tactic: apply map_add_eq_of_lt_left
-- 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' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
Tactic: have : v' (1 + x) = 1 := by
          rw [← v'.map_one]
          apply map_add_eq_of_lt_left
          simpa
-- 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' : LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
this : Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (1 + x) : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have this₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (1 + x) : Γ₀) (1 : Γ₀)
Tactic: rw [← h] at this
Cleared hypotheses: this