awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
zero : Eq (α := ℕ) (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bitIndices 0))) 0
bit :
  ∀ (b : Bool) (n : ℕ) (hs : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n),
    sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (Nat.bit b n).bitIndices) = Nat.bit b n
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = 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)]

Premises used: Nat.bit, add_comm, List.sum_map_mul_left, Nat.zero, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
i : ℕ
⊢ i ∈ bitIndices 0 ↔ testBit 0 i = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.BitIndices
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
bit₁ : i ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit i = true
⊢ i ∈ (Nat.bit b n).bitIndices ↔ (Nat.bit b n).testBit i = true

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BitIndices
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
bit₁ : ∀ (n_1 : ℕ), n_1 + 1 ∈ (Nat.bit false n).bitIndices ↔ (Nat.bit false n).testBit (n_1 + 1) = true
⊢ i ∈ (Nat.bit false n).bitIndices ↔ (Nat.bit false n).testBit i = true

Tactic:
cases i
-- Module: Mathlib.Data.Nat.BitIndices
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
bit₁ : ∀ (n_1 : ℕ), n_1 + 1 ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit (n_1 + 1) = true
⊢ i ∈ (Nat.bit true n).bitIndices ↔ (Nat.bit true n).testBit i = true

Tactic:
cases i
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit false n).bitIndices ↔ (bit false n).testBit 0 = true

Tactic:
simp_all [Nat.testBit_add_one, Nat.mul_add_div]

Premises used: Nat.mul_add_div, Nat.testBit_add_one
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n_1 : ℕ
⊢ n_1 + 1 ∈ (bit false n).bitIndices ↔ (bit false n).testBit (n_1 + 1) = true

Tactic:
simp_all [Nat.testBit_add_one, Nat.mul_add_div]

Premises used: Nat.mul_add_div, Nat.testBit_add_one
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit true n).bitIndices ↔ (bit true n).testBit 0 = true

Tactic:
simp_all [Nat.testBit_add_one, Nat.mul_add_div]

Premises used: Nat.mul_add_div, Nat.testBit_add_one
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n_1 : ℕ
⊢ n_1 + 1 ∈ (bit true n).bitIndices ↔ (bit true n).testBit (n_1 + 1) = true

Tactic:
simp_all [Nat.testBit_add_one, Nat.mul_add_div]

Premises used: Nat.mul_add_div, Nat.testBit_add_one
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
i n : ℕ
zero : ∀ {i : ℕ}, i ∈ bitIndices 0 ↔ testBit 0 i = true
bit :
  ∀ (b : Bool) (n : ℕ) (ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true) {i : ℕ},
    i ∈ (Nat.bit b n).bitIndices ↔ (Nat.bit b n).testBit i = true
⊢ i ∈ n.bitIndices ↔ 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]

Premises used: Nat.bit, Nat.mul_add_div, Nat.zero, Nat.testBit_add_one
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
hL : SortedLT (α := ℕ) []
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) [])) = []

Tactic:
simp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
a : ℕ
L : List ℕ
hL : (a :: L).SortedLT
⊢ ∀ (a' : ℕ), a' ∈ L → a < a'

Tactic:
obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise

Premises used: List.SortedLT.pairwise, List.pairwise_cons, Iff.mp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
a : ℕ
L : List ℕ
hL : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
⊢ List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L

Tactic:
obtain ⟨haL, hL⟩ := pairwise_cons.1 hL.pairwise

Premises used: List.SortedLT.pairwise, List.pairwise_cons, Iff.mp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
a : ℕ
L : List ℕ
hL_1 : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
hL : List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L
⊢ ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'

Tactic:
simp_rw [Nat.lt_iff_add_one_le] at haL

Premises used: Nat.lt_iff_add_one_le
-- Module: Mathlib.Data.Nat.BitIndices
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₀

Tactic:
⟨L.map (· - (a+1)), ?_, ?_⟩

Premises used: List.map, HSub.hSub, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BitIndices
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)
refine_2 : L = map (fun (x : ℕ) ↦ x + a + 1) (map (fun (x : ℕ) ↦ x - (a + 1)) L)
⊢ ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = map (fun (x : ℕ) ↦ x + a + 1) L₀

Tactic:
refine ⟨L.map (· - (a+1)), ?_, ?_⟩
-- Module: Mathlib.Data.Nat.BitIndices
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 : ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b
⊢ SortedLT (α := ℕ) (map (fun (x : ℕ) ↦ x - (a + 1)) L)

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]

Premises used: List.sortedLT_iff_pairwise, List.Pairwise.and_mem, List.Pairwise.iff, List.pairwise_map
-- Module: Mathlib.Data.Nat.BitIndices
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 : ∀ (a_1 b : ℕ), a_1 ∈ L → b ∈ L → (a_1 - (a + 1) < b - (a + 1) ↔ a_1 < b)
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b

Tactic:
simp only [and_congr_right_iff]

Premises used: and_congr_right_iff
-- Module: Mathlib.Data.Nat.BitIndices
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
rw rw₁ : x < y ↔ x < y
⊢ x - (a + 1) < y - (a + 1) ↔ x < y

Tactic:
rw [tsub_lt_tsub_iff_right (haL _ hx)]

Premises used: tsub_lt_tsub_iff_right
-- Module: Mathlib.Data.Nat.BitIndices
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 < b)

Tactic:
exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
-- Module: Mathlib.Data.Nat.BitIndices
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
simp : x - (a + 1) + (a + 1) = x
⊢ ((fun (x : ℕ) ↦ x + a + 1) ∘ fun (x : ℕ) ↦ x - (a + 1)) x = x

Tactic:
simp only [add_assoc, Function.comp_apply]

Premises used: add_assoc, Function.comp_apply
-- Module: Mathlib.Data.Nat.BitIndices
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
rw rw₁ : x = x
⊢ x - (a + 1) + (a + 1) = x

Tactic:
rw [tsub_add_cancel_of_le (haL _ hx)]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Data.Nat.BitIndices
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 : ℕ), 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)]
-- Module: Mathlib.Data.Nat.BitIndices
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' : ∀ (x : ℕ), x ∈ L → ((fun (x : ℕ) ↦ x + a + 1) ∘ fun (x : ℕ) ↦ x - (a + 1)) x = x
⊢ L = map (fun (x : ℕ) ↦ x + a + 1) (map (fun (x : ℕ) ↦ x - (a + 1)) L)

Tactic:
simp [List.map_congr_left h']

Premises used: List.map_congr_left
-- Module: Mathlib.Data.Nat.BitIndices
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₀

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']
-- Module: Mathlib.Data.Nat.BitIndices
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₀
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₀
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L

Tactic:
obtain ⟨L₀, hL₀, rfl⟩ := h'

Premises used: rfl
-- Module: Mathlib.Data.Nat.BitIndices
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'
h :
  ∀ (x : ℕ),
    ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) x =
      HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)
⊢ Eq (α := ℕ → ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) fun (i : ℕ) ↦
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 i)

Tactic:
ext x
-- Module: Mathlib.Data.Nat.BitIndices
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 : ℕ
h : HPow.hPow (α := ℕ) 2 x * HPow.hPow (α := ℕ) 2 a * 2 = HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)
⊢ ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) ∘ fun (x : ℕ) ↦ x + a + 1) x =
    HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)

Tactic:
simp only [Function.comp_apply, pow_add, pow_one]

Premises used: pow_add, pow_one, Function.comp_apply
-- Module: Mathlib.Data.Nat.BitIndices
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 : ℕ
⊢ HPow.hPow (α := ℕ) 2 x * HPow.hPow (α := ℕ) 2 a * 2 = HPow.hPow (α := ℕ) 2 a * (2 * HPow.hPow (α := ℕ) 2 x)

Tactic:
ac_rfl
-- Module: Mathlib.Data.Nat.BitIndices
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)

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
-- Module: Mathlib.Data.Nat.BitIndices
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)
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₀
⊢ 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:
simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]

Premises used: List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons
-- Module: Mathlib.Data.Nat.BitIndices
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)
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₀
⊢ (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:
nth_rw 1 [← mul_one (a := 2 ^ a)]

Premises used: HPow.hPow, mul_one, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BitIndices
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)
cons : map (fun (x : ℕ) ↦ x + a) (0 :: map (fun (x : ℕ) ↦ x + 1) L₀) = a :: map (fun (x : ℕ) ↦ x + a + 1) L₀
⊢ (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:
rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one,
    bitIndices_sum_map_two_pow hL₀]

Premises used: add_comm, Nat.bitIndices_two_mul_add_one, mul_add, Nat.bitIndices_two_pow_mul
-- Module: Mathlib.Data.Nat.BitIndices
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)
⊢ map (fun (x : ℕ) ↦ x + a) (0 :: map (fun (x : ℕ) ↦ x + 1) L₀) = a :: map (fun (x : ℕ) ↦ x + a + 1) L₀

Tactic:
simp [add_comm (a := 1), add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
L : List ℕ
hL : L.SortedLT
nil : ∀ (hL : SortedLT (α := ℕ) []), bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) [])) = []
cons :
  ∀ (a : ℕ) (L : List ℕ) (hL : (a :: L).SortedLT),
    bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (a :: L))) = a :: L
⊢ bitIndices (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) L)) = 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]

Premises used: List.map_cons, add_assoc, List.map_map, Nat.lt_iff_add_one_le, add_comm, List.cons, List.pairwise_cons, List.sum_map_mul_left, Nat.bitIndices_two_mul_add_one, List.sum_cons, Iff.mp, mul_add, Nat.bitIndices_two_pow_mul, OfNat.ofNat, rfl, List.nil
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
a n : ℕ
ha : a ∈ n.bitIndices
⊢ n.testBit a = true

Tactic:
simpa using ha
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
⊢ ¬n ∈ n.bitIndices

Tactic:
fun h ↦ n.lt_two_pow_self.not_ge <| two_pow_le_of_mem_bitIndices h

Premises used: Nat.lt_two_pow_self, LT.lt.not_ge, Not, Nat.two_pow_le_of_mem_bitIndices
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ n.div2 = n / 2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bodd 0 = false

Tactic:
rfl

Premises used: Nat.testBit, rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bodd 1 = true

Tactic:
rfl

Premises used: Nat.testBit, rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bodd 2 = false

Tactic:
rfl

Premises used: Nat.testBit, rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
h : n % 2 = 0
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
simp [h, add_mod]

Premises used: Nat.add_mod
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
h : n % 2 = 1
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
simp [h, add_mod]

Premises used: Nat.add_mod
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ n % 2 = 0 ∨ n % 2 = 1

Tactic:
cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]

Premises used: Nat.mod_two_eq_zero_or_one, Nat.add_mod
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
induction : (m + 0).bodd = (m.bodd ^^ bodd 0)
succ : ∀ (n : ℕ), (m + n).bodd = (m.bodd ^^ n.bodd) → (m + (n + 1)).bodd = (m.bodd ^^ (n + 1).bodd)
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
induction n
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

Tactic:
case zero => simp

Premises used: Nat.zero
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
ih : (m + n).bodd = (m.bodd ^^ n.bodd)
⊢ (m + (n + 1)).bodd = (m.bodd ^^ (n + 1).bodd)

Tactic:
simp [← Nat.add_assoc, ih]

Premises used: Nat.add_assoc
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
⊢ (m * 0).bodd = (m.bodd && bodd 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)
⊢ (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)

Tactic:
simp only [mul_succ, bodd_add, IH, bodd_succ]

Premises used: Nat.mul_succ, Nat.bodd_add, Nat.bodd_succ
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (false && n.bodd ^^ false) = (false && !n.bodd)
succ₁ : (true && n.bodd ^^ true) = (true && !n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)

Tactic:
cases bodd m

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (false && false ^^ false) = (false && !false)
succ₁ : (false && true ^^ false) = (false && !true)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)

Tactic:
cases bodd n

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
succ : (true && false ^^ true) = (true && !false)
succ₁ : (true && true ^^ true) = (true && !true)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)

Tactic:
cases bodd n

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && false ^^ false) = (false && !false)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && true ^^ false) = (false && !true)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && false ^^ true) = (true && !false)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && true ^^ true) = (true && !true)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
zero : (m * 0).bodd = (m.bodd && bodd 0)
succ : ∀ (n : ℕ) (IH : (m * n).bodd = (m.bodd && n.bodd)), (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)
⊢ (m * n).bodd = (m.bodd && n.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

Premises used: Nat.mul_succ, Nat.bodd_add, Nat.zero, Nat.bodd_succ, Nat.bodd, Nat.succ
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
false : (bit Bool.false n).bodd = Bool.false
true : (bit Bool.true n).bodd = Bool.true
⊢ (bit b n).bodd = b

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (bit false n).bodd = false

Tactic:
simp [bodd]

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (bit true n).bodd = true

Tactic:
simp [bodd]

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
bit : Nat.bit false n % 2 = (Nat.bit false n).bodd.toNat
bit₁ : Nat.bit true n % 2 = (Nat.bit true n).bodd.toNat
⊢ Nat.bit b n % 2 = (Nat.bit b n).bodd.toNat

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ bit false n % 2 = (bit false n).bodd.toNat

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ bit true n % 2 = (bit true n).bodd.toNat

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
bit : ∀ (b : Bool) (n : ℕ), Nat.bit b n % 2 = (Nat.bit b n).bodd.toNat
⊢ n % 2 = n.bodd.toNat

Tactic:
cases n using bitCasesOn with
  | bit b n => cases b <;> simp

Premises used: Nat.bit, Nat.bitCasesOn
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ div2 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ div2 1 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ div2 2 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Bits
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
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
⊢ (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

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (bit false n + 1).div2 = bif (bit false n).bodd then (bit false n).div2.succ else (bit false n).div2

Tactic:
simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]

Premises used: Nat.dvd_add_right, Nat.div2_val, Nat.succ_div, Nat.bit_val, Nat.add_assoc, Nat.dvd_mul_right