-- 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:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (∀ (i : Fin w),
      (Fin.hIterate (fun i => α × BitVec i) (state 0, 0#0) fun i q =>
                ((f i q.fst).fst, cons (f i q.fst).snd q.snd)).snd.getLsbD
          ↑i =
        (f i (state ↑i)).snd) ∧
    (Fin.hIterate (fun i => α × BitVec i) (state 0, 0#0) fun i q => ((f i q.fst).fst, cons (f i q.fst).snd q.snd)).fst =
      state w

Tactic:
apply Fin.hIterate_elim
      (fun j (p : α × BitVec j) => (hj : j ≤ w) →
       (∀ i : Fin j,  getLsbD p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
        ∧ p.fst = state j)

Result:
case init
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

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

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

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).fst = state (↑j + 1)

Tactic:
have hj2 : j.val ≤ w := by 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
hj2 : ↑j ≤ w
⊢ (f j s).fst = state (↑j + 1)

Proof state:
case inl
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
⊢ v.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

Tactic:
exact (ih hj2).1 ⟨i.val, h3⟩

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)
⊢ ∀ (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:
intro

Result:
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

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
hj2 : ↑j ≤ w
⊢ (f j s).fst = state (↑j + 1)

Tactic:
rw [← ind j, ← (ih hj2).2]

Result:
no goals

Proof state:
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

Tactic:
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)
hj2 : ↑j ≤ w
⊢ (if ↑i = ↑j then (f j s).snd else v.getLsbD ↑i) = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

Tactic:
cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
| inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
            exact (ih hj2).1 ⟨i.val, h3⟩
| inr h3 => simp [h3, if_pos]
            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:
case init
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

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

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

Tactic:
case hj => simp

Result:
case init
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

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

Proof state:
case inl
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
⊢ (if ↑i = ↑j then (f j s).snd else v.getLsbD ↑i) = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

Tactic:
simp [if_neg, (Nat.ne_of_lt h3)]

Result:
case inl
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
⊢ v.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd