explanation of behavior of existential

Stream: new members

[Nicolas Rolland]

Why is the the second definition exhibiting a failure ?

I imagine there is a lesson to be taken about existentials from this behavior ..

universe u
variable {B : Type u }

abbrev Simple (B : Type u ) :=  Σ x : B, Bool

def id' (th : Simple B ) : Simple B := ⟨th.fst, true⟩

def isOK (th : Simple B) : True := by
      let th' := id' th
      let t' := th'.fst
      have : th.fst =  t' := rfl
      simp

def isKO (th : Simple B) : True := by
      let ⟨t', _⟩ := id' th
      have : th.fst =  t' := rfl
-- type mismatch
--   rfl
-- has type
--   th.fst = th.fst : Prop
-- but is expected to have type
--   th.fst = t' : Prop
      simp

[Daniel Weber]

The problem is that when using patterns let doesn't keep the definition

[Nicolas Rolland]

So I guess the lesson would be : best to not use pattern let, unless we don't need to reason about its provenance, aka it's for consumption only.