awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ 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} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 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
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 1
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 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} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 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
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 1
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 0
neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 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} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 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
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 0 1 ∨ LE.le.{u_4} (α := Γ₀) 0 1
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 0
neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → LE.le.{u_4} (α := Γ₀) 1 0 ∨ LE.le.{u_4} (α := Γ₀) 1 1
pos₃ : ¬x + y = 0 → ¬x = 0 → y = 0 → LE.le.{u_4} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 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} (α := Γ₀) 1 1 ∨ LE.le.{u_4} (α := Γ₀) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
⊢ LE.le.{u_4} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw : LE.le.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1
Tactic: rw [one_apply_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
⊢ LE.le.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1
have pos : x = 0 → LE.le.{u_4} (α := Γ₀) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
x : R
pos : x = 0 → LE.le.{u_4} (α := Γ₀) 0 1
⊢ LE.le.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1
have neg : ¬x = 0 → LE.le.{u_4} (α := Γ₀) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
⊢ LT.lt.{u_4} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔ x = 0
have rw : LT.lt.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1 ↔ x = 0
Tactic: rw [one_apply_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
⊢ LT.lt.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1 ↔ x = 0
have pos : x = 0 → (LT.lt.{u_4} (α := Γ₀) 0 1 ↔ x = 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial R
inst_3 : NoZeroDivisors R
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : Nontrivial Γ₀
x : R
pos : x = 0 → (LT.lt.{u_4} (α := Γ₀) 0 1 ↔ x = 0)
⊢ LT.lt.{u_4} (α := Γ₀) (if x = 0 then 0 else 1) 1 ↔ x = 0
have neg : ¬x = 0 → (LT.lt.{u_4} (α := Γ₀) 1 1 ↔ x = 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
have pos : ∀ (h : x = 0),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
pos :
  ∀ (h : x = 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
have neg : ∀ (h : ¬x = 0),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
have pos : ∀ (h : x = 0),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
pos :
  ∀ (h : x = 0),
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
have neg : ∀ (h : ¬x = 0),
  LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
Tactic: by_cases h : x = 0
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x_1 : R
x_in : Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} x_1
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} (-x_1)
have rwa : (v : (a : R) → Γ₀) (-x_1) ≤ γ
Tactic: rwa [Set.mem_setOf, map_neg]
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x_1 : R
x_in : Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} x_1
rwa : (v : (a : R) → Γ₀) (-x_1) ≤ γ
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x ≤ γ} (-x_1)
have rwa₁ : (v : (a : R) → Γ₀) x_1 ≤ γ
Tactic: rwa [Set.mem_setOf, map_neg]
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have pos : ∀
  (H :
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
Tactic: by_cases H : v x ≠ 0 ∨ v y ≠ 0
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
pos :
  ∀
    (H :
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
      (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
        (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have neg : ∀
  (H :
    ¬(Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀))),
  LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
Tactic: by_cases H : v x ≠ 0 ∨ v y ≠ 0
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
H :
  Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have pos : ∀ (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
  LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
Tactic: rcases H with h | h
Cleared hypotheses: H
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
H :
  Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
pos :
  ∀ (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
      (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
        (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have pos₁ : ∀ (h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
Tactic: rcases H with h | h
Cleared hypotheses: H
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have pos : LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
  (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
    else
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) sorry) :
        WithZero ↥(valueGroup v)) :
    ValueGroup₀ v)
  (max
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : R) → Γ₀) x) sorry) sorry) :
        WithZero ↥(valueGroup v))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) sorry) :
          WithZero ↥(valueGroup v))) :
    ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, h, ↓reduceDIte]
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) (x + y) : ValueGroup₀ v)
    (max (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) x)
      (ZeroHom.toFun (↑(restrict₀ v) : ZeroHom R (ValueGroup₀ v)) y))
have pos : LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
  (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
    else
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) sorry) :
        WithZero ↥(valueGroup v)) :
    ValueGroup₀ v)
  (max
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) sorry) :
          WithZero ↥(valueGroup v)))
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : R) → Γ₀) y) sorry) sorry) :
        WithZero ↥(valueGroup v)) :
    ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, h, ↓reduceDIte]
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
          WithZero ↥(valueGroup v))
        (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have pos : ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
  (_ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) sorry) sorry) :
          WithZero ↥(valueGroup v))
        0 :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: split_ifs with H _ hy
-- 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 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x_1 y_1 x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
pos :
  ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
    (_ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      (max
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
            WithZero ↥(valueGroup v))
          0 :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) (x + y)) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) ⋯) ⋯) :
          WithZero ↥(valueGroup v))
        (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have neg : ∀ (H : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (0 : Γ₀))
  (_ : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
    (max
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) sorry) sorry) :
          WithZero ↥(valueGroup v))
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) _) sorry) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: split_ifs with H _ hy