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

State before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ |nestedIntervalSeq U j - nestedIntervalSeq U i| ≤ (2 ^ i)⁻¹
Tactic:
have := nestedIntervalSeq_isCauSeq_aux (nestedIntervalSeq_mem U i) (nestedIntervalSeq_mem_of_le U hij)
State after:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
this : |nestedIntervalSeq U j - nestedIntervalSeq U i| ≤ (nestedInterval U i).2 - (nestedInterval U i).1
⊢ |nestedIntervalSeq U j - nestedIntervalSeq U i| ≤ (2 ^ i)⁻¹

State before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
this : |nestedIntervalSeq U j - nestedIntervalSeq U i| ≤ (nestedInterval U i).2 - (nestedInterval U i).1
⊢ |nestedIntervalSeq U j - nestedIntervalSeq U i| ≤ (2 ^ i)⁻¹
Tactic:
simpa [nestedInterval_len] using this
State after:
no goals