How to prove 1+1=2 in Lean4 "inline"?

I'm learnin to use Lean, specifically I'm at the existential quantifier, and I'm doing simple theorems to figure out how it works.

I've run into an issue I can't explain, namely that this code:

def even (n : Nat) : Prop := ∃(m:Nat), m+m=n

theorem even2 : even 2 :=
  have e : 1+1=2 := Eq.refl _
  ⟨1,e⟩

produces the following error:

type mismatch
  Eq.refl (1 + 1)
has type
  1 + 1 = 1 + 1 : Prop
but is expected to have type
  1 + 1 = 2 : Prop

while this code:

def even (n : Nat) : Prop := ∃(m:Nat), m+m=n

theorem plus11 : 1+1=2 := Eq.refl _

theorem even2 : even 2 :=
  have e : 1+1=2 := plus11
  ⟨1,e⟩

compiles just fine. I think it may have something to do with the difference between have and lambda application, but I get a similar error even when trying to refactor the code to use the latter rather than the former, so I'm probably wrong and I'm out of ideas.

So, how can I prove that 1+1=2, within the proof, without constructing an external theorem?

(Note: by simp seems to work, but I'd like to be able to do this without tactics)

Solution

Looking into the elaboration of your have using:

set_option trace.Meta.isDefEq.assign true
set_option trace.Meta.isDefEq true
def even2 : sorry :=
  have e : 1 + 1 = 2 := Eq.refl _
  sorry

We get two pieces of information:

When trying to elaborate, the equality, lean tries to check whether ?m.55.1 1 1 =?= ?m.37.1, where ?m.55 should be the addition operation, and ?m.37.1 should be 2.
These two metavariables are assigned earlier during elaboration ! The elaborator does assign ?m.55 := instHAdd and ?m.37 := instOfNatNat 2.

All in all, this seems like a bug, or a misoptimisation, where the metavariables are not instantiated when checking for defeq, leading to the equality check getting stuck.