α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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)
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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
conv_rhs => { rw [← s.diag_card] }
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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)
simp only [diag_card] at *
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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)
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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
rw [tsub_eq_of_eq_add_rev]
no goals
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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)
rw [this]
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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)
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (diag s) + card (offDiag s) = card s * card s
rw [← card_product, diag, offDiag]
no goals
α : Type u_1
β : Type ?u.112877
γ : Type ?u.112880
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)
conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]