-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem trichotomy (f : CauSeq α abs) : Pos f ∨ LimZero f ∨ Pos (-f)

Proof state:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0

Tactic:
rw [abs_of_nonpos h] at h₁

Result:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0

Proof state:
case inr.intro.intro.intro.refine_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ ↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j

Tactic:
exact
  (le_add_iff_nonneg_right _).1
    (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑f j

Tactic:
rwa [abs_of_nonneg] at this

Result:
case inr.intro.intro.intro.refine_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
rcases Classical.em (LimZero f) with h | h <;> simp [*]

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬f.LimZero
⊢ f.Pos ∨ (-f).Pos

Proof state:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j - ?inr.intro.intro.intro.refine_2.intro ≤ -?inr.intro.intro.intro.refine_2.intro

case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ α

Tactic:
exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
⊢ f.Pos ∨ (-f).Pos

Tactic:
rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩

Result:
case inr.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
⊢ f.Pos ∨ (-f).Pos

Proof state:
case inr.intro.intro.intro.refine_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j

Tactic:
rw [abs_of_nonneg h] at h₁

Result:
case inr.intro.intro.intro.refine_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ ↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j

Proof state:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0

Tactic:
rw [← sub_le_sub_iff_right, zero_sub]

Result:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j - ?inr.intro.intro.intro.refine_2.intro ≤ -?inr.intro.intro.intro.refine_2.intro

case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ α

Proof state:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j

Tactic:
rwa [abs_of_nonpos] at this

Result:
case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬f.LimZero
⊢ f.Pos ∨ (-f).Pos

Tactic:
rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩

Result:
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
⊢ f.Pos ∨ (-f).Pos

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
⊢ f.Pos ∨ (-f).Pos

Tactic:
refine (le_total 0 (f i)).imp ?_ ?_ <;>
  refine fun h => ⟨K, K0, i, fun j ij => ?_⟩ <;>
  have := (hi _ ij).1 <;>
  obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Result:
case inr.intro.intro.intro.refine_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑f j

case inr.intro.intro.intro.refine_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j