α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card (filter (fun x => p x.fst = q x.snd) (s ×ˢ t)) =
    card (filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t))

α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t)) (filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t))
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card (filter (fun x => p x.fst = q x.snd) (s ×ˢ t)) =
    card (filter p s) * card (filter q t) + card (filter (fun x => ¬p x) s) * card (filter (fun x => ¬q x) t)
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_eq]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.fst = q x.snd) (s ×ˢ t) =
    filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t)
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card (filter (fun x => p x.fst = q x.snd) (s ×ˢ t)) =
    card (filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t))
apply congr_arg
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.fst = q x.snd) (s ×ˢ t) ↔
    (a, b) ∈ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t)
case h
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.fst = q x.snd) (s ×ˢ t) =
    filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t)
ext ⟨a, b⟩
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ p a = q b ↔ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.fst = q x.snd) (s ×ˢ t) ↔
    (a, b) ∈ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ∪ filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t)
simp only [filter_union_right, mem_filter, mem_product]
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ p a = q b
⊢ p a ∧ q b ∨ ¬p a ∧ ¬q b

case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ p a = q b
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ p a = q b ↔ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
constructor <;> intro h <;> use h.1
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ p a = q b
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ p a = q b
⊢ p a ∧ q b ∨ ¬p a ∧ ¬q b

case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ p a = q b
. simp only [h.2, Function.comp_apply, Decidable.em, and_self]
no goals
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ p a = q b
. revert h
  simp only [Function.comp_apply, and_imp]
  rintro _ _ (_|_) <;> simp [*]
no goals
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ p a = q b
⊢ p a ∧ q b ∨ ¬p a ∧ ¬q b
simp only [h.2, Function.comp_apply, Decidable.em, and_self]
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b) → p a = q b
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
h : (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
⊢ p a = q b
revert h
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ a ∈ s → b ∈ t → p a ∧ q b ∨ ¬p a ∧ ¬q b → p a = q b
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b) → p a = q b
simp only [Function.comp_apply, and_imp]
no goals
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a✝ : α
b✝ : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ a ∈ s → b ∈ t → p a ∧ q b ∨ ¬p a ∧ ¬q b → p a = q b
rintro _ _ (_|_) <;> simp [*]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (fun x => p x.fst ∧ q x.snd) fun x => ¬p x.fst ∧ ¬q x.snd
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t)) (filter (fun x => ¬p x.fst ∧ ¬q x.snd) (s ×ˢ t))
apply Finset.disjoint_filter_filter'
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.63122
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (fun x => p x.fst ∧ q x.snd) fun x => ¬p x.fst ∧ ¬q x.snd
exact (disjoint_compl_right.inf_left _).inf_right _