n : ℕ
⊢ ↑(bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
n : ℕ
⊢ (bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
no goals
n : ℕ
⊢ ↑(bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
exact congr_arg ofNat n.bodd_add_div2
no goals
n : ℕ
⊢ (bif bodd ↑n then 1 else 0) = ↑(bif bodd ↑n then 1 else 0)
cases bodd n <;> rfl
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[n+1]
refine' Eq.trans _ (congr_arg negSucc n.bodd_add_div2)
n : ℕ
⊢ (bif !Nat.bodd n then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
dsimp [bodd]
case false
n : ℕ
⊢ 1 + 2 * -[Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]

case true
n : ℕ
⊢ 0 + 2 * -[Nat.div2 n+1] = -[1 + 2 * Nat.div2 n+1]
n : ℕ
⊢ (bif !Nat.bodd n then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]
case false
n : ℕ
⊢ -[2 * Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
case false
n : ℕ
⊢ 1 + 2 * -[Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
change -[2 * Nat.div2 n+1] = _
no goals
case false
n : ℕ
⊢ -[2 * Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
rw [zero_add]
case true
n : ℕ
⊢ 2 * -[Nat.div2 n+1] = -[2 * Nat.div2 n + 1+1]
case true
n : ℕ
⊢ 0 + 2 * -[Nat.div2 n+1] = -[1 + 2 * Nat.div2 n+1]
rw [zero_add, add_comm]
no goals
case true
n : ℕ
⊢ 2 * -[Nat.div2 n+1] = -[2 * Nat.div2 n + 1+1]
rfl