Theorem: SizedArray.foldlMIdx_empty (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
⊢ foldlMIdx f init empty = pure init
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
⊢ foldlMIdx.loop f empty 0 (_ : 0 ≤ 0) init = pure init

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
⊢ foldlMIdx.loop f empty 0 (_ : 0 ≤ 0) init = pure init
Tactic:
unfold foldlMIdx.loop
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
⊢ (if h : 0 = 0 then pure (h ▸ init)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f 0 init empty[0]
      foldlMIdx.loop f empty (0 + 1) this __do_lift) =
    pure init

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
⊢ (if h : 0 = 0 then pure (h ▸ init)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f 0 init empty[0]
      foldlMIdx.loop f empty (0 + 1) this __do_lift) =
    pure init
Tactic:
exact dif_pos rfl
State after:
no goals