-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sup_eq_right {a b : CauSeq α abs} (h : a ≤ b) : a ⊔ b ≈ b

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ a ⊔ b ≈ b

Tactic:
refine Setoid.trans (sup_equiv_sup h (Setoid.refl _)) ?_

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ b ⊔ b ≈ b

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ b ⊔ b ≈ b

Tactic:
rw [CauSeq.sup_idem]

Result:
no goals

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

Tactic:
rw [← max_sub_sub_right]

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

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

Tactic:
exact ε0.le.trans (h _ hj)

Result:
no goals

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

Tactic:
refine ⟨i, fun j hj => ?_⟩

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

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

Tactic:
intro _ _

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

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊔ b ≈ b

Tactic:
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ 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

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

Tactic:
rwa [sub_self, max_eq_right, abs_zero]

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

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

Tactic:
rw [sub_nonpos, ← sub_nonneg]

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

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

Tactic:
dsimp

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