awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i = 0
⊢ bit b n < bit b' m
have neg : ∀ (i' : ℕ) (hn : (bit b n).testBit i'.succ = false) (hm : (bit b' m).testBit i'.succ = true)
  (hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j) (hi : ¬i'.succ = 0), bit b n < bit b' m
Tactic: obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
Cleared hypotheses: i, hn, hm, hnm, hi
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hn : (bit b n).testBit i'.succ = false
hm : (bit b' m).testBit i'.succ = true
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
⊢ bit b n < bit b' m
have hn₁ : n.testBit i' = false
Tactic: simp only [testBit_bit_succ] at hn hm
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hn : (bit b n).testBit i'.succ = false
hm : (bit b' m).testBit i'.succ = true
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn₁ : n.testBit i' = false
⊢ bit b n < bit b' m
have hm₁ : m.testBit i' = true
Tactic: simp only [testBit_bit_succ] at hn hm
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = m.testBit j
have h : n.testBit j = (bit b n).testBit j.succ
Tactic: convert! hnm j.succ (succ_lt_succ hj) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
h : n.testBit j = (bit b n).testBit j.succ
⊢ n.testBit j = m.testBit j
have h₁ : m.testBit j = (bit b' m).testBit j.succ
Tactic: convert! hnm j.succ (succ_lt_succ hj) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = (bit b n).testBit j.succ
have h : n.testBit j = n.testBit j
Tactic: rw [testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ m.testBit j = (bit b' m).testBit j.succ
have h : m.testBit j = m.testBit j
Tactic: rw [testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
⊢ bit b n < bit b' m
have this : n < m
Tactic: have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
m i : ℕ
hn : (bit b n).testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j
⊢ bit b n < m
have bit : ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : testBit 0 i = true)
  (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = testBit 0 j), bit b n < 0
Tactic: induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this
Cleared hypotheses: m, i, hn, hm, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
m i : ℕ
hn : (Nat.bit b n).testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = m.testBit j
bit :
  ∀ (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : testBit 0 i = true)
    (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = testBit 0 j), Nat.bit b n < 0
⊢ Nat.bit b n < m
have bit₁ : ∀ (b' : Bool) (m : ℕ)
  (hm' :
    ∀ (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : m.testBit i = true)
      (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = m.testBit j), Nat.bit b n < m)
  (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : (Nat.bit b' m).testBit i = true)
  (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = (Nat.bit b' m).testBit j), Nat.bit b n < Nat.bit b' m
Tactic: induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this
Cleared hypotheses: m, i, hn, hm, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m i : ℕ
hn : n.testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j
⊢ n < m
have zero : ∀ {m : ℕ} (i : ℕ) (hn : testBit 0 i = false) (hm : m.testBit i = true)
  (hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j), 0 < m
Tactic: induction n using Nat.binaryRec generalizing i m with
  | zero =>
    rw [Nat.pos_iff_ne_zero]
    rintro rfl
    simp at hm
  | bit b n hn' =>
    induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this
Cleared hypotheses: n, m, i, hn, hm, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m i : ℕ
hn : n.testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j
zero :
  ∀ {m : ℕ} (i : ℕ) (hn : testBit 0 i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j), 0 < m
⊢ n < m
have bit : ∀ (b : Bool) (n : ℕ)
  (hn' :
    ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
      (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m)
  {m : ℕ} (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
  (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
Tactic: induction n using Nat.binaryRec generalizing i m with
  | zero =>
    rw [Nat.pos_iff_ne_zero]
    rintro rfl
    simp at hm
  | bit b n hn' =>
    induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this
Cleared hypotheses: n, m, i, hn, hm, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)
have h : ∀ (m n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f) m n
Tactic: funext m n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
h : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)
have h : bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
  bitwise f (bit bn n) (bit bm m)
Tactic: rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
h_1 : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
h :
  bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
    bitwise f (bit bn n) (bit bm m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)
have h₁ : bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
  bit (f bn bm) (bitwise f n m)
Tactic: rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
h_1 : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
h :
  bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
    bitwise f (bit bn n) (bit bm m)
h₁ :
  bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
    bit (f bn bm) (bitwise f n m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)
have h₂ : bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise f n m) = bit (f bn bm) (bitwise f n m)
Tactic: rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
n : ℕ
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
have h : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) 0 = bitwise f 0 (bit bm m)
Tactic: induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
n : ℕ
h : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) 0 = bitwise f 0 (bit bm m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
have h₁ : ∀ (bn : Bool) (n : ℕ) (hn : n = 0 → bn = true),
  bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m) →
    bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)
Tactic: induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
have h : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) 0 n = bitwise f n 0
Tactic: induction m using Nat.binaryRec' generalizing n with
  | zero => simp
  | bit bm m hm ihm =>
    induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
Cleared hypotheses: m, n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
m n : ℕ
h : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) 0 n = bitwise f n 0
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
have h₁ : ∀ (bm : Bool) (m : ℕ) (hm : m = 0 → bm = true)
  (ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m) (n : ℕ),
  bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
Tactic: induction m using Nat.binaryRec' generalizing n with
  | zero => simp
  | bit bm m hm ihm =>
    induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
Cleared hypotheses: m, n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)
| bitwise f n m
have rw : swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f) n m
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)
⊢ bitwise f n m = bitwise f m n
have conv_lhs : bitwise f n m = bitwise f m n
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)
conv_lhs : bitwise f n m = bitwise f m n
⊢ bitwise f n m = bitwise f m n
have conv_lhs₁ : swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f) n m = bitwise f m n
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
⊢ n &&& HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
have refine : ∀ (j : ℕ), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
Tactic: refine eq_of_testBit_eq fun j => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i j : ℕ
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
have inl : (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit i
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i j : ℕ
inl : (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit i
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
have inr : ∀ (hij : i ≠ j), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit i
have inl : ∀ (h : n.testBit i = false), (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit i
Tactic: cases h : n.testBit i
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
inl :
  ∀ (h : n.testBit i = false),
    (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit i
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit i
have inl₁ : ∀ (h : n.testBit i = true), (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (true.toNat * HPow.hPow (α := ℕ) 2 i).testBit i
Tactic: cases h : n.testBit i
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i j : ℕ
hij : i ≠ j
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
have inr : ∀ (h : n.testBit i = false), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit j
Tactic: cases h : n.testBit i
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i j : ℕ
hij : i ≠ j
inr :
  ∀ (h : n.testBit i = false),
    (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit j
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
have inr₁ : ∀ (h : n.testBit i = true), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (true.toNat * HPow.hPow (α := ℕ) 2 i).testBit j
Tactic: cases h : n.testBit i
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
⊢ HPow.hPow (α := ℕ) 2 i &&& n = HPow.hPow (α := ℕ) 2 i * (n.testBit i).toNat
have rw : HPow.hPow (α := ℕ) 2 i &&& n = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
Tactic: rw [mul_comm, land_comm, and_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
rw : HPow.hPow (α := ℕ) 2 i &&& n = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
⊢ HPow.hPow (α := ℕ) 2 i &&& n = HPow.hPow (α := ℕ) 2 i * (n.testBit i).toNat
have rw₁ : n &&& HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
Tactic: rw [mul_comm, land_comm, and_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
rw : HPow.hPow (α := ℕ) 2 i &&& n = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
rw₁ : n &&& HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
⊢ HPow.hPow (α := ℕ) 2 i &&& n = HPow.hPow (α := ℕ) 2 i * (n.testBit i).toNat
have rw₂ : (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
Tactic: rw [mul_comm, land_comm, and_two_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m k : ℕ
⊢ n &&& m &&& k = n &&& (m &&& k)
have zero : ∀ (m k : ℕ), 0 &&& m &&& k = 0 &&& (m &&& k)
Tactic: bitwise_assoc_tac
Cleared hypotheses: n, m, k
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m k : ℕ
zero : ∀ (m k : ℕ), 0 &&& m &&& k = 0 &&& (m &&& k)
⊢ n &&& m &&& k = n &&& (m &&& k)
have bit : ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n &&& m &&& k = n &&& (m &&& k)) (m k : ℕ),
  bit b n &&& m &&& k = bit b n &&& (m &&& k)
Tactic: bitwise_assoc_tac
Cleared hypotheses: n, m, k
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m k : ℕ
zero : ∀ (m k : ℕ), 0 &&& m &&& k = 0 &&& (m &&& k)
bit bit₁ bit₂ :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n &&& m &&& k = n &&& (m &&& k)) (m k : ℕ),
    Nat.bit b n &&& m &&& k = Nat.bit b n &&& (m &&& k)
⊢ n &&& m &&& k = n &&& (m &&& k)
have bit₃ : ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n &&& m &&& k = n &&& (m &&& k)) (k : ℕ) (b' : Bool) (m : ℕ)
  (hm : Nat.bit b n &&& m &&& k = Nat.bit b n &&& (m &&& k)),
  Nat.bit b n &&& Nat.bit b' m &&& k = Nat.bit b n &&& (Nat.bit b' m &&& k)
Tactic: bitwise_assoc_tac
Cleared hypotheses: n, m, k
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m k : ℕ
⊢ n ||| m ||| k = n ||| (m ||| k)
have zero : ∀ (m k : ℕ), 0 ||| m ||| k = 0 ||| (m ||| k)
Tactic: bitwise_assoc_tac
Cleared hypotheses: n, m, k
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m k : ℕ
zero : ∀ (m k : ℕ), 0 ||| m ||| k = 0 ||| (m ||| k)
⊢ n ||| m ||| k = n ||| (m ||| k)
have bit : ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n ||| m ||| k = n ||| (m ||| k)) (m k : ℕ),
  bit b n ||| m ||| k = bit b n ||| (m ||| k)
Tactic: bitwise_assoc_tac
Cleared hypotheses: n, m, k
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n m k : ℕ
zero : ∀ (m k : ℕ), 0 ||| m ||| k = 0 ||| (m ||| k)
bit bit₁ bit₂ :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n ||| m ||| k = n ||| (m ||| k)) (m k : ℕ),
    Nat.bit b n ||| m ||| k = Nat.bit b n ||| (m ||| k)
⊢ n ||| m ||| k = n ||| (m ||| k)
have bit₃ : ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n ||| m ||| k = n ||| (m ||| k)) (k : ℕ) (b' : Bool) (m : ℕ)
  (hm : Nat.bit b n ||| m ||| k = Nat.bit b n ||| (m ||| k)),
  Nat.bit b n ||| Nat.bit b' m ||| k = Nat.bit b n ||| (Nat.bit b' m ||| k)
Tactic: bitwise_assoc_tac
Cleared hypotheses: n, m, k