case inr
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
⊢ Pos f ∨ Pos (-f)
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
⊢ Pos f ∨ LimZero f ∨ Pos (-f)
cases' Classical.em (LimZero f) with h h <;> simp [*]
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
⊢ Pos f ∨ Pos (-f)
case inr
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
⊢ Pos f ∨ Pos (-f)
rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
case inr.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
⊢ Pos f ∨ Pos (-f)
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
⊢ Pos f ∨ Pos (-f)
rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑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✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ K ≤ ↑(-f) j
case inr.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
⊢ Pos f ∨ Pos (-f)
refine' (le_total 0 (f i)).imp _ _ <;>
  refine' fun h => ⟨K, K0, i, fun j ij => _⟩ <;>
  have := (hi _ ij).1 <;>
  cases' hi _ le_rfl with h₁ h₂
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ 0 ≤ ↑f j
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ K ≤ ↑f j
rwa [abs_of_nonneg] at this
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ ↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ 0 ≤ ↑f j
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ 0 ≤ ↑f j
rw [abs_of_nonneg h] at h₁
no goals
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ ↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ 0 ≤ ↑f j
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)
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ ↑f j ≤ 0
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ K ≤ ↑(-f) j
rwa [abs_of_nonpos] at this
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ ↑f j ≤ 0
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ abs (↑f i)
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ ↑f j ≤ 0
rw [abs_of_nonpos h] at h₁
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑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✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ α
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ ↑f j ≤ 0
rw [← sub_le_sub_iff_right, zero_sub]
no goals
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑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✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ abs (↑f j) ∧ ∀ (k : ℕ), k ≥ j → abs (↑f k - ↑f j) < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ abs (↑f j)
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → abs (↑f k - ↑f i) < K
⊢ α
exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁