Weird Type Mismatch Error

Stream: lean4

[Abdalrhman M Mohamed]

Hi, I am new to Lean and have been going over tba-2021 course slides and exercises. Exercise 6 of the course contains the following piece of code:

abbrev Map (α β : Type) := α → Option β

namespace Map

def update [DecidableEq α] (m : Map α β) (k : α) (v : Option β) : Map α β :=
  fun k' => if k = k' then v else m k'

scoped notation:max m "[" k " ↦ " v "]" => update m k v

theorem apply_update [DecidableEq α] (m : Map α β) : m[k ↦ v] k = v := by
  simp [update]

I tried to prove apply_update theorem without using tactics:

theorem apply_update' [h : DecidableEq α] (m : Map α β) : m[k ↦ v] k = v :=
  show (if k = k then v else m k) = v from
  eq_self k ▸ ite_true v (m k)

However, I am getting this weird type mismatch error for ite_true v (m k):

type mismatch
  ite_true _ _
has type
  (if True then v else m k) = v : Prop
but is expected to have type
  (if True then v else m k) = v : Prop

I am confused, as the expected and actual type are exactly the same. Could someone expalin why I am getting this error and how to resolve it?

P.S. I am using the latest nightly version of Lean4.