mathlib

8582b06b - feat(logic/basic): mark cast_eq as a `simp` lemma (#3547)

feat(logic/basic): mark cast_eq as a `simp` lemma (#3547) The theorem `cast_eq` is in core and says `theorem cast_eq : ∀ {α : Sort u} (h : α = α) (a : α), cast h a = a` Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>