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

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
hac : HasFinSubCover U (Icc a c)
hcb : HasFinSubCover U (Icc c b)
⊢ HasFinSubCover U (Icc a b)
Tactic:
rcases hac with ⟨ι_ac, cover_ac⟩
State after:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
hcb : HasFinSubCover U (Icc c b)
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
⊢ HasFinSubCover U (Icc a b)

State before:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
hcb : HasFinSubCover U (Icc c b)
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
⊢ HasFinSubCover U (Icc a b)
Tactic:
rcases hcb with ⟨ι_cb, cover_cb⟩
State after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ HasFinSubCover U (Icc a b)

State before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ HasFinSubCover U (Icc a b)
Tactic:
exists ι_ac ∪ ι_cb
State after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ Icc a b ⊆ ⋃ i ∈ ι_ac ∪ ι_cb, U i

State before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ Icc a b ⊆ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Tactic:
intro x hx
State after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ x ∈ ⋃ i ∈ ι_ac ∪ ι_cb, U i

State before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ x ∈ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Tactic:
suffices ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i by
  simpa using this
State after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i

State before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
cases le_total x c
State after:
case intro.intro.inl
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
h✝ : x ≤ c
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i

case intro.intro.inr
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
h✝ : c ≤ x
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
case inl hxc =>
  obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_ac ∧ x ∈ U i := by simpa using cover_ac ⟨hx.left, hxc⟩
  exact ⟨i, Or.inl hi.1, hi.2⟩
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
case inr hxc =>
  obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_cb ∧ x ∈ U i := by simpa using cover_cb ⟨hxc, hx.right⟩
  exact ⟨i, Or.inr hi.1, hi.2⟩
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
this : ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
⊢ x ∈ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Tactic:
simpa using this
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_ac ∧ x ∈ U i := by simpa using cover_ac ⟨hx.left, hxc⟩
State after:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
i : ι
hi : i ∈ ι_ac ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i

State before:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
i : ι
hi : i ∈ ι_ac ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
exact ⟨i, Or.inl hi.1, hi.2⟩
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
⊢ ∃ i ∈ ι_ac, x ∈ U i
Tactic:
simpa using cover_ac ⟨hx.left, hxc⟩
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_cb ∧ x ∈ U i := by simpa using cover_cb ⟨hxc, hx.right⟩
State after:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
i : ι
hi : i ∈ ι_cb ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i

State before:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
i : ι
hi : i ∈ ι_cb ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
exact ⟨i, Or.inr hi.1, hi.2⟩
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
⊢ ∃ i ∈ ι_cb, x ∈ U i
Tactic:
simpa using cover_cb ⟨hxc, hx.right⟩
State after:
no goals