-- Mathlib/Data/Nat/Bitwise.lean
/-- An alternative for `bitwise_bit` which replaces the `f false false = false` assumption
with assumptions that neither `bit a m` nor `bit b n` are `0`
(albeit, phrased as the implications `m = 0 → a = true` and `n = 0 → b = true`) -/
lemma bitwise_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool) (n : Nat)
    (ham : m = 0 → a = true) (hbn : n = 0 → b = true) :
    bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Proof state:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)

Tactic:
conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]

Result:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    (if f a b = true then fun x => x + x + 1 else fun x => x + x) (bitwise f m n)

Proof state:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
conv_lhs => unfold bitwise

Result:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        let n' := bit a m / 2;
        let m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Proof state:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        let n' := bit a m / 2;
        let m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Tactic:
rw [← bit_ne_zero_iff] at ham hbn

Result:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        let n' := bit a m / 2;
        let m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Proof state:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    (if f a b = true then fun x => x + x + 1 else fun x => x + x) (bitwise f m n)

Tactic:
split_ifs with hf <;> rfl

Result:
no goals

Proof state:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        let n' := bit a m / 2;
        let m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Tactic:
simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit, ne_eq,
  ite_false]

Result:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)