[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s
[PROOFSTEP]
simp (config := { contextual := true }) [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t
[PROOFSTEP]
simp (config := { contextual := true }) [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
⊢ image Prod.fst (s ×ˢ t) = s
[PROOFSTEP]
ext i
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
[PROOFSTEP]
simp [mem_image, ht.bex]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq β
ht : Finset.Nonempty s
⊢ image Prod.snd (s ×ˢ t) = t
[PROOFSTEP]
ext i
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq β
ht : Finset.Nonempty s
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t
[PROOFSTEP]
simp [mem_image, ht.bex]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (t ×ˢ s)) = ↑(s ×ˢ t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ (fun a => ↑{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } a) '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
[PROOFSTEP]
exact Set.image_swap_prod _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ ↑(image Prod.swap (t ×ˢ s)) = ↑(s ×ˢ t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
[PROOFSTEP]
exact Set.image_swap_prod _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ Finset.biUnion s fun a => image (fun b => (a, b)) t
[PROOFSTEP]
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm, exists_and_left,
  exists_eq_right, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm, exists_and_left,
  exists_eq_right, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun b => f (a, b)
[PROOFSTEP]
classical simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun b => f (a, b)
[PROOFSTEP]
simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) = filter p s ×ˢ filter q t
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
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 p s ×ˢ filter q t
[PROOFSTEP]
simp [mem_filter, mem_product, decide_eq_true_eq, and_comm, and_left_comm, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
p : α → Prop
inst✝ : DecidablePred p
⊢ filter (fun x => p x.fst) (s ×ˢ t) = filter p s ×ˢ t
[PROOFSTEP]
simpa using filter_product p fun _ => true
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
q : β → Prop
inst✝ : DecidablePred q
⊢ filter (fun x => q x.snd) (s ×ˢ t) = s ×ˢ filter q t
[PROOFSTEP]
simpa using filter_product (fun _ : α => true) q
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
classical
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_eq]
· apply congr_arg
  ext ⟨a, b⟩
  simp only [filter_union_right, mem_filter, mem_product]
  constructor <;> intro h <;> use h.1
  · simp only [h.2, Function.comp_apply, Decidable.em, and_self]
  · revert h
    simp only [Function.comp_apply, and_imp]
    rintro _ _ (_ | _) <;> simp [*]
· apply Finset.disjoint_filter_filter'
  exact (disjoint_compl_right.inf_left _).inf_right _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
simp only [filter_union_right, mem_filter, mem_product]
[GOAL]
case h.a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
constructor
[GOAL]
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
intro h
[GOAL]
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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) → (a ∈ s ∧ b ∈ t) ∧ p a = q b
[PROOFSTEP]
intro h
[GOAL]
case h.a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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
⊢ (a ∈ s ∧ b ∈ t) ∧ (p a ∧ q b ∨ ¬p a ∧ ¬q b)
[PROOFSTEP]
use h.1
[GOAL]
case h.a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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)
⊢ (a ∈ s ∧ b ∈ t) ∧ p a = q b
[PROOFSTEP]
use h.1
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [h.2, Function.comp_apply, Decidable.em, and_self]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
revert h
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [Function.comp_apply, and_imp]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro _ _ (_ | _)
[GOAL]
case right.inl
α : Type u_1
β : Type u_2
γ : Type u_3
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✝¹ : a ∈ s
a✝ : b ∈ t
h✝ : p a ∧ q b
⊢ p a = q b
[PROOFSTEP]
simp [*]
[GOAL]
case right.inr
α : Type u_1
β : Type u_2
γ : Type u_3
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✝¹ : a ∈ s
a✝ : b ∈ t
h✝ : ¬p a ∧ ¬q b
⊢ p a = q b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
apply Finset.disjoint_filter_filter'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact (disjoint_compl_right.inf_left _).inf_right _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, nonempty_product, not_and_or, not_nonempty_iff_eq_empty, not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a : α
⊢ {a} ×ˢ t = map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b✝ b : β
⊢ s ×ˢ {b} = map { toFun := fun i => (i, b), inj' := (_ : Function.Injective fun a => (a, b)) } s
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b✝ b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ map { toFun := fun i => (i, b), inj' := (_ : Function.Injective fun a => (a, b)) } s
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}
[PROOFSTEP]
simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t
[PROOFSTEP]
simp only [or_and_right, mem_union, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∪ t') ↔ (x, y) ∈ s ×ˢ t ∪ s ×ˢ t'
[PROOFSTEP]
simp only [and_or_left, mem_union, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∩ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t
[PROOFSTEP]
simp only [← and_and_right, mem_inter, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∩ t') ↔ (x, y) ∈ s ×ˢ t ∩ s ×ˢ t'
[PROOFSTEP]
simp only [← and_and_left, mem_inter, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t' ↔ (x, y) ∈ (s ∩ s') ×ˢ (t ∩ t')
[PROOFSTEP]
simp only [and_assoc, and_left_comm, mem_inter, mem_product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s' : Finset α
t t' : Finset β
a : α
b : β
⊢ _root_.Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ _root_.Disjoint s s' ∨ _root_.Disjoint t t'
[PROOFSTEP]
simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ x ∈ diag s ↔ x.fst ∈ s ∧ x.fst = x.snd
[PROOFSTEP]
simp (config := { contextual := true }) [diag]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ x ∈ offDiag s ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd
[PROOFSTEP]
simp [offDiag, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (diag s) = card s
[PROOFSTEP]
suffices diag s = s.image fun a => (a, a) by
  rw [this]
  apply card_image_of_injOn
  exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (diag s) = card s
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (image (fun a => (a, a)) s) = card s
[PROOFSTEP]
apply card_image_of_injOn
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ Set.InjOn (fun a => (a, a)) ↑s
[PROOFSTEP]
exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s = image (fun a => (a, a)) s
[PROOFSTEP]
ext ⟨a₁, a₂⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ diag s ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
rw [mem_diag]
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd → (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
intro h
[GOAL]
case a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ image (fun a => (a, a)) s → (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
intro h
[GOAL]
case a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ (a₁, a₂) ∈ image (fun a => (a, a)) s
[PROOFSTEP]
rw [Finset.mem_image] at *
[GOAL]
case a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂) ∈ image (fun a => (a, a)) s
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
rw [Finset.mem_image] at *
[GOAL]
case a.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
[PROOFSTEP]
use a₁
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ a₁ ∈ s ∧ (a₁, a₁) = (a₁, a₂)
[PROOFSTEP]
simpa using h
[GOAL]
case a.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
rcases h with ⟨a, h1, h2⟩
[GOAL]
case a.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
have h := Prod.mk.inj h2
[GOAL]
case a.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
[PROOFSTEP]
rw [← h.1, ← h.2]
[GOAL]
case a.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a, a).fst ∈ s ∧ (a, a).fst = (a, a).snd
[PROOFSTEP]
use h1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (diag s) + card (offDiag s) = card s * card s
[PROOFSTEP]
rw [← card_product, diag, offDiag]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (filter (fun a => a.fst = a.snd) (s ×ˢ s)) + card (filter (fun a => a.fst ≠ a.snd) (s ×ˢ s)) = card (s ×ˢ s)
[PROOFSTEP]
conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| card (s ×ˢ s)
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| card (s ×ˢ s)
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| card (s ×ˢ s)
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
⊢ card (offDiag s) = card s * card s - card s
[PROOFSTEP]
conv_rhs => {rw [← s.diag_card]}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
| card s * card s - card s
[PROOFSTEP]
{rw [← s.diag_card]}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
| card s * card s - card s
[PROOFSTEP]
{rw [← s.diag_card]}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
| card s * card s - card s
[PROOFSTEP]
rw [← s.diag_card]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card (diag s) + card (offDiag s) = card s * card s
⊢ card (offDiag s) = card (diag s) * card (diag s) - card (diag s)
[PROOFSTEP]
simp only [diag_card] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card s + card (offDiag s) = card s * card s
⊢ card (offDiag s) = card s * card s - card s
[PROOFSTEP]
rw [tsub_eq_of_eq_add_rev]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : card s + card (offDiag s) = card s * card s
⊢ card s * card s = card s + card (offDiag s)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s ∪ offDiag s = s ×ˢ s
[PROOFSTEP]
conv_rhs => rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| s ×ˢ s
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| s ×ˢ s
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
| s ×ˢ s
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ s ×ˢ s \ diag s = offDiag s
[PROOFSTEP]
rw [← diag_union_offDiag, union_comm, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _).symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ s ×ˢ s \ offDiag s = diag s
[PROOFSTEP]
rw [← diag_union_offDiag, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x✝ x : α × α
⊢ x ∈ diag (s ∩ t) ↔ x ∈ diag s ∩ diag t
[PROOFSTEP]
simpa only [mem_diag, mem_inter] using and_and_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ ↑(offDiag (s ∩ t)) = ↑(offDiag s ∩ offDiag t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ Set.offDiag (↑s ∩ ↑t) = Set.offDiag ↑s ∩ Set.offDiag ↑t
[PROOFSTEP]
exact Set.offDiag_inter _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag (s ∪ t) = diag s ∪ diag t
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
i j : α
⊢ (i, j) ∈ diag (s ∪ t) ↔ (i, j) ∈ diag s ∪ diag t
[PROOFSTEP]
simp only [mem_diag, mem_union, or_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ ↑(offDiag (s ∪ t)) = ↑(offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ Set.offDiag (↑s ∪ ↑t) = Set.offDiag ↑s ∪ Set.offDiag ↑t ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s
[PROOFSTEP]
exact Set.offDiag_union (disjoint_coe.2 h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ offDiag {a} = ∅
[PROOFSTEP]
simp [← Finset.card_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ diag {a} = {(a, a)}
[PROOFSTEP]
rw [← product_sdiff_offDiag, offDiag_singleton, sdiff_empty, singleton_product_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ diag (insert a s) = insert (a, a) (diag s)
[PROOFSTEP]
rw [insert_eq, insert_eq, diag_union, diag_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
has : ¬a ∈ s
⊢ offDiag (insert a s) = offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}
[PROOFSTEP]
rw [insert_eq, union_comm, offDiag_union (disjoint_singleton_right.2 has), offDiag_singleton, union_empty,
  union_right_comm]
