no goals
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ bit1 a = 1 ↔ a = 0
rw [show (1 : R) = bit1 0 by simp, bit1_eq_bit1]
no goals
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ 1 = bit1 0
simp