awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
change :
  Eq.rec (motive :=
      fun (x : Sort u)
        (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
      x)
      (bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
        (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)))
      ⋯ =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
⊢ (have x : motive (Nat.bit (1 &&& Nat.bit b n != 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) :=
      bit (1 &&& Nat.bit b n != 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
        (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1));
    Eq.rec (motive :=
      fun (x : Sort u)
        (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
      x) x ⋯) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)

Tactic:
change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
generalize :
  ∀
    (e :
      motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) =
        motive (Nat.bit b n)),
    Eq.rec (motive :=
        fun (x : Sort u)
          (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
        x)
        (bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
          (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit
            (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)))
        e =
      bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
⊢ Eq.rec (motive :=
      fun (x : Sort u)
        (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
      x)
      (bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
        (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)))
      ⋯ =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)

Tactic:
generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e

Premises used: Nat.bit, congrArg, Nat.bit_testBit_zero_shiftRight_one
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e :
  motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = motive (Nat.bit b n)
revert :
  ∀
    (e :
      motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) =
        motive (Nat.bit b n)),
    Eq.rec (motive :=
        fun (x : Sort u)
          (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
        x)
        (bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
          (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit
            (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)))
        e =
      bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
⊢ Eq.rec (motive :=
      fun (x : Sort u)
        (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
      x)
      (bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
        (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)))
      e =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)

Tactic:
revert e
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
rw :
  ∀ (e : motive (Nat.bit b n) = motive (Nat.bit b n)),
    Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit b n) = x) ↦ x)
        (bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)) e =
      bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
⊢ ∀
    (e :
      motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) =
        motive (Nat.bit b n)),
    Eq.rec (motive :=
        fun (x : Sort u)
          (h : motive (Nat.bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)) = x) ↦
        x)
        (bit ((Nat.bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)
          (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit
            (HShiftRight.hShiftRight (β := Nat) (Nat.bit b n) 1)))
        e =
      bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)

Tactic:
rw [testBit_bit_zero, bit_shiftRight_one]

Premises used: Nat.testBit_bit_zero, Nat.bit_shiftRight_one
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e : motive (Nat.bit b n) = motive (Nat.bit b n)
⊢ Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit b n) = x) ↦ x)
      (bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)) e =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
rw :
  binaryRec (motive := fun (x : Nat) ↦ motive x) zero
      (fun (b : Bool) (n : Nat) (ih : motive n) ↦
        if h : n = 0 → b = true then bit b n h ih
        else
          have this := ⋯;
          Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
      0 =
    zero
rw₁ rw₂ : zero = zero
⊢ binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit 0 = zero

Tactic:
rw [binaryRec', binaryRec_zero]

Premises used: Nat.binaryRec_zero
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ Eq (α := Nat) 0 0 → true = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
rw :
  binaryRec (motive := fun (x : Nat) ↦ motive x) zero
      (fun (b : Bool) (n : Nat) (ih : motive n) ↦
        if h : n = 0 → b = true then bit b n h ih
        else
          have this := ⋯;
          Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
      1 =
    bit true 0 binaryRec'_one._proof_1 zero
rw₁ :
  (if h : Eq (α := Nat) 0 0 → true = true then bit true 0 h zero
    else
      have this := ⋯;
      Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯) =
    bit true 0 binaryRec'_one._proof_1 zero
rw₂ : bit true 0 binaryRec'_one._proof_1 zero = bit true 0 binaryRec'_one._proof_1 zero
hc : Eq (α := Nat) 0 0 → true = true
rw₃ : bit true 0 binaryRec'_one._proof_1 zero = bit true 0 binaryRec'_one._proof_1 zero
hc₁ : Eq (α := Nat) 0 0 → true = true
⊢ binaryRec' (motive := motive) zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero

Tactic:
rw [binaryRec', binaryRec_one, dif_pos]

Premises used: dif_pos, Nat.binaryRec_one
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ (if h : Eq (α := Nat) 0 0 → false = true then bit false 0 h zero
      else
        have this := ⋯;
        Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯) =
      zero ∨
    (n = 0 → b = true)

Tactic:
simp
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
rw :
  binaryRec (motive := fun (x : Nat) ↦ motive x) zero
      (fun (b : Bool) (n : Nat) (ih : motive n) ↦
        if h : n = 0 → b = true then bit b n h ih
        else
          have this := ⋯;
          Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
      (Nat.bit b n) =
    bit b n h (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit n)
rw₁ :
  (if h : n = 0 → b = true then
      bit b n h
        (binaryRec (motive := fun (x : Nat) ↦ motive x) zero
          (fun (b : Bool) (n : Nat) (ih : motive n) ↦
            if h : n = 0 → b = true then bit b n h ih
            else
              have this := ⋯;
              Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
          n)
    else
      have this := ⋯;
      Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯) =
    bit b n h (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit n)
rw₂ :
  bit b n h
      (binaryRec (motive := fun (x : Nat) ↦ motive x) zero
        (fun (b : Bool) (n : Nat) (ih : motive n) ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
        n) =
    bit b n h (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit n)
rw₃ rw₄ :
  bit b n h
      (binaryRec (motive := fun (x : Nat) ↦ motive x) zero
        (fun (b : Bool) (n : Nat) (ih : motive n) ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
        n) =
    bit b n h
      (binaryRec (motive := fun (x : Nat) ↦ motive x) zero
        (fun (b : Bool) (n : Nat) (ih : motive n) ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯)
        n)
⊢ binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n h (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit n)

Tactic:
rw [binaryRec', binaryRec_eq _ _ (by simp), dif_pos h, binaryRec']

Premises used: dif_pos, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
⊢ binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit 0 = zero

Tactic:
binaryRec'_zero _ _

Premises used: Nat.binaryRec'_zero, Nat.binaryRecFromOne
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
rw :
  binaryRec' (motive := fun (x : Nat) ↦ motive x) zero
      (fun (b : Bool) (n : Nat) (h : n = 0 → b = true) (ih : motive n) ↦
        if h' : n = 0 then
          have this := ⋯;
          Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
        else bit b n h' ih)
      1 =
    one
rw₁ :
  (if h' : Eq (α := Nat) 0 0 then
      have this := ⋯;
      Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
    else bit true 0 h' zero) =
    one
rw₂ rw₃ :
  (have this := ⋯;
    Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯) =
    one
⊢ binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit 1 = one

Tactic:
rw [binaryRecFromOne, binaryRec'_one, dif_pos rfl]

Premises used: dif_pos, Nat.binaryRec'_one, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
⊢ n = 0 → b = true

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
rw :
  binaryRec' (motive := fun (x : Nat) ↦ motive x) zero
      (fun (b : Bool) (n : Nat) (h : n = 0 → b = true) (ih : motive n) ↦
        if h' : n = 0 then
          have this := ⋯;
          Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
        else bit b n h' ih)
      (Nat.bit b n) =
    bit b n h (binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit n)
rw₁ :
  (if h' : n = 0 then
      have this := ⋯;
      Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
    else
      bit b n h'
        (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero
          (fun (b : Bool) (n : Nat) (h : n = 0 → b = true) (ih : motive n) ↦
            if h' : n = 0 then
              have this := ⋯;
              Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
            else bit b n h' ih)
          n)) =
    bit b n h (binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit n)
rw₂ :
  bit b n h
      (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero
        (fun (b : Bool) (n : Nat) (h : n = 0 → b = true) (ih : motive n) ↦
          if h' : n = 0 then
            have this := ⋯;
            Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
          else bit b n h' ih)
        n) =
    bit b n h (binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit n)
rw₃ rw₄ :
  bit b n h
      (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero
        (fun (b : Bool) (n : Nat) (h : n = 0 → b = true) (ih : motive n) ↦
          if h' : n = 0 then
            have this := ⋯;
            Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
          else bit b n h' ih)
        n) =
    bit b n h
      (binaryRec' (motive := fun (x : Nat) ↦ motive x) zero
        (fun (b : Bool) (n : Nat) (h : n = 0 → b = true) (ih : motive n) ↦
          if h' : n = 0 then
            have this := ⋯;
            Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one ⋯
          else bit b n h' ih)
        n)
⊢ binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit (Nat.bit b n) =
    bit b n h (binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit n)

Tactic:
rw [binaryRecFromOne, binaryRec'_eq _ _ (by simp [h]), dif_neg h, binaryRecFromOne]

Premises used: dif_neg, Nat.binaryRec'_eq
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
⊢ bitIndices 0 = []

Tactic:
simp [bitIndices]

Premises used: Nat.bitIndices
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
⊢ bitIndices 1 = [0]

Tactic:
simp [bitIndices]

Premises used: Nat.bitIndices
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
⊢ (bit true n).bitIndices = 0 :: map (fun (x : ℕ) ↦ x + 1) n.bitIndices

Tactic:
binaryRec_eq _ _ (.inl rfl)

Premises used: Nat.bitIndices, Or.inl, rfl, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
⊢ (bit false n).bitIndices = map (fun (x : ℕ) ↦ x + 1) n.bitIndices

Tactic:
binaryRec_eq _ _ (.inl rfl)

Premises used: Nat.bitIndices, Or.inl, rfl, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
rw : (2 * n + 1).bitIndices = (bit true n).bitIndices
rw₁ rw₂ : (2 * n + 1).bitIndices = bitIndices ((fun (x : ℕ) ↦ 2 * x + 1) n)
⊢ (2 * n + 1).bitIndices = 0 :: map (fun (x : ℕ) ↦ x + 1) n.bitIndices

Tactic:
rw [← bitIndices_bit_true, bit_true]

Premises used: Nat.bit_true, Nat.bitIndices_bit_true
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
rw : (2 * n).bitIndices = (bit false n).bitIndices
rw₁ rw₂ : (2 * n).bitIndices = bitIndices ((fun (x : ℕ) ↦ 2 * x) n)
⊢ (2 * n).bitIndices = map (fun (x : ℕ) ↦ x + 1) n.bitIndices

Tactic:
rw [← bitIndices_bit_false, bit_false]

Premises used: Nat.bit_false, Nat.bitIndices_bit_false
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
⊢ (bitIndices 0).SortedLT

Tactic:
simp [sortedLT_iff_pairwise]

Premises used: List.sortedLT_iff_pairwise
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices
false : (bit Bool.false n).bitIndices.SortedLT
true : (bit Bool.true n).bitIndices.SortedLT
⊢ (bit b n).bitIndices.SortedLT

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices
⊢ (bit false n).bitIndices.SortedLT

Tactic:
simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]

Premises used: List.sortedLT_iff_pairwise, Nat.bit_true, List.pairwise_map, Nat.bit_false
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices
⊢ (bit true n).bitIndices.SortedLT

Tactic:
simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]

Premises used: List.sortedLT_iff_pairwise, Nat.bit_true, List.pairwise_map, Nat.bit_false
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
bit : List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices
⊢ (Nat.bit b n).bitIndices.SortedLT

Tactic:
suffices List.Pairwise (fun a b ↦ a < b) n.bitIndices by
      cases b <;> simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ ∀ {a b : ℕ}, a < b → a < b

Tactic:
simp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices

Tactic:
exact List.Pairwise.imp (by simp) hs.pairwise

Premises used: List.SortedLT.pairwise, List.Pairwise.imp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
zero : (bitIndices 0).SortedLT
bit : ∀ (b : Bool) (n : ℕ) (hs : n.bitIndices.SortedLT), (Nat.bit b n).bitIndices.SortedLT
⊢ n.bitIndices.SortedLT

Tactic:
induction n using binaryRec with
  | zero => simp [sortedLT_iff_pairwise]
  | bit b n hs =>
    suffices List.Pairwise (fun a b ↦ a < b) n.bitIndices by
      cases b <;> simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]
    exact List.Pairwise.imp (by simp) hs.pairwise

Premises used: Nat.bit, List.sortedLT_iff_pairwise, Nat.zero
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
⊢ n.bitIndices.Nodup

Tactic:
bitIndices_sorted.pairwise.nodup

Premises used: Nat.bitIndices_sorted, List.SortedLT.pairwise, List.Pairwise.nodup
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n : ℕ
⊢ (HPow.hPow (α := ℕ) (β := ℕ) 2 0 * n).bitIndices = map (fun (x : ℕ) ↦ x + 0) n.bitIndices

Tactic:
simp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n k : ℕ
ih : (HPow.hPow (α := ℕ) 2 k * n).bitIndices = map (fun (x : ℕ) ↦ x + k) n.bitIndices
succ : Eq (α := List ℕ) (map (fun (x : ℕ) ↦ x + (k + 1)) n.bitIndices) (map (fun (x : ℕ) ↦ x + (1 + k)) n.bitIndices)
⊢ (HPow.hPow (α := ℕ) 2 (k + 1) * n).bitIndices = map (fun (x : ℕ) ↦ x + (k + 1)) n.bitIndices

Tactic:
rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]

Premises used: mul_assoc, pow_add, List.map_map, comp_add_right, add_comm, pow_one, Nat.bitIndices_two_mul
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
n k : ℕ
ih : (HPow.hPow (α := ℕ) 2 k * n).bitIndices = map (fun (x : ℕ) ↦ x + k) n.bitIndices
⊢ Eq (α := List ℕ) (map (fun (x : ℕ) ↦ x + (k + 1)) n.bitIndices) (map (fun (x : ℕ) ↦ x + (1 + k)) n.bitIndices)

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

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
k n : ℕ
zero : (HPow.hPow (α := ℕ) (β := ℕ) 2 0 * n).bitIndices = map (fun (x : ℕ) ↦ x + 0) n.bitIndices
succ :
  ∀ (k : ℕ) (ih : (HPow.hPow (α := ℕ) 2 k * n).bitIndices = map (fun (x : ℕ) ↦ x + k) n.bitIndices),
    (HPow.hPow (α := ℕ) 2 (k + 1) * n).bitIndices = map (fun (x : ℕ) ↦ x + (k + 1)) n.bitIndices
⊢ (HPow.hPow (α := ℕ) 2 k * n).bitIndices = map (fun (x : ℕ) ↦ x + k) n.bitIndices

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]
    simp [add_comm (a := 1)]

Premises used: mul_assoc, pow_add, List.map_map, comp_add_right, add_comm, pow_one, Nat.zero, Nat.bitIndices_two_mul, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
k : ℕ
rw : map (fun (x : ℕ) ↦ x + k) (bitIndices 1) = [k]
⊢ (HPow.hPow (α := ℕ) 2 k).bitIndices = [k]

Tactic:
rw [← mul_one (a := 2 ^ k), bitIndices_two_pow_mul]

Premises used: HPow.hPow, mul_one, Nat.bitIndices_two_pow_mul, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
k : ℕ
⊢ map (fun (x : ℕ) ↦ x + k) (bitIndices 1) = [k]

Tactic:
simp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
⊢ Eq (α := ℕ) (sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bitIndices 0))) 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n
h : ∀ (i : ℕ), ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) i = 2 * HPow.hPow (α := ℕ) 2 i
⊢ Eq (α := ℕ → ℕ) ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) fun (i : ℕ) ↦
    2 * HPow.hPow (α := ℕ) 2 i

Tactic:
ext i
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n
i : ℕ
⊢ ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) i = 2 * HPow.hPow (α := ℕ) 2 i

Tactic:
simp [pow_add, mul_comm]

Premises used: pow_add, mul_comm
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
b : Bool
n : ℕ
hs : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) n.bitIndices) = n
⊢ Eq (α := ℕ → ℕ) ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) fun (i : ℕ) ↦
    2 * HPow.hPow (α := ℕ) 2 i

Tactic:
have hrw : (fun i ↦ 2 ^ i) ∘ (fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i := by
      ext i; simp [pow_add, mul_comm]
-- Module: Mathlib.Data.Nat.BitIndices
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
bit₁ : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (Nat.bit true n).bitIndices) = Nat.bit true n
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (Nat.bit b n).bitIndices) = Nat.bit b n

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
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
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bit false n).bitIndices) = bit false n

Tactic:
simpa [hrw, List.sum_map_mul_left]

Premises used: List.sum_map_mul_left
-- Module: Mathlib.Data.Nat.BitIndices
Goal:
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
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bit true n).bitIndices) = bit true n

Tactic:
simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]

Premises used: add_comm, List.sum_map_mul_left, OfNat.ofNat