-- Mathlib/Data/Finset/Prod.lean
theorem filter_product_card (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop)
    [DecidablePred p] [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => (p x.1) = (q x.2)).card =
      (s.filter p).card * (t.filter q).card +
        (s.filter (¬ p ·)).card * (t.filter (¬ q ·)).card

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t)) (filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t))

Tactic:
apply Finset.disjoint_filter_filter'

Result:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (fun x => p x.1 ∧ q x.2) fun x => ¬p x.1 ∧ ¬q x.2

Proof state:
case right
α : Type u_1
β : Type u_2
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

Tactic:
simp only [h.2, Function.comp_apply, Decidable.em, and_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #(filter (fun x => p x.1 = q x.2) (s ×ˢ t)) =
    #(filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ∪ filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t))

Tactic:
apply congr_arg

Result:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.1 = q x.2) (s ×ˢ t) =
    filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ∪ filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t)

Proof state:
case h.h.mk
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.1 = q x.2) (s ×ˢ t) ↔
    (a, b) ∈ filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ∪ filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t)

Tactic:
simp only [filter_union_right, mem_filter, mem_product]

Result:
case h.h.mk
α : Type u_1
β : Type u_2
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)

Proof state:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (fun x => p x.1 ∧ q x.2) fun x => ¬p x.1 ∧ ¬q x.2

Tactic:
exact (disjoint_compl_right.inf_left _).inf_right _

Result:
no goals

Proof state:
case h.h.mk
α : Type u_1
β : Type u_2
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)

Tactic:
constructor <;> intro h <;> use h.1

Result:
case right
α : Type u_1
β : Type u_2
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 right
α : Type u_1
β : Type u_2
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

Proof state:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.1 = q x.2) (s ×ˢ t) =
    filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ∪ filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t)

Tactic:
ext ⟨a, b⟩

Result:
case h.h.mk
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.1 = q x.2) (s ×ˢ t) ↔
    (a, b) ∈ filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ∪ filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t)

Proof state:
case right
α : Type u_1
β : Type u_2
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

Tactic:
revert h

Result:
case right
α : Type u_1
β : Type u_2
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

Proof state:
case right
α : Type u_1
β : Type u_2
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

Tactic:
simp only [Function.comp_apply, and_imp]

Result:
case right
α : Type u_1
β : Type u_2
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

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #(filter (fun x => p x.1 = q x.2) (s ×ˢ t)) =
    #(filter p s) * #(filter q t) + #(filter (fun x => ¬p x) s) * #(filter (fun x => ¬q x) t)

Tactic:
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #(filter (fun x => p x.1 = q x.2) (s ×ˢ t)) =
    #(filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ∪ filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t))

α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t)) (filter (fun x => ¬p x.1 ∧ ¬q x.2) (s ×ˢ t))

Proof state:
case right
α : Type u_1
β : Type u_2
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

Tactic:
rintro _ _ (_|_) <;> simp [*]

Result:
no goals