Theorem: Tutorial.nestedIntervalSeq_isCauSeq_aux (Tutorial/Advanced/Analysis/Lecture3.lean)

State before:
ι : Type
U : ι → Set ℝ
a b x y : ℝ
hx : x ∈ Icc a b
hy : y ∈ Icc a b
⊢ |y - x| ≤ b - a
Tactic:
dsimp [Icc] at hx hy
State after:
ι : Type
U : ι → Set ℝ
a b x y : ℝ
hx : a ≤ x ∧ x ≤ b
hy : a ≤ y ∧ y ≤ b
⊢ |y - x| ≤ b - a

State before:
ι : Type
U : ι → Set ℝ
a b x y : ℝ
hx : a ≤ x ∧ x ≤ b
hy : a ≤ y ∧ y ≤ b
⊢ |y - x| ≤ b - a
Tactic:
apply (abs_sub_le_iff.2 ⟨_, _⟩) <;> linarith
State after:
no goals