Is this a bug in the interaction between subtypes, `Prod`?

Stream: new members

[Malcolm Langfield]

Consider the following MWE:

import Mathlib

example : { F : ℕ × ℕ → StateM ℕ ℕ // ∀ a b, F (a,b) = return a }
:= by
  constructor
  introv
  rfl

which yields this error:

error: stdout:
./././Experiments/MWE.lean:7:2: error: type mismatch
  HEq.rfl
has type
  HEq ?m.163 ?m.163 : Prop
but is expected to have type
  ?val (a, b) = pure a : Prop

I'm very surprised it cannot unify this. Anyone know what's going on?

[Filippo A. E. Nuccio]

Your example aims at producing one element F such that F(a,b)=return a, so you could do

import Mathlib

example : { F : ℕ × ℕ → StateM ℕ ℕ // ∀ a b, F (a,b) = return a }
:= by
  use fun (a : ℕ × ℕ) ↦ return a.1
  rfl

[Filippo A. E. Nuccio]

If you like the constructor tactic, in this case you should use a variant:

import Mathlib

example : { F : ℕ × ℕ → StateM ℕ ℕ // ∀ a b, F (a,b) = return a }
:= by
  fconstructor
  · use fun (a : ℕ × ℕ) ↦ return a.1
  · introv
    rfl

[Filippo A. E. Nuccio]

The point is that constructor orders the goals in the opposite order of what you would expect (and fconstructor is its "forward" version, that orders them as you would expect). So, with your code, the first goal was to prove that ∀ (a b : ℕ), ?val (a, b) = pure a for a function ? that has not yet been defined, so the goal cannot be closed by rfl. With my second one, the goals are swapped, and you are first required to define the function and then to prove its properties, that now rfl can do.