-- 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 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)

Tactic:
case step =>
  intro j ⟨s, v⟩ ih hj
  apply And.intro
  case left =>
    intro i
    simp only [getLsbD_cons]
    have hj2 : j.val ≤ w := by simp
    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
  case right =>
    simp
    have hj2 : j.val ≤ w := by simp
    rw [← ind j, ← (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)
⊢ w ≤ w

Tactic:
simp

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
⊢ ↑j ≤ w

Tactic:
simp

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

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

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

Tactic:
intro i

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

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:
simp only [getLsbD_cons]

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

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

Tactic:
simp [h3, if_pos]

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

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

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)
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:
case left =>
  intro i
  simp only [getLsbD_cons]
  have hj2 : j.val ≤ w := by simp
  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:
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)
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)