Unknown identifier, but works elsewhere

Stream: general

[Quinn Culver]

Aloha,

For some reason, I'm getting a mysterious 'unknown identifier' error.

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 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₂₁,

    let q := mk_point hl₃l₁,
    have hq: q ∈ l₃ ∧ q ∈ l₁, from mk_point_ax hl₃1₁, --ERROR here: unknown identifier 'hl₃1₁'
  end

The error message is unknown identifier 'hl₃1₁'

Mysteriously, the error-producing line, mutatis muntandis, works if I do

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 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 hl₁l₃: l₁ ≠ l₃, from distinct_lines h h₁₃,
    let q := mk_point hl₁l₃,
    have hq: q ∈ l₁ ∧ q ∈ l₃, from mk_point_ax hl₁l₃, --SAME LINE WORKS HERE
  end,

  begin
    sorry
  end,

Pardon me in advance for what is likely a silly oversight. :heart:

[Patrick Johnson]

Note the difference: hl₃1₁ and hl₃l₁