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
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
by_contra hc₂
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
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
obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_le hc₂)
no goals
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
exact lt_irrefl _ this
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
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
rw [Finset.mem_image]
no goals
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
exact fun ⟨a, ⟨h, h'⟩⟩ => ⟨a, ⟨h, h'.symm⟩⟩
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
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
obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
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

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
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
refine'
  Finset.sum_lt_sum_of_subset (Finset.univ.image f).subset_univ (Finset.mem_univ p) _ _
    fun p _ _ => zero_le (lineCount L p)
no goals
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
simpa only [Finset.mem_image, exists_prop, Finset.mem_univ, true_and_iff]
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 }
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
rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
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 }
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 }
obtain ⟨l, _⟩ := @exists_line P L _ _ p
no goals
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 }
exact
  let this := not_exists.mp hp l
  ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩