awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n0 : ¬Eq (α := Nat) 0 0
⊢ (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
    else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
    if Eq (α := Nat) 0 0 then 0 else (log2 0).succ

Tactic:
(n0 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n0 : ¬Eq (α := Nat) 0 0
⊢ (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
    else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
    if Eq (α := Nat) 0 0 then 0 else (log2 0).succ

Tactic:
exact (n0 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
n0 : ¬n + 1 = 0
succ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
succ₁ :
  ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
      if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
    if n + 1 = 0 then 0 else (n + 1).log2.succ

Tactic:
obtain _ | n := n
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0
⊢ (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
    if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ

Tactic:
simp
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ Ne (α := Nat) 2 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 ≠ 0

Tactic:
have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
n0 : ¬n + 1 + 1 = 0
this : HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 ≠ 0
⊢ (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _

Premises used: Nat.lt_succ_self, Nat.log2_eq_succ_log2_shiftRight, if_neg
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
zero₁ :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ₁ succ₂ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
succ₃ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
succ₄ :
  ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
      if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
succ₅ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
succ₆ succ₇ :
  ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
      if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
succ₈ :
  ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0) (this : HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 ≠ 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
      if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ

Tactic:
decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _

Premises used: False.elim, Nat.lt_succ_self, if_neg
-- 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
ih : motive n
h : ¬(n = 0 → b = true)
rw : n = 0 ∧ b = false
⊢ Nat.bit b n = 0

Tactic:
rw [bit_eq_zero_iff]

Premises used: Nat.bit_eq_zero_iff
-- 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
ih : motive n
h : ¬(n = 0 → b = true)
zero₁ : ∀ (ih : motive 0) (h : ¬(Eq (α := Nat) 0 0 → b = true)), Eq (α := Nat) 0 0 ∧ b = false
succ : ∀ (n : Nat) (ih : motive (n + 1)) (h : ¬(n + 1 = 0 → b = true)), n + 1 = 0 ∧ b = false
⊢ n = 0 ∧ b = false

Tactic:
cases n
-- 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
ih : motive 0
h : ¬(Eq (α := Nat) 0 0 → b = true)
zero₁ : ∀ (h : ¬(Eq (α := Nat) 0 0 → false = true)), Eq (α := Nat) 0 0 ∧ false = false
zero₂ : ∀ (h : ¬(Eq (α := Nat) 0 0 → true = true)), Eq (α := Nat) 0 0 ∧ true = false
⊢ Eq (α := Nat) 0 0 ∧ b = false

Tactic:
cases b
-- 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
ih : motive (n + 1)
h : ¬(n + 1 = 0 → b = true)
succ : ∀ (h : ¬(n + 1 = 0 → false = true)), n + 1 = 0 ∧ false = false
succ₁ : ∀ (h : ¬(n + 1 = 0 → true = true)), n + 1 = 0 ∧ true = false
⊢ n + 1 = 0 ∧ b = false

Tactic:
cases b
-- 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)
ih : motive 0
h : ¬(Eq (α := Nat) 0 0 → false = true)
⊢ Eq (α := Nat) 0 0 ∧ false = false

Tactic:
simp at h ⊢
-- 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)
ih : motive 0
h : ¬(Eq (α := Nat) 0 0 → true = true)
⊢ Eq (α := Nat) 0 0 ∧ true = false

Tactic:
simp at h ⊢
-- 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)
n : Nat
ih : motive (n + 1)
h : ¬(n + 1 = 0 → false = true)
⊢ n + 1 = 0 ∧ false = false

Tactic:
simp at h ⊢
-- 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)
n : Nat
ih : motive (n + 1)
h : ¬(n + 1 = 0 → true = true)
⊢ n + 1 = 0 ∧ true = false

Tactic:
simp at 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 → b = true
ih : motive n
h' : n = 0
rw : Nat.bit b 0 = Nat.bit true 0
rw₁ rw₂ : Nat.bit true 0 = Nat.bit true 0
⊢ Nat.bit b n = Nat.bit true 0

Tactic:
rw [h', h h']
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
false : bit Bool.false n = 2 * n + Bool.false.toNat
true : bit Bool.true n = 2 * n + Bool.true.toNat
⊢ bit b n = 2 * n + b.toNat

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit false n = 2 * n + false.toNat

Tactic:
rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit true n = 2 * n + true.toNat

Tactic:
rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
rw : b.toNat < 2
H : LT.lt (α := Nat) 0 2
⊢ bit b n / 2 = n

Tactic:
rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]

Premises used: Nat.bit_val, Nat.div_eq_of_lt, Nat.add_mul_div_left, Nat.zero_add, Nat.add_comm
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
false : Bool.false.toNat < 2
true : Bool.true.toNat < 2
⊢ b.toNat < 2

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ false.toNat < 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ true.toNat < 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
⊢ LT.lt (α := Nat) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
false : bit Bool.false n % 2 = Bool.false.toNat
true : bit Bool.true n % 2 = Bool.true.toNat
⊢ bit b n % 2 = b.toNat

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit false n % 2 = false.toNat

Tactic:
simp [bit_val]

Premises used: Nat.bit_val
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit true n % 2 = true.toNat

Tactic:
simp [bit_val]

Premises used: Nat.bit_val
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
⊢ HShiftRight.hShiftRight (β := Nat) (bit b n) 1 = n

Tactic:
bit_div_two b n

Premises used: Nat.shiftRight, Nat.bit_div_two
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
⊢ (bit b n).testBit 0 = b

Tactic:
simp
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
change :
  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)) ⋯ =
    h b n
⊢ bitCasesOn (motive := motive) (bit b n) h = h b n

Tactic:
change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
generalize :
  ∀ (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
⊢ 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)) ⋯ =
    h b n

Tactic:
generalize congrArg motive (bit b n).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
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)
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
⊢ 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
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
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
⊢ ∀ (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:
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
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
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:
rfl
-- 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)
⊢ binaryRec (motive := fun (x : Nat) ↦ motive x) zero bit 0 = zero

Tactic:
rfl

Premises used: WellFounded.Nat.fix, dite, WellFounded.Nat.fix.go, Nat.binaryRec, rfl
-- 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)
⊢ binaryRec (motive := motive) zero bit 1 = bit true 0 zero

Tactic:
rfl

Premises used: cond, Nat.bit, WellFounded.Nat.fix, dite, WellFounded.Nat.fix.go, Nat.binaryRec, rfl
-- 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)
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)
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)

Tactic:
by_cases h' : n.bit b = 0

Premises used: Nat.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
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))
⊢ 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:
obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'

Premises used: Nat.bit_eq_zero_iff, Iff.mp, rfl
-- 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)
h : bit false 0 zero = zero ∨ (Eq (α := Nat) 0 0 → false = true)
h' : Nat.bit false 0 = 0
⊢ bit false 0 zero = zero

Tactic:
simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h

Premises used: imp_false, Bool.false_eq_true, not_true_eq_false, or_false
-- 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)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
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 ⋯
    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 ⋯)
    (bit false 0
      (if n0 : Eq (α := Nat) 0 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯
      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 ⋯))
⊢ 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:
unfold binaryRec
-- 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)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ 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 ⋯
    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 ⋯)
    (bit false 0
      (if n0 : Eq (α := Nat) 0 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯
      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 ⋯))

Tactic:
h.symm

Premises used: cond, Nat.bit, dite, Eq.symm
-- 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)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ 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 ⋯
    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 ⋯)
    (bit false 0
      (if n0 : Eq (α := Nat) 0 0 then Eq.rec (motive := fun (x : Sort u) (h : motive 0 = x) ↦ x) zero ⋯
      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 ⋯))

Tactic:
exact h.symm

Premises used: Eq.symm
-- 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
⊢ 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:
case pos =>
    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
    simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h
    unfold binaryRec
    exact h.symm

Premises used: Nat.bit_eq_zero_iff, imp_false, Bool.false_eq_true, not_true_eq_false, Or.symm, Iff.mp, or_false, rfl
-- 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 :
  (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)

Tactic:
rw [binaryRec, dif_neg h']

Premises used: dif_neg