Theorem: SizedArray.foldlMIdx_cons (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx f init (cons a x) = do
    let b ← f 0 init a
    foldlMIdx (fun i b => f (Nat.succ i) b) b x
Tactic:
unfold foldlMIdx
State after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx.loop f (cons a x) 0 (_ : 0 ≤ n + 1) init = do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx.loop f (cons a x) 0 (_ : 0 ≤ n + 1) init = do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Tactic:
conv => lhs; unfold foldlMIdx.loop; simp only [dif_neg n.succ_ne_zero.symm]
State after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ (do
      let __do_lift ← f 0 init (cons a x)[0]
      foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) __do_lift) =
    do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ (do
      let __do_lift ← f 0 init (cons a x)[0]
      foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) __do_lift) =
    do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Tactic:
apply bind_congr
State after:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) a_1 =
      foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) a_1

State before:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) a_1 =
      foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) a_1
Tactic:
intro b
State after:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
b : β (0 + 1)
⊢ foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) b = foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b

State before:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
b : β (0 + 1)
⊢ foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) b = foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Tactic:
exact foldlMIdx.loop_cons_succ f a x 0 _ _ b
State after:
no goals