## Stream: general

### Topic: Type mismatch at application of lemma

#### Quinn Culver (Jan 10 2023 at 22:05):

Why isn't  have hl₁l₃: l₁ ≠ l₃, from distinct_lines h h₁₃, working below?

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₂ :=  sorry

lemma axiom_3_alternative: ∃ (a₁ a₂ c₁₃ c₂₃ : P), ∀ (l : L),
¬(a₁ ∈ l ∧ a₂ ∈ l ∧ c₁₃ ∈ l)
∧ ¬(a₁ ∈ l ∧ a₂ ∈ l ∧ c₂₃ ∈ l)
∧ ¬(a₁ ∈ l ∧ c₁₃ ∈ l ∧ c₂₃ ∈ l)
∧ ¬(a₂ ∈ l ∧ c₁₃ ∈ l ∧  c₂₃ ∈ 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₃₃⟩,
cases classical.em (p₁ ∈ l₁),
begin
have hl₁l₃: l₁ ≠ l₃,  from distinct_lines h h₁₃, --Why doesn't this work?

end,

begin
sorry
end,
end


The error message is

type mismatch at application
distinct_lines h
term
h
has type
p₁ ∈ l₁ : Prop
but is expected to have type
Type ? : Type (?+1)


#### Sky Wilshaw (Jan 10 2023 at 22:17):

The first parameter of distinct_lines is P. I think you probably want to declare

variables {P L : Type u}


to make the variables implicit.

#### Quinn Culver (Jan 10 2023 at 23:57):

Thanks. I also changed lemma distinct_lines (p: P) (l₁ l₂ : L) to lemma distinct_lines {p: P}{l₁ l₂ : L} before the error went away.

Last updated: Dec 20 2023 at 11:08 UTC