case inl
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : p a
⊢ _root_.Disjoint {a} (filter p s)

case inr
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : ¬p a
⊢ _root_.Disjoint ∅ (filter p s)
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
⊢ _root_.Disjoint (if p a then {a} else ∅) (filter p s)
split_ifs
case inl
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : p a
⊢ ¬a ∈ filter p s
case inl
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : p a
⊢ _root_.Disjoint {a} (filter p s)
rw [disjoint_singleton_left]
no goals
case inl
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : p a
⊢ ¬a ∈ filter p s
exact mem_filter.not.mpr <| mt And.left ha
no goals
case inr
α : Type ?u.367165
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : ¬p a
⊢ _root_.Disjoint ∅ (filter p s)
exact disjoint_empty_left _
case inl
α : Type u_1
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h : p a
⊢ filter p (cons a s ha) = disjUnion {a} (filter p s) (_ : _root_.Disjoint {a} (filter p s))

case inr
α : Type u_1
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h : ¬p a
⊢ filter p (cons a s ha) = disjUnion ∅ (filter p s) (_ : _root_.Disjoint ∅ (filter p s))
α : Type u_1
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
⊢ filter p (cons a s ha) =
    disjUnion (if p a then {a} else ∅) (filter p s) (_ : _root_.Disjoint (if p a then {a} else ∅) (filter p s))
split_ifs with h
no goals
case inl
α : Type u_1
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h : p a
⊢ filter p (cons a s ha) = disjUnion {a} (filter p s) (_ : _root_.Disjoint {a} (filter p s))
rw [filter_cons_of_pos _ _ _ ha h, singleton_disjUnion]
no goals
case inr
α : Type u_1
β : Type ?u.367168
γ : Type ?u.367171
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h : ¬p a
⊢ filter p (cons a s ha) = disjUnion ∅ (filter p s) (_ : _root_.Disjoint ∅ (filter p s))
rw [filter_cons_of_neg _ _ _ ha h, empty_disjUnion]