awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
b : Bool
n : ℕ
hs : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n
hrw :
  Eq (α := ℕ → ℕ) ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) fun (i : ℕ) ↦
    2 * HPow.hPow (α := ℕ) 2 i
bit : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (Nat.bit false n).bitIndices) = Nat.bit false n
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (Nat.bit b n).bitIndices) = Nat.bit b n
have bit₁ : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (Nat.bit true n).bitIndices) = Nat.bit true n
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n
have zero : Eq (α := ℕ) (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bitIndices 0))) 0
Tactic: induction n using binaryRec with
  | zero => simp
  | bit b n hs =>
    have hrw : (fun i ↦ 2 ^ i) ∘ (fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i := by
      ext i; simp [pow_add, mul_comm]
    cases b
    · simpa [hrw, List.sum_map_mul_left]
    simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
zero : Eq (α := ℕ) (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bitIndices 0))) 0
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n
have bit : ∀ (b : Bool) (n : ℕ) (hs : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n),
  sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bit b n).bitIndices) = bit b n
Tactic: induction n using binaryRec with
  | zero => simp
  | bit b n hs =>
    have hrw : (fun i ↦ 2 ^ i) ∘ (fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i := by
      ext i; simp [pow_add, mul_comm]
    cases b
    · simpa [hrw, List.sum_map_mul_left]
    simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
b : Bool
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit b n).bitIndices ↔ (bit b n).testBit i = true
have bit : i ∈ (bit false n).bitIndices ↔ (bit false n).testBit i = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
b : Bool
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
bit : i ∈ (Nat.bit false n).bitIndices ↔ (Nat.bit false n).testBit i = true
⊢ i ∈ (Nat.bit b n).bitIndices ↔ (Nat.bit b n).testBit i = true
have bit₁ : i ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit i = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit false n).bitIndices ↔ (bit false n).testBit i = true
have bit : 0 ∈ (bit false n).bitIndices ↔ (bit false n).testBit 0 = true
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
bit : 0 ∈ (Nat.bit false n).bitIndices ↔ (Nat.bit false n).testBit 0 = true
⊢ i ∈ (Nat.bit false n).bitIndices ↔ (Nat.bit false n).testBit i = true
have bit₁ : ∀ (n_1 : ℕ), n_1 + 1 ∈ (Nat.bit false n).bitIndices ↔ (Nat.bit false n).testBit (n_1 + 1) = true
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit true n).bitIndices ↔ (bit true n).testBit i = true
have bit : 0 ∈ (bit true n).bitIndices ↔ (bit true n).testBit 0 = true
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
bit : 0 ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit 0 = true
⊢ i ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit i = true
have bit₁ : ∀ (n_1 : ℕ), n_1 + 1 ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit (n_1 + 1) = true
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
i n : ℕ
⊢ i ∈ n.bitIndices ↔ n.testBit i = true
have zero : ∀ {i : ℕ}, i ∈ bitIndices 0 ↔ testBit 0 i = true
Tactic: induction n using Nat.binaryRec generalizing i with
  | zero => simp
  | bit b n ih => cases b <;> cases i <;> simp_all [Nat.testBit_add_one, Nat.mul_add_div]
Cleared hypotheses: i, n
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
i n : ℕ
zero : ∀ {i : ℕ}, i ∈ bitIndices 0 ↔ testBit 0 i = true
⊢ i ∈ n.bitIndices ↔ n.testBit i = true
have bit : ∀ (b : Bool) (n : ℕ) (ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true) {i : ℕ},
  i ∈ (bit b n).bitIndices ↔ (bit b n).testBit i = true
Tactic: induction n using Nat.binaryRec generalizing i with
  | zero => simp
  | bit b n ih => cases b <;> cases i <;> simp_all [Nat.testBit_add_one, Nat.mul_add_div]
Cleared hypotheses: i, n
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
a : ℕ
L : List ℕ
hL : (a :: L).SortedLT
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
have haL : ∀ (a' : ℕ), a' ∈ L → a < a'
Tactic: obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
a : ℕ
L : List ℕ
hL : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
have hL₁ : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
Tactic: obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
have haL₁ : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
Tactic: simp_rw [Nat.lt_iff_add_one_le] at haL
Cleared hypotheses: haL
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = map (fun (x : ℕ) ↦ x + a + 1) L₀
have refine_1 : SortedLT (α := ℕ) (map (fun (x : ℕ) ↦ x - (a + 1)) L)
Tactic: refine ⟨L.map (· - (a+1)), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
refine_1 : SortedLT (α := ℕ) (map (fun (x : ℕ) ↦ x - (a + 1)) L)
⊢ ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = map (fun (x : ℕ) ↦ x + a + 1) L₀
have refine_2 : L = map (fun (x : ℕ) ↦ x + a + 1) (map (fun (x : ℕ) ↦ x - (a + 1)) L)
Tactic: refine ⟨L.map (· - (a+1)), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ SortedLT (α := ℕ) (map (fun (x : ℕ) ↦ x - (a + 1)) L)
have refine_1 : ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b
Tactic: rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b
have refine_1 : ∀ (a_1 b : ℕ), a_1 ∈ L → b ∈ L → (a_1 - (a + 1) < b - (a + 1) ↔ a_1 < b)
Tactic: simp only [and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x y : ℕ
hx : x ∈ L
h : y ∈ L
⊢ x - (a + 1) < y - (a + 1) ↔ x < y
have rw : x < y ↔ x < y
Tactic: rw [tsub_lt_tsub_iff_right (haL _ hx)]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x : ℕ
hx : x ∈ L
⊢ ((fun (x : ℕ) ↦ x + a + 1) ∘ fun (x : ℕ) ↦ x - (a + 1)) x = x
have simp : x - (a + 1) + (a + 1) = x
Tactic: simp only [add_assoc, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x : ℕ
hx : x ∈ L
⊢ x - (a + 1) + (a + 1) = x
have rw : x = x
Tactic: rw [tsub_add_cancel_of_le (haL _ hx)]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ L = map (fun (x : ℕ) ↦ x + a + 1) (map (fun (x : ℕ) ↦ x - (a + 1)) L)
have h' : ∀ (x : ℕ), x ∈ L → ((fun (x : ℕ) ↦ x + a + 1) ∘ fun (x : ℕ) ↦ x - (a + 1)) x = x
Tactic: have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
      simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
have h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = map (fun (x : ℕ) ↦ x + a + 1) L₀
Tactic: have h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = L₀.map (· + a + 1) := by
    refine ⟨L.map (· - (a+1)), ?_, ?_⟩
    · rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
      simp only [and_congr_right_iff]
      exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
    have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
      simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
    simp [List.map_congr_left h']
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = map (fun (x : ℕ) ↦ x + a + 1) L₀
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
have cons : ∀ (L₀ : List ℕ) (hL₀ : L₀.SortedLT) (hL : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT)
  (hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀))
  (haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'),
  bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀))) =
    a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
Tactic: obtain ⟨L₀, hL₀, rfl⟩ := h'
Cleared hypotheses: L, hL_1, hL, haL, h'
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL_1 : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'
⊢ Eq (α := ℕ → ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) fun (i : ℕ) ↦
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 i)
have h : ∀ (x : ℕ),
  ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) x =
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL_1 : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'
x : ℕ
⊢ ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) x =
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)
have h : HPow.hPow (α := ℕ) 2 x * HPow.hPow (α := ℕ) 2 a * 2 = HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)
Tactic: simp only [Function.comp_apply, pow_add, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL_1 : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀))) =
    a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
have hrw : Eq (α := ℕ → ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) fun (i : ℕ) ↦
  HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 i)
Tactic: have hrw : (2 ^ ·) ∘ (· + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i) := by
    ext x; simp only [Function.comp_apply, pow_add, pow_one]; ac_rfl
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL_1 : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'
hrw :
  Eq (α := ℕ → ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) fun (i : ℕ) ↦
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 i)
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀))) =
    a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
have cons : (HPow.hPow (α := ℕ) 2 a + HPow.hPow (α := ℕ) 2 a * (2 * (map (HPow.hPow (α := ℕ) 2) L₀).sum)).bitIndices =
  a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
Tactic: simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL_1 : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'
hrw :
  Eq (α := ℕ → ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) fun (i : ℕ) ↦
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 i)
⊢ (HPow.hPow (α := ℕ) 2 a + HPow.hPow (α := ℕ) 2 a * (2 * (map (HPow.hPow (α := ℕ) 2) L₀).sum)).bitIndices =
    a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
have cons : (HPow.hPow (α := ℕ) 2 a * 1 + HPow.hPow (α := ℕ) 2 a * (2 * (map (HPow.hPow (α := ℕ) 2) L₀).sum)).bitIndices =
  a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
Tactic: nth_rw 1 [← mul_one (a := 2 ^ a)]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL_1 : (a :: map (fun (x : ℕ) ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (map (fun (x : ℕ) ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), Membership.mem (γ := List ℕ) (map (fun (x : ℕ) ↦ x + a + 1) L₀) a' → a + 1 ≤ a'
hrw :
  Eq (α := ℕ → ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) fun (i : ℕ) ↦
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 i)
⊢ (HPow.hPow (α := ℕ) 2 a * 1 + HPow.hPow (α := ℕ) 2 a * (2 * (map (HPow.hPow (α := ℕ) 2) L₀).sum)).bitIndices =
    a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
have cons : map (fun (x : ℕ) ↦ x + a) (0 :: map (fun (x : ℕ) ↦ x + 1) L₀) = a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
Tactic: rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one,
    bitIndices_sum_map_two_pow hL₀]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
L : List ℕ
hL : L.SortedLT
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) L)) = L
have nil : ∀ (hL : SortedLT (α := ℕ) []), bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) [])) = []
Tactic: cases L with | nil => simp | cons a L =>
  obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise
  simp_rw [Nat.lt_iff_add_one_le] at haL
  have h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = L₀.map (· + a + 1) := by
    refine ⟨L.map (· - (a+1)), ?_, ?_⟩
    · rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
      simp only [and_congr_right_iff]
      exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
    have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
      simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
    simp [List.map_congr_left h']
  obtain ⟨L₀, hL₀, rfl⟩ := h'
  have hrw : (2 ^ ·) ∘ (· + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i) := by
    ext x; simp only [Function.comp_apply, pow_add, pow_one]; ac_rfl
  simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]
  nth_rw 1 [← mul_one (a := 2 ^ a)]
  rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one,
    bitIndices_sum_map_two_pow hL₀]
  simp [add_comm (a := 1), add_assoc]
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
L : List ℕ
hL : L.SortedLT
nil : ∀ (hL : SortedLT (α := ℕ) []), bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) [])) = []
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) L)) = L
have cons : ∀ (a : ℕ) (L : List ℕ) (hL : (a :: L).SortedLT),
  bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
Tactic: cases L with | nil => simp | cons a L =>
  obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise
  simp_rw [Nat.lt_iff_add_one_le] at haL
  have h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = L₀.map (· + a + 1) := by
    refine ⟨L.map (· - (a+1)), ?_, ?_⟩
    · rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
      simp only [and_congr_right_iff]
      exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
    have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
      simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
    simp [List.map_congr_left h']
  obtain ⟨L₀, hL₀, rfl⟩ := h'
  have hrw : (2 ^ ·) ∘ (· + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i) := by
    ext x; simp only [Function.comp_apply, pow_add, pow_one]; ac_rfl
  simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]
  nth_rw 1 [← mul_one (a := 2 ^ a)]
  rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one,
    bitIndices_sum_map_two_pow hL₀]
  simp [add_comm (a := 1), add_assoc]
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (hypothesis)
Goal:
n : ℕ
⊢ n.succ.testBit 0 = !n.testBit 0
have x : n % 2 = 0 ∨ n % 2 = 1
Tactic: cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)
have induction : (m + 0).bodd = (m.bodd ^^ bodd 0)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
induction : (m + 0).bodd = (m.bodd ^^ bodd 0)
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)
have succ : ∀ (n : ℕ), (m + n).bodd = (m.bodd ^^ n.bodd) → (m + (n + 1)).bodd = (m.bodd ^^ (n + 1).bodd)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)
have succ : (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)
Tactic: simp only [mul_succ, bodd_add, IH, bodd_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)
have succ : (false && n.bodd ^^ false) = (false && !n.bodd)
Tactic: cases bodd m
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (false && n.bodd ^^ false) = (false && !n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)
have succ₁ : (true && n.bodd ^^ true) = (true && !n.bodd)
Tactic: cases bodd m
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)
have succ : (false && false ^^ false) = (false && !false)
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (false && false ^^ false) = (false && !false)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)
have succ₁ : (false && true ^^ false) = (false && !true)
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)
have succ : (true && false ^^ true) = (true && !false)
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (true && false ^^ true) = (true && !false)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)
have succ₁ : (true && true ^^ true) = (true && !true)
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
⊢ (m * n).bodd = (m.bodd && n.bodd)
have zero : (m * 0).bodd = (m.bodd && bodd 0)
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    simp only [mul_succ, bodd_add, IH, bodd_succ]
    cases bodd m <;> cases bodd n <;> rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
m n : ℕ
zero : (m * 0).bodd = (m.bodd && bodd 0)
⊢ (m * n).bodd = (m.bodd && n.bodd)
have succ : ∀ (n : ℕ) (IH : (m * n).bodd = (m.bodd && n.bodd)), (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    simp only [mul_succ, bodd_add, IH, bodd_succ]
    cases bodd m <;> cases bodd n <;> rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
⊢ (bit b n).bodd = b
have false : (bit false n).bodd = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
false : (bit Bool.false n).bodd = Bool.false
⊢ (bit b n).bodd = b
have true : (bit true n).bodd = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
⊢ bit b n % 2 = (bit b n).bodd.toNat
have bit : bit false n % 2 = (bit false n).bodd.toNat
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
bit : Nat.bit false n % 2 = (Nat.bit false n).bodd.toNat
⊢ Nat.bit b n % 2 = (Nat.bit b n).bodd.toNat
have bit₁ : Nat.bit true n % 2 = (Nat.bit true n).bodd.toNat
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
n : ℕ
⊢ n % 2 = n.bodd.toNat
have bit : ∀ (b : Bool) (n : ℕ), bit b n % 2 = (bit b n).bodd.toNat
Tactic: cases n using bitCasesOn with
  | bit b n => cases b <;> simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
⊢ (bit b n + 1).div2 = bif (bit b n).bodd then (bit b n).div2.succ else (bit b n).div2
have bit : (bit false n + 1).div2 = bif (bit false n).bodd then (bit false n).div2.succ else (bit false n).div2
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bits (goal)
Goal:
b : Bool
n : ℕ
bit :
  (Nat.bit false n + 1).div2 = bif (Nat.bit false n).bodd then (Nat.bit false n).div2.succ else (Nat.bit false n).div2
⊢ (Nat.bit b n + 1).div2 = bif (Nat.bit b n).bodd then (Nat.bit b n).div2.succ else (Nat.bit b n).div2
have bit₁ : (Nat.bit true n + 1).div2 = bif (Nat.bit true n).bodd then (Nat.bit true n).div2.succ else (Nat.bit true n).div2
Tactic: cases b
Cleared hypotheses: b