α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ h, x ∈ t h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then ∅ else t h) ↔ ∃ h, x ∈ t h
simp only [mem_dite, mem_empty_iff_false, imp_false]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ h, x ∈ t h
exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩