-- Mathlib/Data/Nat/Bitwise.lean
lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
    bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2))

Proof state:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
⊢ (if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        let n' := n / 2;
        let m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))

Tactic:
simp only [hn, hm, mod_two_iff_bod, ite_false, bit, two_mul, Bool.cond_eq_ite]

Result:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
⊢ (if f n.bodd m.bodd = true then bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
    else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)) =
    (if f n.bodd m.bodd = true then fun x => x + x + 1 else fun x => x + x) (bitwise f (n / 2) (m / 2))

Proof state:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x % 2 = 1) = x.bodd

Tactic:
simp only [mod_two_of_bodd, cond]

Result:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x.bodd.toNat = 1) = x.bodd

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

Tactic:
have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
  simp only [mod_two_of_bodd, cond]; cases bodd x <;> rfl

Result:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
⊢ (if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        let n' := n / 2;
        let m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))

Proof state:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
⊢ bitwise f n m = bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))

Tactic:
conv_lhs => unfold bitwise

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

Proof state:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
⊢ (if f n.bodd m.bodd = true then bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
    else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)) =
    (if f n.bodd m.bodd = true then fun x => x + x + 1 else fun x => x + x) (bitwise f (n / 2) (m / 2))

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x.bodd.toNat = 1) = x.bodd

Tactic:
cases bodd x <;> rfl

Result:
no goals