norm_cast was upstreamed to Lean4

In 2019, I was an intern at Matryoshka in Amsterdam. There, I worked with Robert Y. Lewis on a tactic for the Lean prover called norm_cast. The goal was to reduce the frustration of mathematicians when working with expressions containing casts and coercions. This work was merged into Mathlib and even led to the writing of a paper.

Well, after a brief transit in Lean’s standard library, the tactic was merged yesterday into the core language!