α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ (∑ x in s, ∑ a in t, if r x a then 1 else 0) = ∑ x in t, ∑ a in s, if r a x then 1 else 0
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a in s, card (bipartiteAbove r t a) = ∑ b in t, card (bipartiteBelow r s b)
simp_rw [card_eq_sum_ones, bipartiteAbove, bipartiteBelow, sum_filter]
no goals
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ (∑ x in s, ∑ a in t, if r x a then 1 else 0) = ∑ x in t, ∑ a in s, if r a x then 1 else 0
exact sum_comm