α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ (x : α) (_ : x ∈ s₁), t x) ⊆ ⋃ (x : α) (_ : x ∈ s₂ ∪ s₁ \ s₂), t x
α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ ((⋃ (x : α) (_ : x ∈ s₁), t x) \ ⋃ (x : α) (_ : x ∈ s₂), t x) ⊆ ⋃ (x : α) (_ : x ∈ s₁ \ s₂), t x
simp only [diff_subset_iff, ← biUnion_union]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂
α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ (x : α) (_ : x ∈ s₁), t x) ⊆ ⋃ (x : α) (_ : x ∈ s₂ ∪ s₁ \ s₂), t x
apply biUnion_subset_biUnion_left
case h
α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁
case h
α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂
rw [union_diff_self]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.298193
ι : Sort ?u.298196
ι' : Sort ?u.298199
ι₂ : Sort ?u.298202
κ : ι → Sort ?u.298207
κ₁ : ι → Sort ?u.298212
κ₂ : ι → Sort ?u.298217
κ' : ι' → Sort ?u.298222
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁
apply subset_union_right