α : Type ?u.271140
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ r * (bit0 n + 1) = 2 • (r * n) + r
α : Type ?u.271140
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ r * bit1 n = 2 • (r * n) + r
dsimp [bit1]
no goals
α : Type ?u.271140
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocRing R
n r : R
⊢ r * (bit0 n + 1) = 2 • (r * n) + r
rw [mul_add, mul_bit0, mul_one]