Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: 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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
⊢ ((if x + y = 0 then 0 else 1) ≤ if x = 0 then 0 else 1) ∨ (if x + y = 0 then 0 else 1) ≤ if y = 0 then 0 else 1

Tactic:
split_ifs

Goal state after:
case pos
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : x + y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 ≤ 0 ∨ 0 ≤ 0

case neg
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : x + y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 0 ∨ 0 ≤ 1

case pos
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : x + y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 0 ≤ 1 ∨ 0 ≤ 0

case neg
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : x + y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1 ∨ 0 ≤ 1

case pos
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : ¬x + y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 ≤ 0 ∨ 1 ≤ 0

case neg
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : ¬x + y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 1 ≤ 0 ∨ 1 ≤ 1

case pos
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : ¬x + y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 1 ≤ 1 ∨ 1 ≤ 0

case neg
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✝⁶ : Ring R
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ₀
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x✝ y✝ : R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x y : R
h✝² : ¬x + y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 1 ≤ 1 ∨ 1 ≤ 1