case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : p
⊢ x ∈ s hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h

case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : ¬p
⊢ x ∈ t hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), 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
s : p → Set α
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then s h else t h) ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
split_ifs with hp
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : ¬p
⊢ x ∈ t hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : p
⊢ x ∈ s hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h

case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : ¬p
⊢ x ∈ t hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
. exact ⟨fun hx => ⟨fun _ => hx, fun hnp => (hnp hp).elim⟩, fun hx => hx.1 hp⟩
no goals
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : ¬p
⊢ x ∈ t hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
. exact ⟨fun hx => ⟨fun h => (hp h).elim, fun _ => hx⟩, fun hx => hx.2 hp⟩
no goals
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : p
⊢ x ∈ s hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
exact ⟨fun hx => ⟨fun _ => hx, fun hnp => (hnp hp).elim⟩, fun hx => hx.1 hp⟩
no goals
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : ¬p
⊢ x ∈ t hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
exact ⟨fun hx => ⟨fun h => (hp h).elim, fun _ => hx⟩, fun hx => hx.2 hp⟩