[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
⊢ ∃ f, Function.Injective f ∧ ∀ (l : L), ¬f l ∈ l
[PROOFSTEP]
classical
let t : L → Finset P := fun l => Set.toFinset {p | p ∉ l}
suffices ∀ s : Finset L, s.card ≤ (s.biUnion t).card by
  -- Hall's marriage theorem
  obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
  exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
intro s
by_cases hs₀ :
  s.card =
    0
      -- If `s = ∅`, then `s.card = 0 ≤ (s.bUnion t).card`
· simp_rw [hs₀, zero_le]
by_cases hs₁ :
  s.card =
    1
      -- If `s = {l}`, then pick a point `p ∉ l`
· obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
  obtain ⟨p, hl⟩ := exists_point l
  rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
  exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
suffices (s.biUnion t)ᶜ.card ≤ sᶜ.card by
  -- Rephrase in terms of complements (uses `h`)
  rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
  replace := h.trans this
  rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ), add_le_add_iff_right] at
    this
have hs₂ : (s.biUnion t)ᶜ.card ≤ 1 := by
  -- At most one line through two points of `s`
  refine' Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => _
  simp_rw [Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and, Set.mem_toFinset, Set.mem_setOf_eq,
    Classical.not_not] at hp₁ hp₂
  obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ := Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
  exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
by_cases hs₃ : sᶜ.card = 0
· rw [hs₃, le_zero_iff]
  rw [Finset.card_compl, tsub_eq_zero_iff_le, LE.le.le_iff_eq (Finset.card_le_univ _), eq_comm,
    Finset.card_eq_iff_eq_univ] at hs₃ ⊢
  rw [hs₃]
  rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
  exact fun p =>
    Exists.elim
      (exists_line p)
        -- If `s = univ`, then show `s.bUnion t = univ`
      fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
· exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
⊢ ∃ f, Function.Injective f ∧ ∀ (l : L), ¬f l ∈ l
[PROOFSTEP]
let t : L → Finset P := fun l => Set.toFinset {p | p ∉ l}
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
⊢ ∃ f, Function.Injective f ∧ ∀ (l : L), ¬f l ∈ l
[PROOFSTEP]
suffices ∀ s : Finset L, s.card ≤ (s.biUnion t).card by
  -- Hall's marriage theorem
  obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
  exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
this : ∀ (s : Finset L), Finset.card s ≤ Finset.card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (l : L), ¬f l ∈ l
[PROOFSTEP]
obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
this : ∀ (s : Finset L), Finset.card s ≤ Finset.card (Finset.biUnion s t)
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (x : L), f x ∈ t x
⊢ ∃ f, Function.Injective f ∧ ∀ (l : L), ¬f l ∈ l
[PROOFSTEP]
exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
⊢ ∀ (s : Finset L), Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
intro s
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
by_cases hs₀ :
  s.card =
    0
      -- If `s = ∅`, then `s.card = 0 ≤ (s.bUnion t).card`
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : Finset.card s = 0
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
simp_rw [hs₀, zero_le]
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
by_cases hs₁ :
  s.card =
    1
      -- If `s = {l}`, then pick a point `p ∉ l`
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : Finset.card s = 1
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
[GOAL]
case pos.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
l : L
hs₀ : ¬Finset.card {l} = 0
hs₁ : Finset.card {l} = 1
⊢ Finset.card {l} ≤ Finset.card (Finset.biUnion {l} t)
[PROOFSTEP]
obtain ⟨p, hl⟩ := exists_point l
[GOAL]
case pos.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
l : L
hs₀ : ¬Finset.card {l} = 0
hs₁ : Finset.card {l} = 1
p : P
hl : ¬p ∈ l
⊢ Finset.card {l} ≤ Finset.card (Finset.biUnion {l} t)
[PROOFSTEP]
rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
[GOAL]
case pos.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
l : L
hs₀ : ¬Finset.card {l} = 0
hs₁ : Finset.card {l} = 1
p : P
hl : ¬p ∈ l
⊢ Finset.card (t l) ≠ 0
[PROOFSTEP]
exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
suffices (s.biUnion t)ᶜ.card ≤ sᶜ.card by
  -- Rephrase in terms of complements (uses `h`)
  rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
  replace := h.trans this
  rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ), add_le_add_iff_right] at
    this
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
this : Finset.card (Finset.biUnion s t)ᶜ ≤ Finset.card sᶜ
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
this✝ : Fintype.card P - Finset.card (Finset.biUnion s t) ≤ Fintype.card L - Finset.card s
this : Fintype.card P ≤ Finset.card (Finset.biUnion s t) + (Fintype.card L - Finset.card s)
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
replace := h.trans this
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
this✝ : Fintype.card P - Finset.card (Finset.biUnion s t) ≤ Fintype.card L - Finset.card s
this : Fintype.card L ≤ Finset.card (Finset.biUnion s t) + (Fintype.card L - Finset.card s)
⊢ Finset.card s ≤ Finset.card (Finset.biUnion s t)
[PROOFSTEP]
rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ), add_le_add_iff_right] at this
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
⊢ Finset.card (Finset.biUnion s t)ᶜ ≤ Finset.card sᶜ
[PROOFSTEP]
have hs₂ : (s.biUnion t)ᶜ.card ≤ 1 := by
  -- At most one line through two points of `s`
  refine' Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => _
  simp_rw [Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and, Set.mem_toFinset, Set.mem_setOf_eq,
    Classical.not_not] at hp₁ hp₂
  obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ := Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
  exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
⊢ Finset.card (Finset.biUnion s t)ᶜ ≤ 1
[PROOFSTEP]
refine' Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => _
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
p₁ p₂ : P
hp₁ : p₁ ∈ (Finset.biUnion s t)ᶜ
hp₂ : p₂ ∈ (Finset.biUnion s t)ᶜ
⊢ p₁ = p₂
[PROOFSTEP]
simp_rw [Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and, Set.mem_toFinset, Set.mem_setOf_eq,
  Classical.not_not] at hp₁ hp₂
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
p₁ p₂ : P
hp₁ : ∀ (x : L), x ∈ s → p₁ ∈ x
hp₂ : ∀ (x : L), x ∈ s → p₂ ∈ x
⊢ p₁ = p₂
[PROOFSTEP]
obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ := Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩)
[GOAL]
case intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
p₁ p₂ : P
hp₁ : ∀ (x : L), x ∈ s → p₁ ∈ x
hp₂ : ∀ (x : L), x ∈ s → p₂ ∈ x
l₁ l₂ : L
hl₁ : l₁ ∈ s
hl₂ : l₂ ∈ s
hl₃ : l₁ ≠ l₂
⊢ p₁ = p₂
[PROOFSTEP]
exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
⊢ Finset.card (Finset.biUnion s t)ᶜ ≤ Finset.card sᶜ
[PROOFSTEP]
by_cases hs₃ : sᶜ.card = 0
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
hs₃ : Finset.card sᶜ = 0
⊢ Finset.card (Finset.biUnion s t)ᶜ ≤ Finset.card sᶜ
[PROOFSTEP]
rw [hs₃, le_zero_iff]
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
hs₃ : Finset.card sᶜ = 0
⊢ Finset.card (Finset.biUnion s t)ᶜ = 0
[PROOFSTEP]
rw [Finset.card_compl, tsub_eq_zero_iff_le, LE.le.le_iff_eq (Finset.card_le_univ _), eq_comm,
  Finset.card_eq_iff_eq_univ] at hs₃ ⊢
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
hs₃ : s = Finset.univ
⊢ Finset.biUnion s t = Finset.univ
[PROOFSTEP]
rw [hs₃]
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
hs₃ : s = Finset.univ
⊢ Finset.biUnion Finset.univ t = Finset.univ
[PROOFSTEP]
rw [Finset.eq_univ_iff_forall] at hs₃ ⊢
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
hs₃ : ∀ (x : L), x ∈ s
⊢ ∀ (x : P), x ∈ Finset.biUnion Finset.univ t
[PROOFSTEP]
exact fun p =>
  Exists.elim
    (exists_line p)
      -- If `s = univ`, then show `s.bUnion t = univ`
    fun l hl => Finset.mem_biUnion.mpr ⟨l, Finset.mem_univ l, Set.mem_toFinset.mpr hl⟩
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => Set.toFinset {p | ¬p ∈ l}
s : Finset L
hs₀ : ¬Finset.card s = 0
hs₁ : ¬Finset.card s = 1
hs₂ : Finset.card (Finset.biUnion s t)ᶜ ≤ 1
hs₃ : ¬Finset.card sᶜ = 0
⊢ Finset.card (Finset.biUnion s t)ᶜ ≤ Finset.card sᶜ
[PROOFSTEP]
exact hs₂.trans (Nat.one_le_iff_ne_zero.mpr hs₃)
[GOAL]
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
[PROOFSTEP]
classical
simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
apply Fintype.card_congr
calc
  (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } := (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
  _ ≃ { x : L × P // x.2 ∈ x.1 } := ((Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl)
  _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l
[GOAL]
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
[PROOFSTEP]
simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
[GOAL]
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 })
[PROOFSTEP]
apply Fintype.card_congr
[GOAL]
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 }
[PROOFSTEP]
calc
  (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } := (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
  _ ≃ { x : L × P // x.2 ∈ x.1 } := ((Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl)
  _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l
[GOAL]
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
[PROOFSTEP]
by_cases hf : Infinite { p : P // p ∈ l }
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
hf : Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
[PROOFSTEP]
exact (le_of_eq Nat.card_eq_zero_of_infinite).trans (zero_le (lineCount L p))
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
[PROOFSTEP]
haveI := fintypeOfNotInfinite hf
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
[PROOFSTEP]
cases nonempty_fintype { l : L // p ∈ l }
[GOAL]
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
[PROOFSTEP]
rw [lineCount, pointCount, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
[GOAL]
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }
[PROOFSTEP]
have : ∀ p' : { p // p ∈ l }, p ≠ p' := fun p' hp' => h ((congr_arg (· ∈ l) hp').mpr p'.2)
[GOAL]
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : ¬p ∈ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this✝ : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
this : ∀ (p' : { p // p ∈ l }), p ≠ ↑p'
⊢ Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }
[PROOFSTEP]
exact
  Fintype.card_le_of_injective (fun p' => ⟨mkLine (this p'), (mkLine_ax (this p')).1⟩) fun p₁ p₂ hp =>
    Subtype.ext
      ((eq_or_eq p₁.2 p₂.2 (mkLine_ax (this p₁)).2
            ((congr_arg _ (Subtype.ext_iff.mp hp)).mpr (mkLine_ax (this p₂)).2)).resolve_right
        fun h' => (congr_arg (¬p ∈ ·) h').mp h (mkLine_ax (this p₁)).1)
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card P ≤ Fintype.card L
[PROOFSTEP]
classical
by_contra hc₂
obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_le hc₂)
have :=
  calc
    ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
    _ ≤ ∑ l, lineCount L (f l) := (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
    _ = ∑ p in Finset.univ.image f, lineCount L p :=
      (Finset.sum_bij (fun l _ => f l) (fun l hl => Finset.mem_image_of_mem f hl) (fun l _ => rfl)
        (fun l₁ l₂ hl₁ hl₂ hl₃ => hf₁ hl₃) fun p => by
        rw [Finset.mem_image]
        exact fun ⟨a, ⟨h, h'⟩⟩ => ⟨a, ⟨h, h'.symm⟩⟩)
    _ < ∑ p, lineCount L p :=
      by
      obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
      refine'
        Finset.sum_lt_sum_of_subset (Finset.univ.image f).subset_univ (Finset.mem_univ p) _ _ fun p _ _ =>
          zero_le (lineCount L p)
      · simpa only [Finset.mem_image, exists_prop, Finset.mem_univ, true_and_iff]
      · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
        obtain ⟨l, _⟩ := @exists_line P L _ _ p
        exact
          let this := not_exists.mp hp l
          ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
exact lt_irrefl _ this
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card P ≤ Fintype.card L
[PROOFSTEP]
by_contra hc₂
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
⊢ False
[PROOFSTEP]
obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_le hc₂)
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
⊢ False
[PROOFSTEP]
have :=
  calc
    ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
    _ ≤ ∑ l, lineCount L (f l) := (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
    _ = ∑ p in Finset.univ.image f, lineCount L p :=
      (Finset.sum_bij (fun l _ => f l) (fun l hl => Finset.mem_image_of_mem f hl) (fun l _ => rfl)
        (fun l₁ l₂ hl₁ hl₂ hl₃ => hf₁ hl₃) fun p => by
        rw [Finset.mem_image]
        exact fun ⟨a, ⟨h, h'⟩⟩ => ⟨a, ⟨h, h'.symm⟩⟩)
    _ < ∑ p, lineCount L p :=
      by
      obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
      refine'
        Finset.sum_lt_sum_of_subset (Finset.univ.image f).subset_univ (Finset.mem_univ p) _ _ fun p _ _ =>
          zero_le (lineCount L p)
      · simpa only [Finset.mem_image, exists_prop, Finset.mem_univ, true_and_iff]
      · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
        obtain ⟨l, _⟩ := @exists_line P L _ _ p
        exact
          let this := not_exists.mp hp l
          ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
⊢ p ∈ Finset.image f Finset.univ → ∃ a ha, p = (fun l x => f l) a ha
[PROOFSTEP]
rw [Finset.mem_image]
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
⊢ (∃ a, a ∈ Finset.univ ∧ f a = p) → ∃ a ha, p = (fun l x => f l) a ha
[PROOFSTEP]
exact fun ⟨a, ⟨h, h'⟩⟩ => ⟨a, ⟨h, h'.symm⟩⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
⊢ ∑ p in Finset.image f Finset.univ, lineCount L p < ∑ p : P, lineCount L p
[PROOFSTEP]
obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
[GOAL]
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
hp : ¬∃ a, f a = p
⊢ ∑ p in Finset.image f Finset.univ, lineCount L p < ∑ p : P, lineCount L p
[PROOFSTEP]
refine'
  Finset.sum_lt_sum_of_subset (Finset.univ.image f).subset_univ (Finset.mem_univ p) _ _ fun p _ _ =>
    zero_le (lineCount L p)
[GOAL]
case intro.refine'_1
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
hp : ¬∃ a, f a = p
⊢ ¬p ∈ Finset.image f Finset.univ
[PROOFSTEP]
simpa only [Finset.mem_image, exists_prop, Finset.mem_univ, true_and_iff]
[GOAL]
case intro.refine'_2
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
hp : ¬∃ a, f a = p
⊢ 0 < lineCount L p
[PROOFSTEP]
rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
[GOAL]
case intro.refine'_2
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
hp : ¬∃ a, f a = p
⊢ Nonempty { l // p ∈ l }
[PROOFSTEP]
obtain ⟨l, _⟩ := @exists_line P L _ _ p
[GOAL]
case intro.refine'_2.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
p : P
hp : ¬∃ a, f a = p
l : L
h✝ : ¬p ∈ l
⊢ Nonempty { l // p ∈ l }
[PROOFSTEP]
exact
  let this := not_exists.mp hp l
  ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), ¬f l ∈ l
this : ∑ p : P, lineCount L p < ∑ p : P, lineCount L p
⊢ False
[PROOFSTEP]
exact lt_irrefl _ this
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
[PROOFSTEP]
classical
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
refine'
  ⟨f, hf3, fun l =>
    (Finset.sum_eq_sum_iff_of_le fun l _ => HasLines.pointCount_le_lineCount (hf2 l)).mp
      ((sum_lineCount_eq_sum_pointCount P L).symm.trans
        (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l)) (fun l _ => refl (lineCount L (f l)))
            (fun l₁ l₂ hl₁ hl₂ hl => hf1 hl) fun p hp => _).symm)
      l (Finset.mem_univ l)⟩
obtain ⟨l, rfl⟩ := hf3.2 p
exact ⟨l, Finset.mem_univ l, rfl⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
[PROOFSTEP]
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), ¬f l ∈ l
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
[PROOFSTEP]
have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), ¬f l ∈ l
hf3 : Function.Bijective f
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)
[PROOFSTEP]
refine'
  ⟨f, hf3, fun l =>
    (Finset.sum_eq_sum_iff_of_le fun l _ => HasLines.pointCount_le_lineCount (hf2 l)).mp
      ((sum_lineCount_eq_sum_pointCount P L).symm.trans
        (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l)) (fun l _ => refl (lineCount L (f l)))
            (fun l₁ l₂ hl₁ hl₂ hl => hf1 hl) fun p hp => _).symm)
      l (Finset.mem_univ l)⟩
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), ¬f l ∈ l
hf3 : Function.Bijective f
l : L
p : P
hp : p ∈ Finset.univ
⊢ ∃ a ha, p = (fun l x => f l) a ha
[PROOFSTEP]
obtain ⟨l, rfl⟩ := hf3.2 p
[GOAL]
case intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), ¬f l ∈ l
hf3 : Function.Bijective f
l✝ l : L
hp : f l ∈ Finset.univ
⊢ ∃ a ha, f l = (fun l x => f l) a ha
[PROOFSTEP]
exact ⟨l, Finset.mem_univ l, rfl⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
classical
obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
let s : Finset (P × L) := Set.toFinset {i | i.1 ∈ i.2}
have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 :=
  by
  rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
  simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
have step2 : ∑ i in s, lineCount L i.1 = ∑ i in s, pointCount P i.2 :=
  by
  rw [s.sum_finset_product Finset.univ fun p => Set.toFinset {l | p ∈ l}]
  rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset {p | p ∈ l}]
  refine'
    (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l)) (fun l hl => _) (fun _ _ _ _ h => hf1.1 h)
        fun p _ => _).symm
  · simp_rw [Finset.sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
    change pointCount P l • pointCount P l = lineCount L (f l) • lineCount L (f l)
    rw [hf2]
  · obtain ⟨l, hl⟩ := hf1.2 p
    exact ⟨l, Finset.mem_univ l, hl.symm⟩
  all_goals simp_rw [Finset.mem_univ, true_and_iff, Set.mem_toFinset]; exact fun p => Iff.rfl
have step3 : ∑ i in sᶜ, lineCount L i.1 = ∑ i in sᶜ, pointCount P i.2 := by
  rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
rw [← Set.toFinset_compl] at step3
exact
  ((Finset.sum_eq_sum_iff_of_le fun i hi => HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
      step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
let s : Finset (P × L) := Set.toFinset {i | i.1 ∈ i.2}
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 :=
  by
  rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
  simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
⊢ ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
[PROOFSTEP]
rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
⊢ ∑ y : L, ∑ x : P, lineCount L (x, y).fst = ∑ x : P, ∑ y : L, pointCount P (x, y).snd
[PROOFSTEP]
simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
have step2 : ∑ i in s, lineCount L i.1 = ∑ i in s, pointCount P i.2 :=
  by
  rw [s.sum_finset_product Finset.univ fun p => Set.toFinset {l | p ∈ l}]
  rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset {p | p ∈ l}]
  refine'
    (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l)) (fun l hl => _) (fun _ _ _ _ h => hf1.1 h)
        fun p _ => _).symm
  · simp_rw [Finset.sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
    change pointCount P l • pointCount P l = lineCount L (f l) • lineCount L (f l)
    rw [hf2]
  · obtain ⟨l, hl⟩ := hf1.2 p
    exact ⟨l, Finset.mem_univ l, hl.symm⟩
  all_goals simp_rw [Finset.mem_univ, true_and_iff, Set.mem_toFinset]; exact fun p => Iff.rfl
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∑ i in s, lineCount L i.fst = ∑ i in s, pointCount P i.snd
[PROOFSTEP]
rw [s.sum_finset_product Finset.univ fun p => Set.toFinset {l | p ∈ l}]
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∑ c : P, ∑ a in Set.toFinset {l | c ∈ l}, lineCount L (c, a).fst = ∑ i in s, pointCount P i.snd
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.fst ∈ Finset.univ ∧ p.snd ∈ Set.toFinset {l | p.fst ∈ l}
[PROOFSTEP]
rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset {p | p ∈ l}]
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∑ c : P, ∑ a in Set.toFinset {l | c ∈ l}, lineCount L (c, a).fst =
    ∑ c : L, ∑ a in Set.toFinset {p | p ∈ c}, pointCount P (a, c).snd
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.snd ∈ Finset.univ ∧ p.fst ∈ Set.toFinset {p_1 | p_1 ∈ p.snd}
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.fst ∈ Finset.univ ∧ p.snd ∈ Set.toFinset {l | p.fst ∈ l}
[PROOFSTEP]
refine'
  (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l)) (fun l hl => _) (fun _ _ _ _ h => hf1.1 h)
      fun p _ => _).symm
[GOAL]
case refine'_1
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : ¬p ∈ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
l : L
hl : l ∈ Finset.univ
⊢ ∑ a in Set.toFinset {p | p ∈ l}, pointCount P (a, l).snd =
    ∑ a in Set.toFinset {l_1 | (fun l x => f l) l hl ∈ l_1}, lineCount L ((fun l x => f l) l hl, a).fst
[PROOFSTEP]
simp_rw [Finset.sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
[GOAL]
case refine'_1
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : ¬p ∈ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
l : L
hl : l ∈ Finset.univ
⊢ Nat.card ↑{p | p ∈ l} • pointCount P l = Nat.card ↑{l_1 | f l ∈ l_1} • lineCount L (f l)
[PROOFSTEP]
change pointCount P l • pointCount P l = lineCount L (f l) • lineCount L (f l)
[GOAL]
case refine'_1
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : ¬p ∈ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
l : L
hl : l ∈ Finset.univ
⊢ pointCount P l • pointCount P l = lineCount L (f l) • lineCount L (f l)
[PROOFSTEP]
rw [hf2]
[GOAL]
case refine'_2
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p✝ : P
l : L
hpl : ¬p✝ ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
p : P
x✝ : p ∈ Finset.univ
⊢ ∃ a ha, p = (fun l x => f l) a ha
[PROOFSTEP]
obtain ⟨l, hl⟩ := hf1.2 p
[GOAL]
case refine'_2.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p✝ : P
l✝ : L
hpl : ¬p✝ ∈ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
p : P
x✝ : p ∈ Finset.univ
l : L
hl : f l = p
⊢ ∃ a ha, p = (fun l x => f l) a ha
[PROOFSTEP]
exact ⟨l, Finset.mem_univ l, hl.symm⟩
[GOAL]
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.snd ∈ Finset.univ ∧ p.fst ∈ Set.toFinset {p_1 | p_1 ∈ p.snd}
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.fst ∈ Finset.univ ∧ p.snd ∈ Set.toFinset {l | p.fst ∈ l}
[PROOFSTEP]
all_goals simp_rw [Finset.mem_univ, true_and_iff, Set.mem_toFinset]; exact fun p => Iff.rfl
[GOAL]
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.snd ∈ Finset.univ ∧ p.fst ∈ Set.toFinset {p_1 | p_1 ∈ p.snd}
[PROOFSTEP]
simp_rw [Finset.mem_univ, true_and_iff, Set.mem_toFinset]
[GOAL]
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ {i | i.fst ∈ i.snd} ↔ p.fst ∈ {p_1 | p_1 ∈ p.snd}
[PROOFSTEP]
exact fun p => Iff.rfl
[GOAL]
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ s ↔ p.fst ∈ Finset.univ ∧ p.snd ∈ Set.toFinset {l | p.fst ∈ l}
[PROOFSTEP]
simp_rw [Finset.mem_univ, true_and_iff, Set.mem_toFinset]
[GOAL]
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
⊢ ∀ (p : P × L), p ∈ {i | i.fst ∈ i.snd} ↔ p.snd ∈ {l | p.fst ∈ l}
[PROOFSTEP]
exact fun p => Iff.rfl
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
step2 : ∑ i in s, lineCount L i.fst = ∑ i in s, pointCount P i.snd
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
have step3 : ∑ i in sᶜ, lineCount L i.1 = ∑ i in sᶜ, pointCount P i.2 := by
  rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
step2 : ∑ i in s, lineCount L i.fst = ∑ i in s, pointCount P i.snd
⊢ ∑ i in sᶜ, lineCount L i.fst = ∑ i in sᶜ, pointCount P i.snd
[PROOFSTEP]
rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
step2 : ∑ i in s, lineCount L i.fst = ∑ i in s, pointCount P i.snd
step3 : ∑ i in sᶜ, lineCount L i.fst = ∑ i in sᶜ, pointCount P i.snd
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
rw [← Set.toFinset_compl] at step3
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
step2 : ∑ i in s, lineCount L i.fst = ∑ i in s, pointCount P i.snd
step3 :
  ∑ i in Set.toFinset {i | i.fst ∈ i.snd}ᶜ, lineCount L i.fst =
    ∑ i in Set.toFinset {i | i.fst ∈ i.snd}ᶜ, pointCount P i.snd
⊢ lineCount L p = pointCount P l
[PROOFSTEP]
exact
  ((Finset.sum_eq_sum_iff_of_le fun i hi => HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
      step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : ¬p ∈ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := Set.toFinset {i | i.fst ∈ i.snd}
step1 : ∑ i : P × L, lineCount L i.fst = ∑ i : P × L, pointCount P i.snd
step2 : ∑ i in s, lineCount L i.fst = ∑ i in s, pointCount P i.snd
step3 :
  ∑ i in Set.toFinset {i | i.fst ∈ i.snd}ᶜ, lineCount L i.fst =
    ∑ i in Set.toFinset {i | i.fst ∈ i.snd}ᶜ, pointCount P i.snd
i : P × L
hi : i ∈ Set.toFinset {i | i.fst ∈ i.snd}ᶜ
⊢ ¬i.fst ∈ i.snd
[PROOFSTEP]
exact Set.mem_toFinset.mp hi
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
classical
obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h
haveI : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩
haveI := Fintype.one_lt_card_iff_nontrivial.mp ((congr_arg _ h).mpr Fintype.one_lt_card)
have h₁ : ∀ p : P, 0 < lineCount L p := fun p =>
  Exists.elim (exists_ne p) fun q hq =>
    (congr_arg _ Nat.card_eq_fintype_card).mpr (Fintype.card_pos_iff.mpr ⟨⟨mkLine hq, (mkLine_ax hq).2⟩⟩)
have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l))
obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁))
by_cases hl₂ : p ∈ l₂
exact ⟨p, hl₁, hl₂⟩
have key' : Fintype.card { q : P // q ∈ l₂ } = Fintype.card { l : L // p ∈ l } :=
  ((HasLines.lineCount_eq_pointCount h hl₂).trans Nat.card_eq_fintype_card).symm.trans Nat.card_eq_fintype_card
have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)
let f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } := fun q => ⟨mkLine (this q), (mkLine_ax (this q)).1⟩
have hf : Function.Injective f := fun q₁ q₂ hq =>
  Subtype.ext
    ((eq_or_eq q₁.2 q₂.2 (mkLine_ax (this q₁)).2
          ((congr_arg _ (Subtype.ext_iff.mp hq)).mpr (mkLine_ax (this q₂)).2)).resolve_right
      fun h => (congr_arg (¬p ∈ ·) h).mp hl₂ (mkLine_ax (this q₁)).1)
have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2
obtain ⟨q, hq⟩ := key' ⟨l₁, hl₁⟩
exact ⟨q, (congr_arg _ (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
haveI : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this : Nontrivial L
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
haveI := Fintype.one_lt_card_iff_nontrivial.mp ((congr_arg _ h).mpr Fintype.one_lt_card)
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
have h₁ : ∀ p : P, 0 < lineCount L p := fun p =>
  Exists.elim (exists_ne p) fun q hq =>
    (congr_arg _ Nat.card_eq_fintype_card).mpr (Fintype.card_pos_iff.mpr ⟨⟨mkLine hq, (mkLine_ax hq).2⟩⟩)
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l))
[GOAL]
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁))
[GOAL]
case intro.intro.intro.mk
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
by_cases hl₂ : p ∈ l₂
[GOAL]
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∈ l₂
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
exact ⟨p, hl₁, hl₂⟩
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
have key' : Fintype.card { q : P // q ∈ l₂ } = Fintype.card { l : L // p ∈ l } :=
  ((HasLines.lineCount_eq_pointCount h hl₂).trans Nat.card_eq_fintype_card).symm.trans Nat.card_eq_fintype_card
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
let f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } := fun q => ⟨mkLine (this q), (mkLine_ax (this q)).1⟩
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } :=
  fun q => { val := mkLine (_ : p ≠ ↑q), property := (_ : p ∈ mkLine (_ : p ≠ ↑q)) }
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
have hf : Function.Injective f := fun q₁ q₂ hq =>
  Subtype.ext
    ((eq_or_eq q₁.2 q₂.2 (mkLine_ax (this q₁)).2
          ((congr_arg _ (Subtype.ext_iff.mp hq)).mpr (mkLine_ax (this q₂)).2)).resolve_right
      fun h => (congr_arg (¬p ∈ ·) h).mp hl₂ (mkLine_ax (this q₁)).1)
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } :=
  fun q => { val := mkLine (_ : p ≠ ↑q), property := (_ : p ∈ mkLine (_ : p ≠ ↑q)) }
hf : Function.Injective f
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2
[GOAL]
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
key'✝ : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } :=
  fun q => { val := mkLine (_ : p ≠ ↑q), property := (_ : p ∈ mkLine (_ : p ≠ ↑q)) }
hf : Function.Injective f
key' : Function.Surjective f
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
obtain ⟨q, hq⟩ := key' ⟨l₁, hl₁⟩
[GOAL]
case neg.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : ¬p ∈ l₂
key'✝ : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } :=
  fun q => { val := mkLine (_ : p ≠ ↑q), property := (_ : p ∈ mkLine (_ : p ≠ ↑q)) }
hf : Function.Injective f
key' : Function.Surjective f
q : { q // q ∈ l₂ }
hq : f q = { val := l₁, property := hl₁ }
⊢ ∃ p, p ∈ l₁ ∧ p ∈ l₂
[PROOFSTEP]
exact ⟨q, (congr_arg _ (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
cases nonempty_fintype P
[GOAL]
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 q : P
val✝ : Fintype P
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
cases nonempty_fintype L
[GOAL]
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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have h := card_points_eq_card_lines P L
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
let n := lineCount L p₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have hp₂ : lineCount L p₂ = n := rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have hl₁ : pointCount P l₁ = n := (HasLines.lineCount_eq_pointCount h h₂₁).symm.trans hp₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have hp₃ : lineCount L p₃ = n := (HasLines.lineCount_eq_pointCount h h₃₁).trans hl₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans hp₃
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have hp₁ : lineCount L p₁ = n := (HasLines.lineCount_eq_pointCount h h₁₃).trans hl₃
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
have hl₂ : pointCount P l₂ = n := (HasLines.lineCount_eq_pointCount h h₁₂).symm.trans hp₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
suffices ∀ p : P, lineCount L p = n by exact (this p).trans (this q).symm
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
this : ∀ (p : P), lineCount L p = n
⊢ lineCount L p = lineCount L q
[PROOFSTEP]
exact (this p).trans (this q).symm
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
⊢ ∀ (p : P), lineCount L p = n
[PROOFSTEP]
refine' fun p => or_not.elim (fun h₂ => _) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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✝ q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
⊢ lineCount L p = n
[PROOFSTEP]
refine' or_not.elim (fun h₃ => _) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans hl₃
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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✝ q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : ¬p₁ ∈ l₂
h₁₃ : ¬p₁ ∈ l₃
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
p : P
h₂ : p ∈ l₂
h₃ : p ∈ l₃
⊢ lineCount L p = n
[PROOFSTEP]
rw [(eq_or_eq h₂ h₂₂ h₃ h₂₃).resolve_right fun h => h₃₃ ((congr_arg (Membership.mem p₃) h).mp h₃₂)]
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l m : L
⊢ pointCount P l = pointCount P m
[PROOFSTEP]
apply lineCount_eq_lineCount (Dual P)
[GOAL]
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
[PROOFSTEP]
cases nonempty_fintype P
[GOAL]
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
[PROOFSTEP]
cases nonempty_fintype L
[GOAL]
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
[PROOFSTEP]
exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ lineCount L p = order P L + 1
[PROOFSTEP]
classical
obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)
cases nonempty_fintype { l : L // q ∈ l }
rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q, lineCount,
  Nat.card_eq_fintype_card, Nat.sub_add_cancel]
exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ lineCount L p = order P L + 1
[PROOFSTEP]
obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.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 q : P
l : L
h : q ∈ l
⊢ lineCount L p = order P L + 1
[PROOFSTEP]
cases nonempty_fintype { l : L // q ∈ l }
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ lineCount L p = order P L + 1
[PROOFSTEP]
rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q, lineCount,
  Nat.card_eq_fintype_card, Nat.sub_add_cancel]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.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 q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ 1 ≤ Fintype.card { l // q ∈ l }
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
⊢ 1 < order P L
[PROOFSTEP]
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
⊢ 1 < order P L
[PROOFSTEP]
cases nonempty_fintype { p : P // p ∈ l₂ }
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ 1 < order P L
[PROOFSTEP]
rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card, Fintype.two_lt_card_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
simp_rw [Ne, Subtype.ext_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, ¬↑a = ↑b ∧ ¬↑a = ↑c ∧ ¬↑b = ↑c
[PROOFSTEP]
have h := mkPoint_ax fun h => h₂₁ ((congr_arg _ h).mpr h₂₂)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : ¬p₂ ∈ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : ¬p₃ ∈ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : ¬p₃ ∈ l₃
val✝ : Fintype { p // p ∈ l₂ }
h : mkPoint (_ : l₁ = l₂ → False) ∈ l₁ ∧ mkPoint (_ : l₁ = l₂ → False) ∈ l₂
⊢ ∃ a b c, ¬↑a = ↑b ∧ ¬↑a = ↑c ∧ ¬↑b = ↑c
[PROOFSTEP]
exact
  ⟨⟨mkPoint _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩, ne_of_mem_of_not_mem h.1 h₂₁, ne_of_mem_of_not_mem h.1 h₃₁,
    ne_of_mem_of_not_mem h₂₃ h₃₃⟩
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ 2 < lineCount L p
[PROOFSTEP]
simpa only [lineCount_eq L p, Nat.succ_lt_succ_iff] using one_lt_order P L
[GOAL]
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l : L
⊢ 2 < pointCount P l
[PROOFSTEP]
simpa only [pointCount_eq P l, Nat.succ_lt_succ_iff] using one_lt_order P L
[GOAL]
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
[PROOFSTEP]
cases nonempty_fintype L
[GOAL]
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
[PROOFSTEP]
obtain ⟨p, -⟩ := @exists_config P L _ _
[GOAL]
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
[PROOFSTEP]
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 }
[GOAL]
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
[PROOFSTEP]
classical
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))
have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L :=
  by
  intro l
  rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
    Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ← Nat.card_eq_fintype_card]
  refine' tsub_eq_of_eq_add ((pointCount_eq P l.1).trans _)
  rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
  simp_rw [Subtype.ext_iff_val]
simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]
rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]
[GOAL]
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
[PROOFSTEP]
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))
[GOAL]
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
[PROOFSTEP]
apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
[GOAL]
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
[PROOFSTEP]
convert (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
[GOAL]
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
[PROOFSTEP]
have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L :=
  by
  intro l
  rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
    Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ← Nat.card_eq_fintype_card]
  refine' tsub_eq_of_eq_add ((pointCount_eq P l.1).trans _)
  rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
  simp_rw [Subtype.ext_iff_val]
[GOAL]
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
[PROOFSTEP]
intro l
[GOAL]
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
[PROOFSTEP]
rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
  Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ← Nat.card_eq_fintype_card]
[GOAL]
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
[PROOFSTEP]
refine' tsub_eq_of_eq_add ((pointCount_eq P l.1).trans _)
[GOAL]
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 }
[PROOFSTEP]
rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
[GOAL]
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 }
[PROOFSTEP]
simp_rw [Subtype.ext_iff_val]
[GOAL]
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
[PROOFSTEP]
simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]
[GOAL]
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
[PROOFSTEP]
rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]