-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
true :
  (if (if Bool.true = Bool.true then 2 * m + 1 else 2 * m) = 0 then
      if f false Bool.true = Bool.true then if false = Bool.true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = Bool.true then 2 * n + 1 else 2 * n) = 0 then
        if f Bool.true false = Bool.true then if Bool.true = Bool.true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = Bool.true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              Bool.true then
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2)) =
    if f Bool.true false = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
⊢ (if (if Bool.true = Bool.true then 2 * m + 1 else 2 * m) = 0 then
      if f false Bool.true = Bool.true then if b = Bool.true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = Bool.true then 2 * n + 1 else 2 * n) = 0 then
        if f Bool.true false = Bool.true then if Bool.true = Bool.true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if b = Bool.true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              Bool.true then
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if b = Bool.true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if b = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if b = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if b = Bool.true then 2 * n + 1 else 2 * n) / 2)) =
    if f Bool.true b = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have true₁ : (if (if Bool.true = Bool.true then 2 * m + 1 else 2 * m) = 0 then
    if f false Bool.true = Bool.true then if Bool.true = Bool.true then 2 * n + 1 else 2 * n else 0
  else
    if (if Bool.true = Bool.true then 2 * n + 1 else 2 * n) = 0 then
      if f Bool.true false = Bool.true then if Bool.true = Bool.true then 2 * m + 1 else 2 * m else 0
    else
      if
          f (decide ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) % 2 = 1))
              (decide ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) % 2 = 1)) =
            Bool.true then
        bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2) +
          1
      else
        bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
            ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2) +
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
            ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2)) =
  if f Bool.true Bool.true = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Tactic: cases b
Cleared hypotheses: b