F : Type ?u.48517
ι : Type ?u.48520
α : Type u_1
β : Type ?u.48526
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n : ℚ
⊢ bit0 ↑n + 1 = bit1 ↑n
F : Type ?u.48517
ι : Type ?u.48520
α : Type u_1
β : Type ?u.48526
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n : ℚ
⊢ ↑(bit1 n) = bit1 ↑n
rw [bit1, cast_add, cast_one, cast_bit0]
no goals
F : Type ?u.48517
ι : Type ?u.48520
α : Type u_1
β : Type ?u.48526
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n : ℚ
⊢ bit0 ↑n + 1 = bit1 ↑n
rfl