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 (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    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 (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 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 (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    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 (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 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 (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    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 (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 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 (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    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 (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n