Mathlib4 Calc versus Batteries Calc?

Question

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

--import Mathlib.Tactic

def pow256_shr (n : Nat) (m : UInt8) (k : Nat) (p : n < 256^k) : (m.val * 256^k + n < 256^(k+1)) := by
  have mLt : (m.val : Nat) < 256 := m.val.isLt
  calc
    _ < 256 * 256^k := by sorry
    _ = 256^(k+1) := by sorry

On Lean 4.7.0 the above succeeds (ignoring the sorry) for now. However, if I uncomment the import Mathlib.Tactic line, then it fails. Here, Mathlib is imported with this line in the lakefile.lean:

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"v4.7.0"

(I couldn't use the latest commit because that did not compile)

Thoughts?