application type mismatch

Stream: new members

[Henrik Rueping]

I am having trouble to understand what exactly the cause of this message is. Here is a minimal working example:

import Mathlib


lemma myLemma(mon: { x // x ∈ Finset.range 2 } →₀ ℕ):
1=2:= by
    by_cases case1 : Even (mon ⟨1,by simp⟩)
    sorry
    have first:¬∀ (a : ℕ) (b : a < 2), Even (mon { val := a, property := (_ : a ∈ Finset.range 2) }):= by
      simp
      exact ⟨1,⟨(by simp),case1⟩⟩
    sorry

I got:

application type mismatch
  Exists.intro ?m.7349306 case1
argument
  case1
has type
  ¬Even (mon { val := 1, property := (_ : 1 ∈ Finset.range 2) }) : Prop
but is expected to have type
  ¬Even (mon { val := 1, property := (_ : 1 ∈ Finset.range 2) }) : Prop

but is seems as if the present and the expected types are exactly the same.

[Henrik Rueping]

ah that seems related:
https://leanprover-community.github.io/archive/stream/270676-lean4/topic/type.20mismatch.20with.20identical.20types.20on.20named.20pattern.20match.html

[Richard Copley]

#mwe

[Kevin Buzzard]

"printed exactly the same" doesn't mean "exactly the same" -- if you set_option pp.all true then probably they won't be exactly the same any more (because then Lean prints out all the secret stuff too). If you're in a position where you have h which looks the same as the goal but exact h doesn't work and you get an error like the above, then convert h will tell you exactly which parts don't match up. Also, what Richard said.