internlm/Lean-Github huggingface dataset:
Theorem: SizedArray.mapM_cons
Proof state before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β),
    mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons a_1 empty) = do
      let y ← mapM f x
      pure (cons a_1 y)
Tactic:
intro b
Proof state after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
⊢ mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty) = do
    let y ← mapM f x
    pure (cons b y)
Theorem: SizedArray.mapM_cons
Proof state before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
⊢ mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty) = do
    let y ← mapM f x
    pure (cons b y)
Tactic:
exact mapM.loop_cons_succ f a x (hi₁:=n.zero_lt_succ) b empty
Proof state after:
no goals
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let y ← mapM f empty
    let b ← f a
    pure (push y b)
Tactic:
rw [mapM_empty, pure_bind]
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let b ← f a
    pure (push empty b)
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let b ← f a
    pure (push empty b)
Tactic:
unfold mapM
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let b ← f a
    pure (push empty b)
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let b ← f a
    pure (push empty b)
Tactic:
unfold mapM.loop
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (if hlt : 0 < 0 + 1 then do
      let __do_lift ← f (push empty a)[0]
      mapM.loop f (push empty a) (0 + 1) hlt (push (mkEmpty (0 + 1)) __do_lift)
    else
      let_fun this := (_ : 0 = 0 + 1);
      pure (this ▸ mkEmpty (0 + 1))) =
    do
    let b ← f a
    pure (push empty b)
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (if hlt : 0 < 0 + 1 then do
      let __do_lift ← f (push empty a)[0]
      mapM.loop f (push empty a) (0 + 1) hlt (push (mkEmpty (0 + 1)) __do_lift)
    else
      let_fun this := (_ : 0 = 0 + 1);
      pure (this ▸ mkEmpty (0 + 1))) =
    do
    let b ← f a
    pure (push empty b)
Tactic:
unfold mapM.loop
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (if h : 0 < 0 + 1 then do
      let __do_lift ← f (push empty a)[0]
      if hlt : 0 + 1 < 0 + 1 then do
          let __do_lift_1 ← f (push empty a)[0 + 1]
          mapM.loop f (push empty a) (0 + 1 + 1) hlt (push (push (mkEmpty (0 + 1)) __do_lift) __do_lift_1)
        else
          let_fun this := (_ : 0 + 1 = 0 + 1);
          pure (this ▸ push (mkEmpty (0 + 1)) __do_lift)
    else
      let_fun this := (_ : 0 = 0 + 1);
      pure (this ▸ mkEmpty (0 + 1))) =
    do
    let b ← f a
    pure (push empty b)
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (if h : 0 < 0 + 1 then do
      let __do_lift ← f (push empty a)[0]
      if hlt : 0 + 1 < 0 + 1 then do
          let __do_lift_1 ← f (push empty a)[0 + 1]
          mapM.loop f (push empty a) (0 + 1 + 1) hlt (push (push (mkEmpty (0 + 1)) __do_lift) __do_lift_1)
        else
          let_fun this := (_ : 0 + 1 = 0 + 1);
          pure (this ▸ push (mkEmpty (0 + 1)) __do_lift)
    else
      let_fun this := (_ : 0 = 0 + 1);
      pure (this ▸ mkEmpty (0 + 1))) =
    do
    let b ← f a
    pure (push empty b)
Tactic:
simp only [(by decide : 0 < 0+1), (by decide : ¬ (0 + 1 < 0+1)), dif_pos, dif_neg]
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (do
      let __do_lift ← f (push empty a)[0]
      pure (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f a
    pure (push empty b)
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (do
      let __do_lift ← f (push empty a)[0]
      pure (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f a
    pure (push empty b)
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ 0 < 0 + 1
Tactic:
decide
Proof state after:
no goals
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ ¬0 + 1 < 0 + 1
Tactic:
decide
Proof state after:
no goals
Theorem: SizedArray.mapM_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (push (cons a x) a✝) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)
Tactic:
simp only [push_cons_eq_cons_push, mapM_cons, bind_assoc, IH, pure_bind]
Proof state after:
no goals
Theorem: SizedArray.mapMIdx_empty
Proof 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
Proof 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
Theorem: SizedArray.mapMIdx_empty
Proof 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
Proof 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
Theorem: SizedArray.mapMIdx_empty
Proof 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]
Proof 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
Theorem: SizedArray.mapMIdx_empty
Proof 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
Proof state after:
no goals
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop (f ∘ Fin.succ) x i hi₂ r
    pure (cons b y)
Tactic:
cases Nat.eq_or_lt_of_le hi₂ with
| inl heq =>
  cases heq; unfold loop; simp only [dif_pos]; rw [pure_bind]
| inr hlt =>
  unfold loop
  simp only [Nat.ne_of_lt hlt, Nat.ne_of_lt (Nat.succ_lt_succ hlt), dif_neg]
  rw [bind_assoc]
  apply bind_congr; intro b'
  rw [push_cons_eq_cons_push]
  exact mapMIdx.loop_cons_succ f a x (i+1) b (push r b')
Proof state after:
no goals
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
heq : i = n
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop (f ∘ Fin.succ) x i hi₂ r
    pure (cons b y)
Tactic:
cases heq
Proof state after:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ loop f (cons a x) (n + 1) hi₁ (cons b r) = do
    let y ← loop (f ∘ Fin.succ) x n hi₂ r
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ loop f (cons a x) (n + 1) hi₁ (cons b r) = do
    let y ← loop (f ∘ Fin.succ) x n hi₂ r
    pure (cons b y)
Tactic:
unfold loop
Proof state after:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if h : n + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f { val := n + 1, isLt := this } (cons a x)[n + 1]
      let r : SizedArray β (n + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (n + 1 + 1) this r) =
    do
    let y ←
      if h : n = n then pure (h ▸ r)
        else
          let_fun this := (_ : n < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := n, isLt := this } x[n]
          let r : SizedArray β (n + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (n + 1) this r
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if h : n + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f { val := n + 1, isLt := this } (cons a x)[n + 1]
      let r : SizedArray β (n + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (n + 1 + 1) this r) =
    do
    let y ←
      if h : n = n then pure (h ▸ r)
        else
          let_fun this := (_ : n < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := n, isLt := this } x[n]
          let r : SizedArray β (n + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (n + 1) this r
    pure (cons b y)
Tactic:
simp only [dif_pos]
Proof state after:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ pure (cons b r) = do
    let y ← pure r
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ pure (cons b r) = do
    let y ← pure r
    pure (cons b y)
Tactic:
rw [pure_bind]
Proof state after:
no goals
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop (f ∘ Fin.succ) x i hi₂ r
    pure (cons b y)
Tactic:
unfold loop
Proof state after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f { val := i + 1, isLt := this } (cons a x)[i + 1]
      let r : SizedArray β (i + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (i + 1 + 1) this r) =
    do
    let y ←
      if h : i = n then pure (h ▸ r)
        else
          let_fun this := (_ : i < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := this } x[i]
          let r : SizedArray β (i + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (i + 1) this r
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f { val := i + 1, isLt := this } (cons a x)[i + 1]
      let r : SizedArray β (i + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (i + 1 + 1) this r) =
    do
    let y ←
      if h : i = n then pure (h ▸ r)
        else
          let_fun this := (_ : i < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := this } x[i]
          let r : SizedArray β (i + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (i + 1) this r
    pure (cons b y)
Tactic:
simp only [Nat.ne_of_lt hlt, Nat.ne_of_lt (Nat.succ_lt_succ hlt), dif_neg]
Proof state after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
        loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r __do_lift)
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
        loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r __do_lift)
    pure (cons b y)
Tactic:
rw [bind_assoc]
Proof state after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let x_1 ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r x_1)
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let x_1 ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r x_1)
    pure (cons b y)
Tactic:
apply bind_congr
Proof state after:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ ∀ (a_1 : β),
    loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) a_1) = do
      let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r a_1)
      pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ ∀ (a_1 : β),
    loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) a_1) = do
      let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r a_1)
      pure (cons b y)
Tactic:
intro b'
Proof state after:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) b') = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) b') = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)
Tactic:
rw [push_cons_eq_cons_push]
Proof state after:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (cons b (push r b')) = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)
Theorem: SizedArray.mapMIdx.loop_cons_succ
Proof state before:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (cons b (push r b')) = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)
Tactic:
exact mapMIdx.loop_cons_succ f a x (i+1) b (push r b')
Proof state after:
no goals
Theorem: SizedArray.mapMIdx_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
⊢ mapMIdx f (cons a x) = do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ n) } a
    let y ← mapMIdx (f ∘ Fin.succ) x
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold mapMIdx; unfold mapMIdx.loop
  rw [dif_neg n.succ_ne_zero.symm]; dsimp
  rhs; ext b; change mapMIdx.loop f (cons a x) 1 n.zero_lt_succ (cons b empty)
  rw [mapMIdx.loop_cons_succ f a x 0 b empty]
Proof state after:
no goals
Theorem: SizedArray.mapMIdx_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ mapMIdx f (push empty a) = do
    let y ← mapMIdx (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
unfold mapMIdx
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ mapMIdx.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let y ← mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty 0 (_ : 0 ≤ 0) (mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Theorem: SizedArray.mapMIdx_push
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ mapMIdx.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let y ← mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty 0 (_ : 0 ≤ 0) (mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
unfold mapMIdx.loop
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (if h : 0 = 0 + 1 then pure (h ▸ mkEmpty (0 + 1))
    else
      let_fun this := (_ : 0 < 0 + 1);
      do
      let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ←
      if h : 0 = 0 then pure (h ▸ mkEmpty 0)
        else
          let_fun this := (_ : 0 < 0);
          do
          let __do_lift ←
            f { val := ↑{ val := 0, isLt := this }, isLt := (_ : ↑{ val := 0, isLt := this } < Nat.succ 0) } empty[0]
          let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
          mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty (0 + 1) this r
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)