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

State before:
ι : Type
U : ι → Set ℝ
⊢ IsCauSeq abs (nestedIntervalSeq U)
Tactic:
intro ε ε0
State after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε

State before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Tactic:
have ⟨i, hi⟩ : ∃ i : ℕ, ε⁻¹ < 2 ^ i := pow_unbounded_of_one_lt ε⁻¹ (by linarith)
State after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ε⁻¹ < 2 ^ i
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε

State before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ε⁻¹ < 2 ^ i
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Tactic:
have hi : (2 ^ i : ℝ)⁻¹ < ε := inv_lt_of_inv_lt ε0 hi
State after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε

State before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Tactic:
exists i
State after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
⊢ ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε

State before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
⊢ ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Tactic:
intro j hj
State after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
j : ℕ
hj : j ≥ i
⊢ |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε

State before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
j : ℕ
hj : j ≥ i
⊢ |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Tactic:
calc |nestedIntervalSeq U j - nestedIntervalSeq U i|
  _ ≤ (2 ^ i : ℝ)⁻¹ := nestedIntervalSeq_isCauSeq_aux' U hj
  _ < ε             := hi
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
⊢ 1 < 2
Tactic:
linarith
State after:
no goals