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

State before:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ foldlM f init x = foldlMIdx (fun x => f) init x
Tactic:
unfold foldlM
State after:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ Array.foldlM f init x.val 0 (Array.size x.val) = foldlMIdx (fun x => f) init x

State before:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ Array.foldlM f init x.val 0 (Array.size x.val) = foldlMIdx (fun x => f) init x
Tactic:
rw [Array.foldlM_eq_foldlM_data']
State after:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x

State before:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
Tactic:
induction x using cons_induction generalizing init with
| empty => rfl
| cons a x IH =>
  conv => lhs; dsimp [cons]
  rw [foldlMIdx_cons]
  apply bind_congr; intro b
  exact IH b
State after:
no goals

State before:
case empty
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
⊢ List.foldlM f init empty.val.data = foldlMIdx (fun x => f) init empty
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ List.foldlM f init (cons a x).val.data = foldlMIdx (fun x => f) init (cons a x)
Tactic:
conv => lhs; dsimp [cons]
State after:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    foldlMIdx (fun x => f) init (cons a x)

State before:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    foldlMIdx (fun x => f) init (cons a x)
Tactic:
rw [foldlMIdx_cons]
State after:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    do
    let b ← f init a
    foldlMIdx (fun i b => f b) b x

State before:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    do
    let b ← f init a
    foldlMIdx (fun i b => f b) b x
Tactic:
apply bind_congr
State after:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ ∀ (a : β), List.foldlM f a x.val.data = foldlMIdx (fun i b => f b) a x

State before:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ ∀ (a : β), List.foldlM f a x.val.data = foldlMIdx (fun i b => f b) a x
Tactic:
intro b
State after:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init b : β
⊢ List.foldlM f b x.val.data = foldlMIdx (fun i b => f b) b x

State before:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init b : β
⊢ List.foldlM f b x.val.data = foldlMIdx (fun i b => f b) b x
Tactic:
exact IH b
State after:
no goals