awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRec' (motive := motive) zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero
have rw₂ : bit true 0 binaryRec'_one._proof_1 zero = bit true 0 binaryRec'_one._proof_1 zero
Tactic: rw [binaryRec', binaryRec_one, dif_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRec' (motive := motive) zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero
have hc : Eq (α := Nat) 0 0 → true = true
Tactic: rw [binaryRec', binaryRec_one, dif_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ 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)
have 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 := sorry;
        Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry)
    (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']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have 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 := sorry;
            Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry)
        n)
  else
    have this := sorry;
    Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry) =
  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']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have 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 := sorry;
          Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry)
      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']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have 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 := sorry;
          Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry)
      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 := sorry;
          Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry)
      n)
Tactic: rw [binaryRec', binaryRec_eq _ _ (by simp), dif_pos h, binaryRec']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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 1 = one
have 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 := sorry;
        Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
      else bit b n h' ih)
    1 =
  one
Tactic: rw [binaryRecFromOne, binaryRec'_one, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit 1 = one
have rw₁ : (if h' : Eq (α := Nat) 0 0 then
    have this := sorry;
    Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
  else bit true 0 h' zero) =
  one
Tactic: rw [binaryRecFromOne, binaryRec'_one, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRecFromOne (motive := fun (x : Nat) ↦ motive x) zero one bit 1 = one
have rw₂ : (have this := sorry;
  Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry) =
  one
Tactic: rw [binaryRecFromOne, binaryRec'_one, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ 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)
have 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 := sorry;
        Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
      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)
Tactic: rw [binaryRecFromOne, binaryRec'_eq _ _ (by simp [h]), dif_neg h, binaryRecFromOne]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have rw₁ : (if h' : n = 0 then
    have this := sorry;
    Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
  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 := sorry;
            Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
          else bit b n h' ih)
        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]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have 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 := sorry;
          Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
        else bit b n h' ih)
      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]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have 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 := sorry;
          Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
        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 := sorry;
          Eq.rec (motive := fun (x : Sort u) (h : motive (Nat.bit true 0) = x) ↦ x) one sorry
        else bit b n h' ih)
      n)
Tactic: rw [binaryRecFromOne, binaryRec'_eq _ _ (by simp [h]), dif_neg h, binaryRecFromOne]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
⊢ (2 * n + 1).bitIndices = 0 :: map (fun (x : ℕ) ↦ x + 1) n.bitIndices
have rw : (2 * n + 1).bitIndices = (bit true n).bitIndices
Tactic: rw [← bitIndices_bit_true, bit_true]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
rw : (2 * n + 1).bitIndices = (bit true n).bitIndices
⊢ (2 * n + 1).bitIndices = 0 :: map (fun (x : ℕ) ↦ x + 1) n.bitIndices
have rw₁ : (2 * n + 1).bitIndices = bitIndices ((fun (x : ℕ) ↦ 2 * x + 1) n)
Tactic: rw [← bitIndices_bit_true, bit_true]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
⊢ (2 * n).bitIndices = map (fun (x : ℕ) ↦ x + 1) n.bitIndices
have rw : (2 * n).bitIndices = (bit false n).bitIndices
Tactic: rw [← bitIndices_bit_false, bit_false]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
rw : (2 * n).bitIndices = (bit false n).bitIndices
⊢ (2 * n).bitIndices = map (fun (x : ℕ) ↦ x + 1) n.bitIndices
have rw₁ : (2 * n).bitIndices = bitIndices ((fun (x : ℕ) ↦ 2 * x) n)
Tactic: rw [← bitIndices_bit_false, bit_false]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices
⊢ (bit b n).bitIndices.SortedLT
have false : (bit false n).bitIndices.SortedLT
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
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
⊢ (bit b n).bitIndices.SortedLT
have true : (bit true n).bitIndices.SortedLT
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ (bit b n).bitIndices.SortedLT
have bit : List.Pairwise (fun (a b : ℕ) ↦ a < b) n.bitIndices
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]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
⊢ n.bitIndices.SortedLT
have zero : (bitIndices 0).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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n : ℕ
zero : (bitIndices 0).SortedLT
⊢ n.bitIndices.SortedLT
have bit : ∀ (b : Bool) (n : ℕ) (hs : n.bitIndices.SortedLT), (bit b 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
n 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
have succ : Eq (α := List ℕ) (map (fun (x : ℕ) ↦ x + (k + 1)) n.bitIndices) (map (fun (x : ℕ) ↦ x + (1 + k)) n.bitIndices)
Tactic: rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
k n : ℕ
⊢ (HPow.hPow (α := ℕ) 2 k * n).bitIndices = map (fun (x : ℕ) ↦ x + k) n.bitIndices
have zero : (HPow.hPow (α := ℕ) (β := ℕ) 2 0 * n).bitIndices = map (fun (x : ℕ) ↦ x + 0) 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)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
k n : ℕ
zero : (HPow.hPow (α := ℕ) (β := ℕ) 2 0 * n).bitIndices = map (fun (x : ℕ) ↦ x + 0) n.bitIndices
⊢ (HPow.hPow (α := ℕ) 2 k * n).bitIndices = map (fun (x : ℕ) ↦ x + k) n.bitIndices
have 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
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)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (goal)
Goal:
k : ℕ
⊢ (HPow.hPow (α := ℕ) 2 k).bitIndices = [k]
have rw : map (fun (x : ℕ) ↦ x + k) (bitIndices 1) = [k]
Tactic: rw [← mul_one (a := 2 ^ k), bitIndices_two_pow_mul]
-- 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
⊢ Eq (α := ℕ → ℕ) ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) fun (i : ℕ) ↦
    2 * HPow.hPow (α := ℕ) 2 i
have h : ∀ (i : ℕ), ((fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) ∘ fun (x : ℕ) ↦ x + 1) i = 2 * HPow.hPow (α := ℕ) 2 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Nat.BitIndices (hypothesis)
Goal:
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
have hrw : 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]
-- 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
⊢ sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bit b n).bitIndices) = bit b n
have bit : sum (map (fun (i : ℕ) ↦ HPow.hPow (α := ℕ) 2 i) (bit false n).bitIndices) = bit false n
Tactic: cases b
Cleared hypotheses: b