Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case false.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n else 0
    else
      if n = 0 then if f true false = true then 2 * m else 0
      else if f false false = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

pp: case false.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n + 1 else 0
    else
      if f false true = true then bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1
      else bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

pp: case true.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if n = 0 then if f true false = true then 2 * m + 1 else 0
    else
      if f true false = true then bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1
      else bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

pp: case true.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
<;>

Goal state after:
case false.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n else 0
    else
      if n = 0 then if f true false = true then 2 * m else 0
      else if f false false = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

case false.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n + 1 else 0
    else
      if f false true = true then bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1
      else bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

case true.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if n = 0 then if f true false = true then 2 * m + 1 else 0
    else
      if f true false = true then bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1
      else bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

case true.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n