English
Same as ShiftLeft_add' with additional structural details; left-shifts by sum decompose into a sequence of two left-shifts.
Русский
То же, что и ShiftLeft_add', разложение сдвига на две операции.
LaTeX
$$$$ \forall m:\mathbb{Z},\; \forall n,k:\mathbb{N},\; m <<< (n+k) = (m <<< n) <<< k. $$$$
Lean4
theorem shiftLeft_add' : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<< (n : ℤ)) <<< k
| (m : ℕ), n, (k : ℕ) => congr_arg ofNat (by simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc])
| -[_+1], _, (k : ℕ) => congr_arg negSucc (Nat.shiftLeft'_add _ _ _ _)
| (m : ℕ), n, -[k+1] =>
subNatNat_elim n k.succ (fun n k i => (↑m) <<< i = (Nat.shiftLeft' false m n) >>> k)
(fun (i n : ℕ) => by simp [← Nat.shiftLeft_sub _, Nat.add_sub_cancel_left]) fun i n =>
by
dsimp only [← Int.natCast_shiftRight]
simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add, ← Nat.shiftLeft_sub _ le_rfl,
Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast, ← shiftRight_add', Nat.cast_one]
| -[m+1], n, -[k+1] =>
subNatNat_elim n k.succ (fun n k i => -[m+1] <<< i = -[(Nat.shiftLeft' true m n) >>> k+1])
(fun i n => congr_arg negSucc <| by rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]; apply Nat.le_add_right)
fun i n =>
congr_arg negSucc <| by
rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl, Nat.sub_self, Nat.shiftLeft']
