Lean tossing an error over having exactly what it wants

Stream: lean4

[Aron]

import Mathlib.Logic.Basic
-- def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

-- syntax "∃!" term "," term: term
-- macro_rules
-- | `(∃! $t:term, $p:term) => `(exunique (fun $t => $p))

class incidence (point line: Type) (inc:point → line → Prop) :=
(one: ∀ P Q, P ≠ Q → ∃! l, inc P l ∧ inc Q l)
(two: ∀ l, ∃ P Q, P ≠ Q ∧ inc P l ∧ inc Q l)
(three: ∃ P Q R, P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ∀ l, ¬(inc P l ∧ inc Q l ∧ inc R l))

variable {point line:Type}
variable (inc:point → line → Prop)
variable [i: incidence point line inc]

-- many lines and theorems hidden for your convenience

theorem t6: ∃ l1 l2 l3, l1≠l2∧l1≠l3∧l2≠l3∧∀ p,¬(inc p l1 ∧ inc p l2 ∧ inc p l3) :=by
have ⟨a,b,c,h'a'n'b,h'a'n'c,h'b'n'c,h'n'col⟩:=i.three
have ⟨l'ab,h'lab'ppty,h'lab'uq⟩:= i.one a b h'a'n'b
have ⟨l'ac,h'lac'ppty,h'lac'uq⟩:= i.one a c h'a'n'c
have ⟨l'bc,h'lbc'ppty,h'lbc'uq⟩:= i.one b c h'b'n'c
refine ⟨l'ab,l'ac,l'bc,?_,?_,?_,?_⟩
{
intro h'lab'lac
have h'c'lab:= Eq.substr h'lab'lac h'lac'ppty

}
{sorry}
{sorry}
{sorry}

Trying.lean:253:35: error: application type mismatch
  Eq.substr h'lab'lac h'lac'ppty
argument
  h'lac'ppty
has type
  (fun l => inc a l ∧ inc c l) l'ac : Prop
but is expected to have type
  (fun l => inc a l ∧ inc c l) l'ac : Prop
././Trying.lean:256:1: warning: declaration uses 'sorry'
././Trying.lean:257:1: warning: declaration uses 'sorry'
././Trying.lean:258:1: warning: declaration uses 'sorry'

It has the type it expects. What's the problem?

[Horațiu Cheval]

It works if you pass the motive explicitly

have h'c'lab := @Eq.substr _ (fun l => inc a l ∧ inc c l) _ _ h'lab'lac h'lac'ppty

[Marc Huisinga]

Note that rw makes all the motive woes disappear, e.g. rw [←h'lab'lac] at h'lac'ppty works as well.

[Leonardo de Moura]

The following section should be useful:
https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality

Notice that the second implicit parameter to Eq.subst, which provides the context in which the substitution is to occur, has type α → Prop. Inferring this predicate therefore requires an instance of higher-order unification. In full generality, the problem of determining whether a higher-order unifier exists is undecidable, and Lean can at best provide imperfect and approximate solutions to the problem. As a result, Eq.subst doesn't always do what you want it to. The macro h ▸ e uses more effective heuristics for computing this implicit parameter, and often succeeds in situations where applying Eq.subst fails.

[Leonardo de Moura]

The macro h ▸ e is quite handy when we are in term-mode (and do not want to switch to tactic-mode and use rw).

[Aron]

I usually use rw, but I can't figure out how to assign the hypothesis a new name when I'm done with it.

[Horațiu Cheval]

You can always do have new_hypothesis := old_hypothesis if you want a new name, and maybe discard the old hypothesis afterwards (I forgot if there is a tactic that does both)

[Horațiu Cheval]

Or variations thereof like have new_hypothesis : new_statement := by rw [h] at old_hypothesis; assumption

[Alex Keizer]

Horațiu Cheval said:

You can always do have new_hypothesis := old_hypothesis if you want a new name, and maybe discard the old hypothesis afterwards (I forgot if there is a tactic that does both)

There's rename which works somewhat similarly, except you have to specify the type of the old hypothesis, rather than it's name. I think it's mostly intended to work with inaccessible/unnamed hypotheses, but also works here.

[Horațiu Cheval]

Good to know!

[Aron]

I've been trying to get rename to work, do you have a use case?

[Aron]

And how do you discard hypotheses?

[Horațiu Cheval]

In Lean 3 it used to be the clear tactic, applied to the hypothesis to discard. I'm not at my computer right now to check if it's the same in Lean 4.

[Alex Keizer]

clear also works as described in lean4!