no goals
α : Type ?u.308729
n : PosNum
⊢ Nat.succ ↑(pred' n) = ↑n
rw [pred'_to_nat n, Nat.succ_pred_eq_of_pos (to_nat_pos n)]
α : Type ?u.308729
n : PosNum
this : Nat.succ ↑(pred' n) = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = Nat.pred (_root_.bit0 ↑1)
α : Type ?u.308729
n : PosNum
this : Nat.succ ↑(pred' n) = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = Nat.pred (_root_.bit0 ↑n)
rw [← to_nat_inj.1 h]
no goals
α : Type ?u.308729
n : PosNum
this : Nat.succ ↑(pred' n) = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = Nat.pred (_root_.bit0 ↑1)
rfl
α : Type ?u.308729
n : PosNum
this : Nat.succ ↑(pred' n) = ↑n
p : PosNum
h : Nat.succ ↑p = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = Nat.pred (_root_.bit0 (Nat.succ ↑p))
α : Type ?u.308729
n : PosNum
this : Nat.succ ↑(pred' n) = ↑n
p : PosNum
h : Nat.succ ↑p = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = Nat.pred (_root_.bit0 ↑n)
rw [← h]
no goals
α : Type ?u.308729
n : PosNum
this : Nat.succ ↑(pred' n) = ↑n
p : PosNum
h : Nat.succ ↑p = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = Nat.pred (_root_.bit0 (Nat.succ ↑p))
exact (Nat.succ_add p p).symm