case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
cases hs
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ range f), t i
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
refine' ⟨range f, finite_range f, fun x hx => _⟩
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ range f), t i
rw [biUnion_range, mem_iUnion]
no goals
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)
exact ⟨⟨x, hx⟩, hf _⟩
no goals
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
⊢ ∀ (x : ↑s), ∃ i, ↑x ∈ t i
simpa [subset_def] using h