ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ (¬∀ (i : ι), ∃ x, i ∈ s → x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi s t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ (∃ i, ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ (¬∀ (i : ι), ∃ x, i ∈ s → x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
push_neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ (∃ i, ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
refine' exists_congr fun i => _
no goals
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.122847
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
cases isEmpty_or_nonempty (α i) <;> simp [*, forall_and, eq_empty_iff_forall_not_mem]