m n✝ k i n : ℕ
⊢ ↑(Nat.shiftl m i) = ↑(Nat.shiftr (Nat.shiftl m (n + i)) n)
m n✝ k i n : ℕ
⊢ (fun n k i => shiftl (↑m) i = ↑(Nat.shiftr (Nat.shiftl m n) k)) (n + i) n ↑i
dsimp
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
m n✝ k i n : ℕ
⊢ ↑(Nat.shiftl m i) = ↑(Nat.shiftr (Nat.shiftl m (n + i)) n)
rw [← Nat.shiftl_sub, add_tsub_cancel_left]
no goals
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
apply Nat.le_add_right
m n✝ k i n : ℕ
⊢ shiftl ↑m -[i+1] = ↑(Nat.shiftr (Nat.shiftl m n) (n + i + 1))
m n✝ k i n : ℕ
⊢ (fun n k i => shiftl (↑m) i = ↑(Nat.shiftr (Nat.shiftl m n) k)) n (n + i + 1) -[i+1]
dsimp
no goals
m n✝ k i n : ℕ
⊢ shiftl ↑m -[i+1] = ↑(Nat.shiftr (Nat.shiftl m n) (n + i + 1))
rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl_sub, tsub_self] <;> rfl
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
m n✝ k i n : ℕ
⊢ Nat.shiftl' true m i = Nat.shiftr (Nat.shiftl' true m (n + i)) n
rw [← Nat.shiftl'_sub, add_tsub_cancel_left]
no goals
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
apply Nat.le_add_right
no goals
m n✝ k i n : ℕ
⊢ Nat.shiftr m (Nat.succ i) = Nat.shiftr (Nat.shiftl' true m n) (n + i + 1)
rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl'_sub, tsub_self] <;> rfl