α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
⊢ (⋃ (i : ι), s i) ⊆ ⋃ (i : ι) (_ : i ∈ t), s i
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
⊢ Set.Finite (⋃ (i : ι), s i)
suffices (⋃ i, s i) ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
⊢ (⋃ (i : ι), s i) ⊆ ⋃ (i : ι) (_ : i ∈ t), s i
refine' iUnion_subset fun i x hx => _
case pos
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i

case neg
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : ¬i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
by_cases hi : i ∈ t
no goals
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
this : (⋃ (i : ι), s i) ⊆ ⋃ (i : ι) (_ : i ∈ t), s i
⊢ Set.Finite (⋃ (i : ι), s i)
exact (ht.biUnion hs).subset this
no goals
case pos
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
exact mem_biUnion hi hx
case neg
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : False
hi : ¬i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
case neg
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : ¬i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
rw [he i hi, mem_empty_iff_false] at hx
no goals
case neg
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : False
hi : ¬i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
contradiction