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
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
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
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
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
cases nonempty_fintype { p : P // p ∈ l₂ }
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
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
rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card,
  Fintype.two_lt_card_iff]
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
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
simp_rw [Ne, Subtype.ext_iff]
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
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
have h := mkPoint_ax fun h => h₂₁ ((congr_arg _ h).mpr h₂₂)
no goals
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
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₃₃⟩