case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : ¬q ∈ l
val✝ : Fintype P
⊢ lineCount L q = pointCount P l
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : ¬q ∈ l
⊢ lineCount L q = pointCount P l
cases nonempty_fintype P
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : ¬q ∈ l
val✝¹ : Fintype P
val✝ : Fintype L
⊢ lineCount L q = pointCount P l
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : ¬q ∈ l
val✝ : Fintype P
⊢ lineCount L q = pointCount P l
cases nonempty_fintype L
no goals
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : ¬q ∈ l
val✝¹ : Fintype P
val✝ : Fintype L
⊢ lineCount L q = pointCount P l
exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq