I’ve typed the following into Lean4 in VSCode:

I was working through converting a proof to calc style (see original here) and came across this strangeness:

I am interested in understanding how this lemma can be improved (which is part of a bigger proof, see below), as it still seems a bit “long winded” to me. Note I’m not using Mathlib and prefer to stick with Std4 (now Batteries?):