case succ k h_ind =>
  by_cases m = 0
  case pos hm =>
    cases hm
    unfold bitwise; simp
    cases f false true <;> simp
    . exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
    . exact hnk
  case neg hm =>
    by_cases n = 0
    case pos hn =>
      cases hn
      unfold bitwise; simp [hm]
      cases f true false <;> simp
      . exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
      . exact hmk
    case neg hn =>
      unfold bitwise; simp [hm, hn]
      rw [←Nat.mul_two, Nat.pow_succ]
      have : m/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hmk
      have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hnk
      cases f (m%2=1) (n%2=1) <;> simp
      . apply Nat.mul_lt_mul_of_pos_right ?_ (Nat.zero_lt_succ 1)
        exact h_ind ‹_› ‹_›
      . calc
        bitwise f (m/2) (n/2) * 2 + 1 
          < bitwise f (m/2) (n/2) * 2 + 2 := Nat.lt_succ_self _
        _ = (bitwise f (m/2) (n/2)) * 2 + 1*2 := rfl
        _ = (bitwise f (m/2) (n/2) + 1) * 2 := (Nat.add_mul _ _ 2).symm
        _ ≤ 2^k * 2 := Nat.mul_le_mul_right 2 (h_ind ‹m/2 < 2^k› ‹n/2 < 2^k›)
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
⊢ bitwise f m n < 2 ^ succ k
no goals