case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
cases nonempty_fintype L
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
obtain ⟨p, -⟩ := @exists_config P L _ _
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
let ϕ : { q // q ≠ p } ≃ Σl : { l : L // p ∈ l }, { q // q ∈ l.1 ∧ q ≠ p } :=
  { toFun := fun q => ⟨⟨mkLine q.2, (mkLine_ax q.2).2⟩, q, (mkLine_ax q.2).1, q.2⟩
    invFun := fun lq => ⟨lq.2, lq.2.2.2⟩
    left_inv := fun q => Subtype.ext rfl
    right_inv := fun lq =>
      Sigma.subtype_ext
        (Subtype.ext
          ((eq_or_eq (mkLine_ax lq.2.2.2).1 (mkLine_ax lq.2.2.2).2 lq.2.2.1 lq.1.2).resolve_left
            lq.2.2.2))
        rfl }
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
have h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P := by
  apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
  convert(Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Fintype.card { l // p ∈ l } • order P L + 1 = order P L ^ 2 + order P L + 1
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]
no goals
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Fintype.card { l // p ∈ l } • order P L + 1 = order P L ^ 2 + order P L + 1
rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
⊢ Fintype.card { q // q ≠ p } = Fintype.card P - Nat.succ 0
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
⊢ Fintype.card { q // q ≠ p } + 1 = Fintype.card P
apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
no goals
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
⊢ Fintype.card { q // q ≠ p } = Fintype.card P - Nat.succ 0
convert(Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
⊢ ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
intro l
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ order P L + 1 = order P L + Fintype.card { x // ↑x = p }
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ Nat.card { x // x ∈ ↑l } - Fintype.card { x // ↑x = p } = order P L
refine' tsub_eq_of_eq_add ((pointCount_eq P l.1).trans _)
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ order P L + Fintype.card { x // x = { val := p, property := (_ : p ∈ ↑l) } } =
    order P L + Fintype.card { x // ↑x = p }
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ order P L + 1 = order P L + Fintype.card { x // ↑x = p }
rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
no goals
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  {
    toFun := fun q =>
      { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
        snd :=
          { val := ↑q,
            property :=
              (_ : ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } },
    invFun := fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) },
    left_inv :=
      (_ :
        ∀ (q : { q // q ≠ p }),
          (fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) })
              ((fun q =>
                  { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                    snd :=
                      { val := ↑q,
                        property :=
                          (_ :
                            ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧
                              ↑q ≠ p) } })
                q) =
            q),
    right_inv :=
      (_ :
        ∀ (lq : (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p }),
          (fun q =>
                { fst := { val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) },
                  snd :=
                    { val := ↑q,
                      property :=
                        (_ :
                          ↑q ∈ ↑{ val := mkLine (_ : ↑q ≠ p), property := (_ : p ∈ mkLine (_ : ↑q ≠ p)) } ∧ ↑q ≠ p) } })
              ((fun lq => { val := ↑lq.snd, property := (_ : ↑lq.snd ≠ p) }) lq) =
            lq) }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ order P L + Fintype.card { x // x = { val := p, property := (_ : p ∈ ↑l) } } =
    order P L + Fintype.card { x // ↑x = p }
simp_rw [Subtype.ext_iff_val]