invalid kernel projection error error

Stream: lean4

[Johan Commelin]

lemma foo {X : Type} (x : X) (h : ∃ y : X, y = x) : x = x := by
  rw [← h.2]
/-
errors with

(kernel) invalid projection
  h.1
-/

That h.1 should be an h.2, I guess.

[Johan Commelin]

Is this a known issue?

[Alex J. Best]

I'm not sure if this is the same as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Kernel.20Invalid.20Projection/near/396687189, they certainly seem related, but perhaps distinct

[Marcus Rossel]

This has probably come up before, as c0b021e seems to be addressing something similar. Perhaps a similar change would need to be applied to kernel-level code.

[Mario Carneiro]

that was the kernel level code. My guess is that Johan is on an old version and this will be fixed in the next one

[Marcus Rossel]

Mario Carneiro said:

My guess is that Johan is on an old version and this will be fixed in the next one

I tried this example on the latest nightly, and that didn't fix it.

[Mario Carneiro]

Oh! It's not an off by one error, the kernel is in fact complaining about h.1 not being valid (it shows up in the type of h.2)

[Mario Carneiro]

On lean4#2747 you get a much more informative error message (notably not a (kernel) message):

invalid projection, the expression
  h
is a proposition and has type
  ∃ y, y = x
but the projected value has type
  w = x → ∃ y, y = x
 depending on the non-proposition w of type
  X

[Gareth Ma]

Mario Carneiro said:

Oh! It's not an off by one error, the kernel is in fact complaining about h.1 not being valid (it shows up in the type of h.2)

What is the correct way to resolve this? I can't match on the intro statement either. Here's my use case:

import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.BigOperators
import Mathlib.SetTheory.Cardinal.SchroederBernstein

open Nat Int Finset

noncomputable def Equiv.ofInjectiveInjective
    (f : α → β) (g : β → α) (hf : f.Injective) (hg : g.Injective) :
    α ≃ β := by
  have h := Function.Embedding.schroeder_bernstein hf hg
  exact Equiv.ofBijective h.1 h.2

I want to construct a equivalence from two injective functions, but h.1 h.2 fails.

[Mario Carneiro]

you can use h.choose and h.choose_spec to apply the axiom of choice to extract a witness

[Gareth Ma]

Aha, perfect, thanks! exact Equiv.ofBijective h.choose h.choose_spec.