α : Type u_1
inst✝ : Semiring α
n : Num
⊢ ↑n + ↑n = _root_.bit0 ↑n
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ ↑(Num.bit0 n) = _root_.bit0 ↑n
rw [← bit0_of_bit0, _root_.bit0, cast_add]
no goals
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ ↑n + ↑n = _root_.bit0 ↑n
rfl