awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = motive (bit b n)
⊢ Eq.rec (motive :=
      fun (x : Sort u) (h : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = x) ↦
      x) (h ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) e =
    h b n
have revert : ∀ (e : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = motive (bit b n)),
  Eq.rec (motive :=
      fun (x : Sort u) (h : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = x) ↦
      x) (h ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) e =
    h b n
Tactic: revert e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = motive (bit b n)),
    Eq.rec (motive :=
        fun (x : Sort u) (h : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = x) ↦
        x) (h ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) e =
      h b n
have rw : ∀ (e : motive (bit b n) = motive (bit b n)),
  Eq.rec (motive := fun (x : Sort u) (h : motive (bit b n) = x) ↦ x) (h b n) e = h b n
Tactic: rw [testBit_bit_zero, bit_shiftRight_one]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have by_cases : ∀ (h' : Nat.bit b n = 0),
  binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
Tactic: by_cases h' : n.bit b = 0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
by_cases :
  ∀ (h' : Nat.bit b n = 0),
    binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
      bit b n (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 (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have by_cases₁ : ∀ (h' : ¬Nat.bit b n = 0),
  binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
Tactic: by_cases h' : n.bit b = 0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have obtain : ∀ (h : bit false 0 zero = zero ∨ (Eq (α := Nat) 0 0 → false = true)) (h' : Nat.bit false 0 = 0),
  Eq (α := motive (Nat.bit false 0)) (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit false 0))
    (bit false 0 (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit 0))
Tactic: obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
Cleared hypotheses: b, n, h, h'
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (hypothesis)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h : bit false 0 zero = zero ∨ (Eq (α := Nat) 0 0 → false = true)
h' : Nat.bit false 0 = 0
⊢ Eq (α := motive (Nat.bit false 0)) (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit false 0))
    (bit false 0 (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit 0))
have h₁ : bit false 0 zero = zero
Tactic: simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ Eq (α := motive (Nat.bit false 0)) (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit false 0))
    (bit false 0 (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit 0))
have unfold : Eq (α := motive (Nat.bit false 0))
  (if n0 : Nat.bit false 0 = 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry
  else
    have x : motive (Nat.bit (1 &&& Nat.bit false 0 != 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit false 0) 1)) :=
      bit (1 &&& Nat.bit false 0 != 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit false 0) 1)
        (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit
          (HShiftRight.hShiftRight (β := Nat) (Nat.bit false 0) 1));
    Eq.rec (motive :=
      fun (x : Sort u)
        (h :
          motive (Nat.bit ((Nat.bit false 0).testBit 0) (HShiftRight.hShiftRight (β := Nat) (Nat.bit false 0) 1)) = x) ↦
      x) x sorry)
  (bit false 0
    (if n0 : Eq (α := Nat) 0 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry
    else
      have x : motive (Nat.bit (HAnd.hAnd (α := Nat) 1 0 != 0) (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1)) :=
        bit (HAnd.hAnd (α := Nat) 1 0 != 0) (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1)
          (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1));
      Eq.rec (motive :=
        fun (x : Sort u) (h : motive (Nat.bit (testBit 0 0) (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1)) = x) ↦
        x) x sorry))
Tactic: unfold binaryRec
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have rw : (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 sorry) =
  bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
Tactic: rw [binaryRec, dif_neg h']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ (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)
have 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)))
    sorry =
  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 _ _ _ = _
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ 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 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)
Tactic: generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)
⊢ 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)
have 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)
Tactic: revert e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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)),
    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)
have 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)
Tactic: rw [testBit_bit_zero, bit_shiftRight_one]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have case : (if n0 : Nat.bit b n = 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry
  else
    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 sorry) =
  bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
Tactic: case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
case :
  (if n0 : Nat.bit b n = 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯
    else
      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)
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have case₁ : (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 sorry) =
  bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
Tactic: case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
case :
  (if n0 : Nat.bit b n = 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯
    else
      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)
case₁ case₂ case₃ :
  (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)
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have case₄ : 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)))
    sorry =
  bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
Tactic: case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
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
case :
  (if n0 : Nat.bit b n = 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯
    else
      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)
case₁ case₂ case₃ :
  (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)
case₄ :
  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)
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit (Nat.bit b n) =
    bit b n (binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit n)
have case₅ : ∀
  (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: case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl
-- 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)
⊢ binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit 0 = zero
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)
    0 =
  zero
Tactic: rw [binaryRec', binaryRec_zero]
-- 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 ⋯)
      0 =
    zero
⊢ binaryRec' (motive := fun (x : Nat) ↦ motive x) zero bit 0 = zero
have rw₁ : zero = zero
Tactic: rw [binaryRec', binaryRec_zero]
-- 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)
⊢ binaryRec' (motive := motive) zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero
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)
    1 =
  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
⊢ binaryRec' (motive := motive) zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero
have rw₁ : (if h : Eq (α := Nat) 0 0 → true = true then bit true 0 h zero
  else
    have this := sorry;
    Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero sorry) =
  bit true 0 binaryRec'_one._proof_1 zero
Tactic: rw [binaryRec', binaryRec_one, dif_pos]