English
The cast commutes with left shift: (m <<< n) cast equals cast(m) left-shifted by n.
Русский
Приведение коммутирует с побитовым сдвигом влево: cast(m <<< n) = cast(m) << n.
LaTeX
$$$\mathrm{castNum}(\mathrm{shiftLeft}\\, m \\text{ by } n) = (m \\alpha) \\text{shiftLeft} (n)$$$
Lean4
@[simp, norm_cast]
theorem castNum_shiftLeft (m : Num) (n : Nat) : ↑(m <<< n) = (m : ℕ) <<< (n : ℕ) :=
by
cases m <;> dsimp only [← shiftl_eq_shiftLeft, shiftl]
· symm
apply Nat.zero_shiftLeft
simp only [cast_pos]
induction n with
| zero => rfl
| succ n IH =>
simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH, mul_comm, -shiftl_eq_shiftLeft,
-PosNum.shiftl_eq_shiftLeft, mul_two]
