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

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
State after:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
⊢ False

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
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

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⟩
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

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ε⟩
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

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
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

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
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)

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
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

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
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Tactic:
suffices ∀ x, x ∈ I(n) → |x - c| < ε by
  sorry
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
⊢ ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε

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
⊢ ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
Tactic:
sorry
State after:
no goals

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)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ ∃ n, (ε / 2)⁻¹ < 2 ^ n
Tactic:
sorry
State after:
no goals

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)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
⊢ False
Tactic:
sorry
State after:
no goals

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)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Tactic:
sorry
State after:
no goals

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)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Tactic:
sorry
State after:
no goals