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

Proof state:
case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ ∀ (k : Fin w) (s : α × BitVec ↑k),
    s.fst = state ↑k → ((fun p => (p.fst, cons p.snd s.snd)) (f k s.fst)).fst = state (↑k + 1)

Tactic:
case step =>
  intro i ⟨s, v⟩ p
  simp_all [ind i]

Result:
no goals

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ ∀ (k : Fin w) (s : α × BitVec ↑k),
    s.fst = state ↑k → ((fun p => (p.fst, cons p.snd s.snd)) (f k s.fst)).fst = state (↑k + 1)

Tactic:
intro i ⟨s, v⟩ p

Result:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s✝ : α
init : s✝ = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
i : Fin w
s : α
v : BitVec ↑i
p : (s, v).fst = state ↑i
⊢ ((fun p => (p.fst, cons p.snd (s, v).snd)) (f i (s, v).fst)).fst = state (↑i + 1)

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s✝ : α
init : s✝ = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
i : Fin w
s : α
v : BitVec ↑i
p : (s, v).fst = state ↑i
⊢ ((fun p => (p.fst, cons p.snd (s, v).snd)) (f i (s, v).fst)).fst = state (↑i + 1)

Tactic:
simp_all [ind i]

Result:
no goals

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (Fin.hIterate (fun i => α × BitVec i) (s, nil) fun i q => (fun p => (p.fst, cons p.snd q.snd)) (f i q.fst)).fst =
    state w

Tactic:
apply Fin.hIterate_elim (fun i (p : α × BitVec i) => p.fst = state i)

Result:
case init
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (s, nil).fst = state 0

case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ ∀ (k : Fin w) (s : α × BitVec ↑k),
    s.fst = state ↑k → ((fun p => (p.fst, cons p.snd s.snd)) (f k s.fst)).fst = state (↑k + 1)

Proof state:
case init
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (s, nil).fst = state 0

case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ ∀ (k : Fin w) (s : α × BitVec ↑k),
    s.fst = state ↑k → ((fun p => (p.fst, cons p.snd s.snd)) (f k s.fst)).fst = state (↑k + 1)

Tactic:
case init =>
  exact init

Result:
case step
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ ∀ (k : Fin w) (s : α × BitVec ↑k),
    s.fst = state ↑k → ((fun p => (p.fst, cons p.snd s.snd)) (f k s.fst)).fst = state (↑k + 1)

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (s, nil).fst = state 0

Tactic:
exact init

Result:
no goals

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (iunfoldr f s).fst = state w

Tactic:
unfold iunfoldr

Result:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
s : α
init : s = state 0
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (Fin.hIterate (fun i => α × BitVec i) (s, nil) fun i q => (fun p => (p.fst, cons p.snd q.snd)) (f i q.fst)).fst =
    state w