internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
apply Icc_subset_Icc (by rw [nestedInterval, h]; dsimp only; linarith) (by rw [nestedInterval, h])
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ (nestedInterval U (n + 1)).1
Tactic:
rw [nestedInterval, h]
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
Tactic:
dsimp only
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U (n + 1)).2 ≤ (nestedInterval U n).2
Tactic:
rw [nestedInterval, h]
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested
Proof state before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ Icc (nestedInterval U j).1 (nestedInterval U j).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
rw [(Nat.add_sub_of_le hij).symm]
Proof state after:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ Icc (nestedInterval U (i + (j - i))).1 (nestedInterval U (i + (j - i))).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Theorem: Tutorial.nestedIntervalSeq_is_nested
Proof state before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ Icc (nestedInterval U (i + (j - i))).1 (nestedInterval U (i + (j - i))).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
set k := j - i
Proof state after:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k : ℕ := j - i
⊢ Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
Theorem: Tutorial.nestedIntervalSeq_is_nested
Proof state before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k : ℕ := j - i
⊢ Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
induction k with
| zero => apply rfl.subset
| succ k ih => intro x hx; apply ih (nestedIntervalSeq_is_nested_succ U (i + k) hx)
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested
Proof state before:
case zero
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k : ℕ := j - i
⊢ Icc (nestedInterval U (i + Nat.zero)).1 (nestedInterval U (i + Nat.zero)).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
apply rfl.subset
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested
Proof state before:
case succ
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k✝ : ℕ := j - i
k : ℕ
ih : Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
⊢ Icc (nestedInterval U (i + Nat.succ k)).1 (nestedInterval U (i + Nat.succ k)).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
intro x hx
Proof state after:
case succ
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k✝ : ℕ := j - i
k : ℕ
ih : Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
x : ℝ
hx : x ∈ Icc (nestedInterval U (i + Nat.succ k)).1 (nestedInterval U (i + Nat.succ k)).2
⊢ x ∈ Icc (nestedInterval U i).1 (nestedInterval U i).2
Theorem: Tutorial.nestedIntervalSeq_is_nested
Proof state before:
case succ
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k✝ : ℕ := j - i
k : ℕ
ih : Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
x : ℝ
hx : x ∈ Icc (nestedInterval U (i + Nat.succ k)).1 (nestedInterval U (i + Nat.succ k)).2
⊢ x ∈ Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
apply ih (nestedIntervalSeq_is_nested_succ U (i + k) hx)
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_mem
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ nestedIntervalSeq U n ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
simp only [mem_Icc, nestedIntervalSeq]
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Theorem: Tutorial.nestedIntervalSeq_mem
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Tactic:
have := nestedInterval_le U n
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Theorem: Tutorial.nestedIntervalSeq_mem
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Tactic:
split_ands <;> linarith
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
by_cases H : HasFinSubCover U (Icc (α n) ((α n + β n) / 2))
Proof state after:
case pos
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)

case neg
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
case pos =>
  rw [nestedInterval, nestedIntervalSucc_right H]
  apply not_HasFinSubCover_concat ?_ H
  apply nestedInterval_not_HasFinSubCover h n
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
case neg =>
  rw [nestedInterval, nestedIntervalSucc_left H]
  apply H
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
rw [nestedInterval, nestedIntervalSucc_right H]
Proof state after:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
        (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
        (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)
Tactic:
apply not_HasFinSubCover_concat ?_ H
Proof state after:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)
Tactic:
apply nestedInterval_not_HasFinSubCover h n
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
rw [nestedInterval, nestedIntervalSucc_left H]
Proof state after:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).1
        ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2)
Theorem: Tutorial.nestedInterval_not_HasFinSubCover
Proof state before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).1
        ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2)
Tactic:
apply H
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_len
Proof state before:
ι : Type
U : ι → Set ℝ
⊢ (nestedInterval U 0).2 - (nestedInterval U 0).1 = (2 ^ 0)⁻¹
Tactic:
simp [nestedInterval]
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_len
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U (n + 1)).2 - (nestedInterval U (n + 1)).1 = (2 ^ (n + 1))⁻¹
Tactic:
have ih := nestedInterval_len n
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
ih : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ (nestedInterval U (n + 1)).2 - (nestedInterval U (n + 1)).1 = (2 ^ (n + 1))⁻¹
Theorem: Tutorial.nestedInterval_len
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
ih : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ (nestedInterval U (n + 1)).2 - (nestedInterval U (n + 1)).1 = (2 ^ (n + 1))⁻¹
Tactic:
rcases nestedIntervalSucc_eq_or_eq U (α n) (β n) with H | H <;>
  rw [nestedInterval, H] <;> field_simp at ih ⊢ <;>
    calc _ = (β n - α n) * 2 ^ n * 2 := by ring
         _ = 2                       := by rw [ih]; ring
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_len
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ ((nestedInterval U n).2 * 2 - ((nestedInterval U n).1 + (nestedInterval U n).2)) * 2 ^ (n + 1) =
    ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n * 2
Tactic:
ring
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_len
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n * 2 = 2
Tactic:
rw [ih]
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ 1 * 2 = 2
Theorem: Tutorial.nestedInterval_len
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ 1 * 2 = 2
Tactic:
ring
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_isCauSeq_aux
Proof 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
Proof state after:
ι : Type
U : ι → Set ℝ
a b x y : ℝ
hx : a ≤ x ∧ x ≤ b
hy : a ≤ y ∧ y ≤ b
⊢ |y - x| ≤ b - a
Theorem: Tutorial.nestedIntervalSeq_isCauSeq_aux
Proof 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
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_isCauSeq_aux'
Proof 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)
Proof 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)⁻¹
Theorem: Tutorial.nestedIntervalSeq_isCauSeq_aux'
Proof 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
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof state before:
ι : Type
U : ι → Set ℝ
⊢ IsCauSeq abs (nestedIntervalSeq U)
Tactic:
intro ε ε0
Proof state after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof 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)
Proof state after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ε⁻¹ < 2 ^ i
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof 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
Proof state after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof 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
Proof state after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
⊢ ∀ j ≥ i, |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof 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
Proof state after:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
i : ℕ
hi✝ : ε⁻¹ < 2 ^ i
hi : (2 ^ i)⁻¹ < ε
j : ℕ
hj : j ≥ i
⊢ |nestedIntervalSeq U j - nestedIntervalSeq U i| < ε
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof 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
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_isCauSeq
Proof state before:
ι : Type
U : ι → Set ℝ
ε : ℝ
ε0 : ε > 0
⊢ 1 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_tendsto
Proof state before:
ι : Type
U : ι → Set ℝ
⊢ Tendsto (nestedIntervalSeq U) atTop (𝓝 (CauSeq.lim (nestedIntervalCauSeq U)))
Tactic:
apply (nestedIntervalCauSeq U).tendsto_limit
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
⊢ HasFinSubCover U (Icc 0 1)
Tactic:
by_contra H
Proof state after:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
⊢ False
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
⊢ False
Tactic:
set c := (nestedIntervalCauSeq U).lim
Proof state after:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
⊢ False
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
⊢ False
Tactic:
rcases cover (nestedIntervalLim_mem U 0) with ⟨_, ⟨i, rfl⟩, hU' : c ∈ U i⟩
Proof state after:
case intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
⊢ False
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
⊢ False
Tactic:
rcases Metric.isOpen_iff.mp (hU i) c hU' with ⟨ε, ε0, hε⟩
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ False
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ False
Tactic:
have ⟨n, hn⟩ : ∃ n : ℕ, (ε / 2)⁻¹ < 2 ^ n := by
  sorry
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ False
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ False
Tactic:
suffices HasFinSubCover U I(n) by
  sorry
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Tactic:
suffices I(n) ⊆ U i by
  sorry
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i