Theorem: LoVe.id_Not_CauchySeq (LoVe/Lectures/LoVe14_RationalAndRealNumbers_Demo.lean)

State before:
⊢ ¬IsCauchySeq fun n => ↑n
Tactic:
rw [IsCauchySeq]
State after:
⊢ ¬∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε

State before:
⊢ ¬∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
Tactic:
intro h
State after:
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
⊢ False

State before:
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
⊢ False
Tactic:
cases h 1 zero_lt_one with
| intro i hi =>
  have hi_succi :=
    hi (i + 1) (by simp)
  simp [←sub_sub] at hi_succi
State after:
no goals

State before:
case intro
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
⊢ False
Tactic:
have hi_succi :=
  hi (i + 1) (by simp)
State after:
case intro
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
hi_succi : |↑i - ↑(i + 1)| < 1
⊢ False

State before:
case intro
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
hi_succi : |↑i - ↑(i + 1)| < 1
⊢ False
Tactic:
simp [←sub_sub] at hi_succi
State after:
no goals

State before:
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
⊢ i + 1 ≥ i
Tactic:
simp
State after:
no goals