case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
⊢ a ⊔ b ≈ b

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ a ⊔ b ≈ b
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊔ b ≈ b
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abs (↑(a ⊔ b - b) j) < ε✝
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
⊢ a ⊔ b ≈ b
intro _ _
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ abs (↑(a ⊔ b - b) j) < ε✝
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abs (↑(a ⊔ b - b) j) < ε✝
refine' ⟨i, fun j hj => _⟩
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ abs (↑a j ⊔ ↑b j - ↑b j) < ε✝
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ abs (↑(a ⊔ b - b) j) < ε✝
dsimp
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ abs (max (↑a j - ↑b j) (↑b j - ↑b j)) < ε✝
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ abs (↑a j ⊔ ↑b j - ↑b j) < ε✝
erw [← max_sub_sub_right]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j - ↑b j ≤ 0
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ abs (max (↑a j - ↑b j) (↑b j - ↑b j)) < ε✝
rwa [sub_self, max_eq_right, abs_zero]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑b j - ↑a j
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j - ↑b j ≤ 0
rw [sub_nonpos, ← sub_nonneg]
no goals
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑b j - ↑a j
exact ε0.le.trans (h _ hj)
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ b ⊔ b ≈ b
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ a ⊔ b ≈ b
refine' Setoid.trans (sup_equiv_sup h (Setoid.refl _)) _
no goals
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ b ⊔ b ≈ b
rw [CauSeq.sup_idem]