-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Folds.lean
theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
  (∀ i : Fin w, getLsbD (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
  ∧ (iunfoldr f (state 0)).fst = state w

Proof state:
case inr
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
i : Fin (↑j + 1)
hj2 : ↑j ≤ w
h3 : ↑i = ↑j
⊢ (f j s).snd = (f j (state ↑j)).snd

Tactic:
cases (Nat.eq_zero_or_pos j.val) with
| inl hj3 => congr
             rw [← (ih hj2).2]
| inr hj3 => congr
             exact (ih hj2).2

Result:
no goals

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
⊢ ∀ (i : Fin (↑j + 1)),
    ((f j (s, v).fst).fst, cons (f j (s, v).fst).snd (s, v).snd).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

Tactic:
intro i

Result:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
i : Fin (↑j + 1)
⊢ ((f j (s, v).fst).fst, cons (f j (s, v).fst).snd (s, v).snd).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
⊢ ((f j (s, v).fst).fst, cons (f j (s, v).fst).snd (s, v).snd).fst = state (↑j + 1)

Tactic:
simp

Result:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
⊢ (f j s).fst = state (↑j + 1)

Proof state:
case inr.inr
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
i : Fin (↑j + 1)
hj2 : ↑j ≤ w
h3 : ↑i = ↑j
hj3 : ↑j > 0
⊢ (f j s).snd = (f j (state ↑j)).snd

Tactic:
congr

Result:
case inr.inr.e_self.e_a
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
j : Fin w
s : α
v : BitVec ↑j
ih : ∀ (hj : ↑j ≤ w), (∀ (i : Fin ↑j), (s, v).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (s, v).fst = state ↑j
hj : ↑j + 1 ≤ w
i : Fin (↑j + 1)
hj2 : ↑j ≤ w
h3 : ↑i = ↑j
hj3 : ↑j > 0
⊢ s = state ↑j

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
hj✝ : 0 ≤ w
⊢ (∀ (i : Fin 0), (state 0, 0#0).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd) ∧ (state 0, 0#0).fst = state 0

Tactic:
apply And.intro

Result:
case left
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
hj✝ : 0 ≤ w
⊢ ∀ (i : Fin 0), (state 0, 0#0).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

case right
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
hj✝ : 0 ≤ w
⊢ (state 0, 0#0).fst = state 0