Use `configuration.has_lines.exists_unique_line`

Stream: general

[Quinn Culver]

How do I use configuration.has_lines.exists_unique_line to complete have hll₂ : l = l₂, from... below ? I tried a few things, most of them similar to have g: ∃! m : L, p₂ ∈ m ∧ p₃ ∈ m, apply configuration.has_lines.exists_unique_line p₂ p₃ hp₂p₃, which gives the error

type mismatch at application
  configuration.has_lines.exists_unique_line p₂
term
  p₂
has type
  P : Type u
but is expected to have type
  Type ? : Type (?+1)

And do I need the two lemmas distinct_lines and distinct_points? My gut says I'm likely reinventing the wheel.

Any other comments, criticisms, etc. about my proof so far would be most appreciated. Having fun learning Lean! :smile:

Here's teh code:

import combinatorics.configuration
open configuration.projective_plane
open classical

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]

lemma distinct_lines {p : P} {l₁ l₂ : L}
(h₁: p ∈ l₁) (h₂: p ∉ l₂)  : l₁ ≠ l₂ :=
begin
  by_contradiction,
  subst_vars,
  contradiction,
end

lemma distinct_points {l : L} {p₁ p₂ : P}
(h₁: p₁ ∈ l) (h₂: p₂ ∉ l)  : p₁ ≠ p₂ :=
begin
  by_contradiction,
  subst_vars,
  contradiction,
end

lemma axiom_3_alternative: ∃ (p₁ p₂ p₃ p₄ : P), ∀ (l : L),
  ¬(p₁ ∈ l ∧ p₂ ∈ l ∧ p₃ ∈ l)
  ∧ ¬(p₁ ∈ l ∧ p₂ ∈ l ∧ p₄ ∈ l)
  ∧ ¬(p₁ ∈ l ∧ p₃ ∈ l ∧ p₄ ∈ l)
  ∧ ¬(p₂ ∈ l ∧ p₃ ∈ l ∧  p₄ ∈ l)
  :=
  begin
    have h: ∃(p₁ p₂ p₃ : P) (l₁ l₂ l₃ : L),
      p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂
        ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃,
      from exists_config,

    rcases h with ⟨p₁, p₂, p₃, l₁, l₂, l₃, hr⟩,
    rcases hr with ⟨h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩,

    have hl₃l₁: l₃ ≠ l₁,
      from  distinct_lines h₂₃ h₂₁,

    have hp₂p₃: p₂ ≠ p₃,
      from  (distinct_points h₂₃ h₃₃),

    let q := mk_point hl₃l₁,
    use [p₁, p₂, p₃, q],
    assume l:L,
    have hq: q ∈ l₃ ∧ q ∈ l₁, from mk_point_ax hl₃l₁,
    have h₁₂₃ : ¬(p₁ ∈ l ∧ p₂ ∈ l ∧ p₃ ∈ l), from
    begin
      by_contradiction,
      cases h with h₁l h_right,
      cases h_right with h₂l h₃l,
      have hll₂ : l = l₂, from
        begin
          have g: ∃! m : L, p₂ ∈ m ∧ p₃ ∈ m, apply configuration.has_lines.exists_unique_line p₂ p₃ hp₂p₃
        end
    end,

    have h₁₂q : ¬(p₁ ∈ l ∧ p₂ ∈ l ∧ q ∈ l), from
    begin
      sorry
    end,

    have h₁₃q : ¬(p₁ ∈ l ∧ p₃ ∈ l ∧ q ∈ l), from
    begin
      sorry
    end,

    have h₂₃q : ¬(p₂ ∈ l ∧ p₃ ∈ l ∧ q ∈ l), from
    begin
      sorry
    end,
    have h₁₂₃q :  ¬(p₁ ∈ l ∧ p₂ ∈ l ∧ p₃ ∈ l) ∧  ¬(p₁ ∈ l ∧ p₂ ∈ l ∧ q∈ l)
      ∧ ¬(p₁ ∈ l ∧ p₃ ∈ l ∧ q ∈ l) ∧ ¬(p₂ ∈ l ∧ p₃ ∈ l ∧ q ∈ l),
      from  ⟨h₁₂₃, ⟨h₁₂q, ⟨h₁₃q, h₂₃q⟩⟩⟩,
    exact h₁₂₃q,
end

[Junyan Xu]

You are just missing some explicit arguments:

apply configuration.has_lines.exists_unique_line P L p₂ p₃ hp₂p₃

Some comments:
distinct_lines is a special case of docs#ne_of_mem_of_not_mem', and
distinct_points is a special case of docs#ne_of_mem_of_not_mem.
⟨h₁₂₃, ⟨h₁₂q, ⟨h₁₃q, h₂₃q⟩⟩⟩, can be written ⟨h₁₂₃, h₁₂q, h₁₃q, h₂₃q⟩,