Theorem: Tutorial.HasFinSubCover_of_Icc (Solution/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
  apply pow_unbounded_of_one_lt (ε / 2)⁻¹ (by linarith)
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
  apply nestedInterval_not_HasFinSubCover H n this
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
  exists {i}
  simpa using this
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
  intro x hx
  apply hε (this x hx)
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:
intro x hx
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 : ℝ
hx : 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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ |x - c| < ε
Tactic:
have hba : β n - α n = (2 ^ n : ℝ)⁻¹ := nestedInterval_len U n
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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ |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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ |x - c| < ε
Tactic:
have hn := inv_lt_of_inv_lt (by linarith) hn
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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ 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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
⊢ |x - c| < ε
Tactic:
have hc : α n ≤ c ∧ c ≤ β n := nestedIntervalLim_mem U n
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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (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 : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
⊢ |x - c| < ε
Tactic:
have hx : α n ≤ x ∧ x ≤ β n := hx
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 : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (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 : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - c| < ε
Tactic:
calc |x - c|
  _ = |(x - α n) - (c - α n)| := by simp
  _ ≤ |x - α n| + |c - α n| := by apply abs_sub
  _ = (x - α n) + (c - α n) := by
    apply congrArg₂ <;> rw [abs_eq_self] <;> linarith
  _ < ε / 2 + ε / 2 := by linarith
  _ = ε := by ring
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:
apply pow_unbounded_of_one_lt (ε / 2)⁻¹ (by linarith)
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
⊢ 1 < 2
Tactic:
linarith
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:
apply nestedInterval_not_HasFinSubCover H n this
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:
exists {i}
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)
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
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ ⋃ i_1 ∈ {i}, U i_1

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
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ ⋃ i_1 ∈ {i}, U i_1
Tactic:
simpa using this
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:
intro x hx
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)
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| < ε
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ x ∈ U i

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| < ε
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ x ∈ U i
Tactic:
apply hε (this x hx)
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
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ 0 < ε / 2
Tactic:
linarith
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
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - c| = |x - (nestedInterval U n).1 - (c - (nestedInterval U n).1)|
Tactic:
simp
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
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - (nestedInterval U n).1 - (c - (nestedInterval U n).1)| ≤
    |x - (nestedInterval U n).1| + |c - (nestedInterval U n).1|
Tactic:
apply abs_sub
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
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - (nestedInterval U n).1| + |c - (nestedInterval U n).1| =
    x - (nestedInterval U n).1 + (c - (nestedInterval U n).1)
Tactic:
apply congrArg₂ <;> rw [abs_eq_self] <;> linarith
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
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ x - (nestedInterval U n).1 + (c - (nestedInterval U n).1) < ε / 2 + ε / 2
Tactic:
linarith
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
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
State after:
no goals