P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card ((a : P) × { l // a ∈ l }) = Fintype.card ((a : L) × { p // p ∈ a })
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ ∑ p : P, lineCount L p = ∑ l : L, pointCount P l
simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
case f
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ (a : P) × { l // a ∈ l } ≃ (a : L) × { p // p ∈ a }
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card ((a : P) × { l // a ∈ l }) = Fintype.card ((a : L) × { p // p ∈ a })
apply Fintype.card_congr