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

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ mapMIdx f empty = pure empty
Tactic:
unfold mapMIdx
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ mapMIdx.loop f empty 0 (_ : 0 ≤ 0) (mkEmpty 0) = pure empty

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ mapMIdx.loop f empty 0 (_ : 0 ≤ 0) (mkEmpty 0) = pure empty
Tactic:
unfold mapMIdx.loop
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ (if h : 0 = 0 then pure (h ▸ mkEmpty 0)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f { val := 0, isLt := this } empty[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
      mapMIdx.loop f empty (0 + 1) this r) =
    pure empty

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ (if h : 0 = 0 then pure (h ▸ mkEmpty 0)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f { val := 0, isLt := this } empty[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
      mapMIdx.loop f empty (0 + 1) this r) =
    pure empty
Tactic:
rw [dif_pos rfl]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ pure ((_ : 0 = 0) ▸ mkEmpty 0) = pure empty

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ pure ((_ : 0 = 0) ▸ mkEmpty 0) = pure empty
Tactic:
rfl
State after:
no goals