α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
⊢ _root_.Disjoint (filter p s) (filter q t)
simp_rw [disjoint_left, mem_filter]
case intro.intro
α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
rintro a ⟨_, hp⟩ ⟨_, hq⟩
case intro.intro
α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), _root_.Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
case intro.intro
α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
rw [Pi.disjoint_iff] at h
no goals
case intro.intro
α : Type u_1
β : Type ?u.355965
γ : Type ?u.355968
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), _root_.Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
simpa [hp, hq] using h a