-- 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 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 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)
⊢ (∀ (i : Fin w),
      (Fin.hIterate (fun i => α × BitVec i) (state 0, nil) fun i q =>
                (fun p => (p.fst, cons p.snd q.snd)) (f i q.fst)).snd.getLsbD
          ↑i =
        (f i (state ↑i)).snd) ∧
    (Fin.hIterate (fun i => α × BitVec i) (state 0, nil) fun i q =>
          (fun p => (p.fst, cons p.snd q.snd)) (f i q.fst)).fst =
      state w

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

Proof state:
case inr.inl.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:
rw [← (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)
⊢ ↑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)
⊢ (∀ (i : Fin w), (iunfoldr f (state 0)).snd.getLsbD ↑i = (f i (state ↑i)).snd) ∧ (iunfoldr f (state 0)).fst = state w

Tactic:
unfold iunfoldr

Result:
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, nil) fun i q =>
                (fun p => (p.fst, cons p.snd q.snd)) (f i q.fst)).snd.getLsbD
          ↑i =
        (f i (state ↑i)).snd) ∧
    (Fin.hIterate (fun i => α × BitVec i) (state 0, nil) fun i q =>
          (fun p => (p.fst, cons p.snd q.snd)) (f i q.fst)).fst =
      state w

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:
have := Fin.pos 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
this : 0 < 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)
⊢ ∀ (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:
intro j ⟨s, v⟩ ih hj

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) ∧
    ((f j (s, v).fst).fst, cons (f j (s, v).fst).snd (s, v).snd).fst = state (↑j + 1)

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
this : 0 < 0
⊢ (state 0, 0#0).snd.getLsbD ↑i = (f ⟨↑i, ⋯⟩ (state ↑i)).snd

Tactic:
contradiction

Result:
no goals

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

Tactic:
rfl

Result:
no goals

Proof state:
case inr.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
hj3 : ↑j = 0
⊢ (f j s).snd = (f j (state ↑j)).snd

Tactic:
congr

Result:
case inr.inl.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)
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) ∧
    ((f j (s, v).fst).fst, cons (f j (s, v).fst).snd (s, v).snd).fst = state (↑j + 1)

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