α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
⊢ (∀ (x : α), x ∈ u → x ∈ Set.ite t s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
⊢ u ⊆ Set.ite t s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
simp only [subset_def, ← forall_and]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ Set.ite t s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
⊢ (∀ (x : α), x ∈ u → x ∈ Set.ite t s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
refine' forall_congr' fun x => _
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ Set.ite t s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
by_cases hx : x ∈ t <;> simp [*, Set.ite]