awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
⊢ (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2
have bit : ∀ (b : Bool) (n : ℕ), (bit b n + 1).div2 = bif (bit b n).bodd then (bit b n).div2.succ else (bit b n).div2
Tactic: cases n using bitCasesOn with
  | bit b n => cases b <;>
    simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
⊢ (bit b n).div2 = n
have rw : bit b n / 2 = n
Tactic: rw [div2_val, bit_div_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
rw : bit b n / 2 = n
⊢ (bit b n).div2 = n
have rw₁ : n = n
Tactic: rw [div2_val, bit_div_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
⊢ n.bodd.toNat + 2 * n.div2 = n
have bit : ∀ (b : Bool) (n : ℕ), (bit b n).bodd.toNat + 2 * (bit b n).div2 = bit b n
Tactic: cases n using bitCasesOn with
  | bit b n => simpa using (bit_val b n).symm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
⊢ 2 * (m * HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n + 1) * m
have rw : m * HPow.hPow (α := ℕ) 2 n.succ = HPow.hPow (α := ℕ) 2 (n + 1) * m
Tactic: rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (hypothesis)
Goal:
m n : ℕ
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)
have this : 2 * (m * HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n + 1) * m
Tactic: have : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m := by
      rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)
have rw : shiftLeft' b m (n - k) = HShiftRight.hShiftRight (β := ℕ) (bit b (shiftLeft' b m n)) 1 >>> k
Tactic: rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = HShiftRight.hShiftRight (β := ℕ) (bit b (shiftLeft' b m n)) 1 >>> k
have simp : shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k
Tactic: simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (HShiftRight.hShiftRight (β := ℕ) (bit b n) 1 >>> m).bodd = (n >>> m).bodd
have simp : (bit b n / HPow.hPow (α := ℕ) (β := ℕ) 2 1 / HPow.hPow (α := ℕ) 2 m).bodd = (n / HPow.hPow (α := ℕ) 2 m).bodd
Tactic: simp only [shiftRight_eq_div_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (hypothesis)
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n).testBit m.succ = n.testBit m
have this : (HShiftRight.hShiftRight (β := ℕ) (bit b n) 1 >>> m).bodd = (n >>> m).bodd
Tactic: have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
    simp only [shiftRight_eq_div_pow]
    simp [← div2_val, div2_bit]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (hypothesis)
Goal:
m : ℕ
b : Bool
n : ℕ
this : (HShiftRight.hShiftRight (β := ℕ) (bit b n) 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
have this₁ : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
Tactic: rw [← shiftRight_add, Nat.add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (hypothesis)
Goal:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
have this₁ : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
Tactic: simp only [bodd_eq_one_and_ne_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)
have succ : (match (motive := Bool × ℕ → Bool × ℕ) (n.bodd, n.div2) with
  | (false, m) => (true, m)
  | (true, m) => (false, m.succ)) =
  ((n + 1).bodd, (n + 1).div2)
Tactic: rw [boddDiv2, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (match (motive := Bool × ℕ → Bool × ℕ) (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
have succ : ∀ (hn : n.bodd = false),
  (match (motive := Bool × ℕ → Bool × ℕ) (false, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
Tactic: cases hn : n.bodd
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
succ :
  ∀ (hn : n.bodd = false),
    (match (motive := Bool × ℕ → Bool × ℕ) (false, n.div2) with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)) =
      ((n + 1).bodd, (n + 1).div2)
⊢ (match (motive := Bool × ℕ → Bool × ℕ) (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
have succ₁ : ∀ (hn : n.bodd = true),
  (match (motive := Bool × ℕ → Bool × ℕ) (true, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
Tactic: cases hn : n.bodd
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
⊢ n.boddDiv2 = (n.bodd, n.div2)
have zero : boddDiv2 0 = (bodd 0, div2 0)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [boddDiv2, ih]
    cases hn : n.bodd <;> simp [hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
zero : boddDiv2 0 = (bodd 0, div2 0)
⊢ n.boddDiv2 = (n.bodd, n.div2)
have succ : ∀ (n : ℕ) (ih : n.boddDiv2 = (n.bodd, n.div2)), (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [boddDiv2, ih]
    cases hn : n.bodd <;> simp [hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0
have false : bit false n ≠ 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
h : n ≠ 0
false : bit Bool.false n ≠ 0
⊢ bit b n ≠ 0
have true : bit true n ≠ 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h :
  Eq.{u} (α := (n : ℕ) → motive n)
    ((fun (H : (b : Bool) → (n : ℕ) → motive (bit b n)) (n : ℕ) ↦ bitCasesOn (motive := motive) n H) H₁)
    ((fun (H : (b : Bool) → (n : ℕ) → motive (bit b n)) (n : ℕ) ↦ bitCasesOn (motive := motive) n H) H₂)
⊢ H₁ = H₂
have h₁ : ∀ (b : Bool) (n : ℕ), H₁ b n = H₂ b n
Tactic: ext b n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
a b : Bool
h : m < n
⊢ bit a m < 2 * n
have false : bit false m < 2 * n
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
a b : Bool
h : m < n
false : bit Bool.false m < 2 * n
⊢ bit a m < 2 * n
have true : bit true m < 2 * n
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
a b : Bool
h : m < n
⊢ 2 * n ≤ bit b n
have false : 2 * n ≤ bit false n
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
a b : Bool
h : m < n
false : 2 * n ≤ bit Bool.false n
⊢ 2 * n ≤ bit b n
have true : 2 * n ≤ bit true n
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ (bit b n).bits = b :: n.bits
have h : [false] = [] ∨ (n = 0 → b = true)
Tactic: rw [Nat.bits, Nat.bits, binaryRec_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
⊢ n.bodd = n.bits.headI
have zero : bodd 0 = (bits 0).headI
Tactic: induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [bodd_bit, bits_append_bit _ _ h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
zero : bodd 0 = (bits 0).headI
⊢ n.bodd = n.bits.headI
have bit : ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true), n.bodd = n.bits.headI → (bit b n).bodd = (bit b n).bits.headI
Tactic: induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [bodd_bit, bits_append_bit _ _ h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
⊢ n.div2.bits = n.bits.tail
have zero : (div2 0).bits = (bits 0).tail
Tactic: induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [div2_bit, bits_append_bit _ _ h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
zero : (div2 0).bits = (bits 0).tail
⊢ n.div2.bits = n.bits.tail
have bit : ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true), n.div2.bits = n.bits.tail → (bit b n).div2.bits = (bit b n).bits.tail
Tactic: induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [div2_bit, bits_append_bit _ _ h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n : ℕ
⊢ bitwise f n 0 = if f true false = true then n else 0
have unfold : (if n = 0 then if f false true = true then 0 else 0
  else
    if Eq (α := ℕ) 0 0 then if f true false = true then n else 0
    else
      have n' := n / 2;
      have m' := 0 / 2;
      let b₁ := n % 2 = 1;
      let b₂ := HMod.hMod (α := ℕ) 0 2 = 1;
      have r := bitwise f n' m';
      if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
  if f true false = true then n else 0
Tactic: unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n : ℕ
⊢ (if n = 0 then if f false true = true then 0 else 0
    else
      if Eq (α := ℕ) 0 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := 0 / 2;
        let b₁ := n % 2 = 1;
        let b₂ := HMod.hMod (α := ℕ) 0 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    if f true false = true then n else 0
have simp : n = 0 → 0 = if f true false = true then n else 0
Tactic: simp only [ite_self, Nat.zero_div, ite_true, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
⊢ Eq (α := ℕ) 0 (if f true false = true then 0 else 0)
have pos : f true false = true → Eq (α := ℕ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
pos : f true false = true → Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) 0 (if f true false = true then 0 else 0)
have neg : ¬f true false = true → Eq (α := ℕ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
| bitwise f n m
have unfold : 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
    have n' := n / 2;
    have m' := m / 2;
    let b₁ := n % 2 = 1;
    let b₂ := m % 2 = 1;
    have r := bitwise f n' m';
    if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
Tactic: unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
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))
have conv_lhs : (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
      have n' := n / 2;
      have m' := m / 2;
      let b₁ := n % 2 = 1;
      let b₂ := m % 2 = 1;
      have 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: conv_lhs => unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x % 2 = 1) = x.bodd
have simp : decide (x.bodd.toNat = 1) = x.bodd
Tactic: simp only [mod_two_of_bodd]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x.bodd.toNat = 1) = x.bodd
have false : decide (false.toNat = 1) = false
Tactic: cases bodd x
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
false : decide (Bool.false.toNat = 1) = Bool.false
⊢ decide (x.bodd.toNat = 1) = x.bodd
have true : decide (true.toNat = 1) = true
Tactic: cases bodd x
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
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
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have 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))
have mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
Tactic: have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
    simp only [mod_two_of_bodd]; cases bodd x <;> rfl
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ binaryRec (motive := fun (x : ℕ) ↦ C x) z f n =
    Eq.rec (motive := fun (x : ℕ) (h : bit n.bodd n.div2 = x) ↦ C x)
      (f n.bodd n.div2 (binaryRec (motive := fun (x : ℕ) ↦ C x) z f n.div2)) ⋯
have rw : Eq.{u_1} (α := C n)
  (cast (α := C (bit (n.testBit 0) (HShiftRight.hShiftRight (β := ℕ) n 1))) sorry
      (f (1 &&& n != 0) (HShiftRight.hShiftRight (β := ℕ) n 1)
        (binaryRec (motive := fun (x : ℕ) ↦ C x) z f (HShiftRight.hShiftRight (β := ℕ) n 1))) :
    C n)
  (cast (α := C (bit n.bodd n.div2)) sorry (f n.bodd n.div2 (binaryRec (motive := fun (x : ℕ) ↦ C x) z f n.div2)) : C n)
Tactic: rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
| bitwise f (bit a m) (bit b n)
have unfold : 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
    have n' := bit a m / 2;
    have m' := bit b n / 2;
    let b₁ := bit a m % 2 = 1;
    let b₂ := bit b n % 2 = 1;
    have r := bitwise f n' m';
    if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
Tactic: unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
have conv_lhs : (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
      have n' := bit a m / 2;
      have m' := bit b n / 2;
      let b₁ := bit a m % 2 = 1;
      let b₂ := bit b n % 2 = 1;
      have 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: conv_lhs => unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ (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
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have 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)
have simp : (if (if a = true then 2 * m + 1 else 2 * m) = 0 then
    if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
  else
    if (if b = true then 2 * n + 1 else 2 * n) = 0 then
      if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0
    else
      if
          f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1))
              (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
            true then
        bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
          1
      else
        bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
  if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Tactic: simp only [bit, Bool.cond_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (x + x + 1) / 2 = x
have rw : (1 + 2 * x) / 2 = x
Tactic: rw [← two_mul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ (if (if a = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
    if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
Tactic: have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if a = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
    if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have false : (if (if false = true then 2 * m + 1 else 2 * m) = 0 then
    if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
  else
    if (if b = 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 b = 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 b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if b = 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 b = true then 2 * n + 1 else 2 * n) / 2) +
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
  if f false b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Tactic: cases a
Cleared hypotheses: a
-- 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
⊢ (if (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = 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 b = 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 b = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if b = 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 b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
    if f false b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have false : (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
Tactic: cases b
Cleared hypotheses: b