-- Mathlib/Data/Nat/Bitwise.lean
theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
    (h : n ≠ 0) :
    binaryRec z f n = bit_decomp n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n))

Proof state:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ f false 0 z = z ∨ (n = 0 → b = true)

Tactic:
right

Result:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ n = 0 → b = true

Proof state:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ ∀ (h : bit b n = bit b n), f b n (binaryRec z f n) = h ▸ f b n (binaryRec z f n)

Tactic:
simp

Result:
no goals

Proof state:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ ∀ (h : bit (bit b n).bodd (bit b n).div2 = bit b n),
    f b n (binaryRec z f n) = h ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Tactic:
rw [bodd_bit, div2_bit]

Result:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ ∀ (h : bit b n = bit b n), f b n (binaryRec z f n) = h ▸ f b n (binaryRec z f n)

Proof state:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ n = 0 → b = true

Tactic:
simpa [bit_eq_zero_iff] using h

Result:
no goals

Proof state:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec z f (bit b n) = ⋯ ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Tactic:
rw [binaryRec_eq _ _ (by right; simpa [bit_eq_zero_iff] using h)]

Result:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ f b n (binaryRec z f n) = ⋯ ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Proof state:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h✝ : bit b n ≠ 0
h : bit (bit b n).bodd (bit b n).div2 = bit b n
⊢ f b n (binaryRec z f n) = h ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Tactic:
revert h

Result:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ ∀ (h : bit (bit b n).bodd (bit b n).div2 = bit b n),
    f b n (binaryRec z f n) = h ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Proof state:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ f b n (binaryRec z f n) = ⋯ ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Tactic:
generalize_proofs h

Result:
case h
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h✝ : bit b n ≠ 0
h : bit (bit b n).bodd (bit b n).div2 = bit b n
⊢ f b n (binaryRec z f n) = h ▸ f (bit b n).bodd (bit b n).div2 (binaryRec z f (bit b n).div2)

Proof state:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ binaryRec z f n = ⋯ ▸ f n.bodd n.div2 (binaryRec z f n.div2)

Tactic:
cases n using bitCasesOn with
| h b n =>
  rw [binaryRec_eq _ _ (by right; simpa [bit_eq_zero_iff] using h)]
  generalize_proofs h; revert h
  rw [bodd_bit, div2_bit]
  simp

Result:
no goals