-- Mathlib/Data/Nat/BinaryRec.lean
theorem binaryRec_eq {z : motive 0} {f : ∀ b n, motive n → motive (bit b n)}
    (b n) (h : f false 0 z = z ∨ (n = 0 → b = true)) :
    binaryRec z f (bit b n) = f b n (binaryRec z f n)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)),
    e ▸ f ((bit b n).testBit 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1)) = f b n (binaryRec z f n)

Tactic:
rw [testBit_bit_zero, bit_shiftRight_one]

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ f b n (binaryRec z f n) = f b n (binaryRec z f n)

Proof state:
case neg
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

Tactic:
case neg =>
  rw [binaryRec, dif_neg h']
  change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ f _ _ _ = _
  generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
  rw [testBit_bit_zero, bit_shiftRight_one]
  intros; rfl

Result:
no goals

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

Tactic:
by_cases h' : bit b n = 0

Result:
case pos
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

case neg
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

Proof state:
case intro
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
h' : bit false 0 = 0
h : f false 0 z = z
⊢ binaryRec z f (bit false 0) = f false 0 (binaryRec z f 0)

Tactic:
unfold binaryRec

Result:
case intro
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
h' : bit false 0 = 0
h : f false 0 z = z
⊢ (if n0 : bit false 0 = 0 then ⋯ ▸ z
    else
      let x := f (1 &&& bit false 0 != 0) (bit false 0 >>> 1) (binaryRec z f (bit false 0 >>> 1));
      ⋯ ▸ x) =
    f false 0
      (if n0 : 0 = 0 then ⋯ ▸ z
      else
        let x := f (1 &&& 0 != 0) (0 >>> 1) (binaryRec z f (0 >>> 1));
        ⋯ ▸ x)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

Tactic:
obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'

Result:
case intro
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
h : f false 0 z = z ∨ (0 = 0 → false = true)
h' : bit false 0 = 0
⊢ binaryRec z f (bit false 0) = f false 0 (binaryRec z f 0)

Proof state:
case pos
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

case neg
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f 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

Result:
case neg
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

Proof state:
case intro
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
h : f false 0 z = z ∨ (0 = 0 → false = true)
h' : bit false 0 = 0
⊢ binaryRec z f (bit false 0) = f false 0 (binaryRec z f 0)

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

Result:
case intro
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
h' : bit false 0 = 0
h : f false 0 z = z
⊢ binaryRec z f (bit false 0) = f false 0 (binaryRec z f 0)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ (let x := f (1 &&& bit b n != 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1));
    ⋯ ▸ x) =
    f b n (binaryRec z f n)

Tactic:
change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ f _ _ _ = _

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ⋯ ▸ f ((bit b n).testBit 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1)) = f b n (binaryRec z f n)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ f b n (binaryRec z f n) = f b n (binaryRec z f n)

Tactic:
rfl

Result:
no goals

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ f ((bit b n).testBit 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1)) = f b n (binaryRec z f n)

Tactic:
revert e

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)),
    e ▸ f ((bit b n).testBit 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1)) = f b n (binaryRec z f n)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)

Tactic:
rw [binaryRec, dif_neg h']

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ (let x := f (1 &&& bit b n != 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1));
    ⋯ ▸ x) =
    f b n (binaryRec z f n)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ f b n (binaryRec z f n) = f b n (binaryRec z f n)

Tactic:
intros

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ f b n (binaryRec z f n) = f b n (binaryRec z f n)