no goals
α : Type ?u.180035
⊢ ofNat' (0 + 1) = ofNat' 0 + 1
simp
case false
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1

case true
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1
α : Type ?u.180035
b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1
cases b
case false
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ cond true Num.bit1 Num.bit0 (ofNat' n) = cond false Num.bit1 Num.bit0 (ofNat' n) + 1
case false
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1
erw [ofNat'_bit true n, ofNat'_bit]
no goals
case false
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ cond true Num.bit1 Num.bit0 (ofNat' n) = cond false Num.bit1 Num.bit0 (ofNat' n) + 1
simp only [← bit1_of_bit1, ← bit0_of_bit0, cond, _root_.bit1]
case true
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ cond false Num.bit1 Num.bit0 (ofNat' n + 1) = cond true Num.bit1 Num.bit0 (ofNat' n) + 1
case true
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1
erw [show n.bit true + 1 = (n + 1).bit false by
  simp [Nat.bit, _root_.bit1, _root_.bit0]; exact Nat.add_left_comm n 1 1,
  ofNat'_bit, ofNat'_bit, ih]
no goals
case true
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ cond false Num.bit1 Num.bit0 (ofNat' n + 1) = cond true Num.bit1 Num.bit0 (ofNat' n) + 1
simp only [cond, add_one, bit1_succ]
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ n + (1 + 1) = 1 + (n + 1)
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ Nat.bit true n + 1 = Nat.bit false (n + 1)
simp [Nat.bit, _root_.bit1, _root_.bit0]
no goals
α : Type ?u.180035
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ n + (1 + 1) = 1 + (n + 1)
exact Nat.add_left_comm n 1 1