α : Type ?u.269208
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✝ : NonUnitalNonAssocRing R
n r : R
⊢ r * (n + n) = 2 • (r * n)
α : Type ?u.269208
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✝ : NonUnitalNonAssocRing R
n r : R
⊢ r * bit0 n = 2 • (r * n)
dsimp [bit0]
no goals
α : Type ?u.269208
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✝ : NonUnitalNonAssocRing R
n r : R
⊢ r * (n + n) = 2 • (r * n)
rw [mul_add, ← one_add_one_eq_two, add_zsmul, one_zsmul]