-- 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)
case₅ case₆ 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)
⊢ 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 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: 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