internlm/Lean-Github huggingface dataset:
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 β
⊢ (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)
Tactic:
rw [dif_neg (c:=0=0+1) (by decide), dif_pos rfl]
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 β
⊢ (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 ← pure ((_ : 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 β
⊢ (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 ← pure ((_ : 0 = 0) ▸ mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
dsimp
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 β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let y ← pure (mkEmpty 0)
    let b ← f 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 β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let y ← pure (mkEmpty 0)
    let b ← f 0 a
    pure (push y b)
Tactic:
rw [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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f 0 a
    pure (push (mkEmpty 0) 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 β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f 0 a
    pure (push (mkEmpty 0) b)
Tactic:
apply bind_congr
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) a_1) = pure (push (mkEmpty 0) a_1)
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) a_1) = pure (push (mkEmpty 0) a_1)
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)
Tactic:
unfold mapMIdx.loop
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ (if h : 0 + 1 = 0 + 1 then pure (h ▸ push (mkEmpty (0 + 1)) b)
    else
      let_fun this := (_ : 0 + 1 < 0 + 1);
      do
      let __do_lift ← f { val := 0 + 1, isLt := this } (push empty a)[0 + 1]
      let r : SizedArray β (0 + 1 + 1) := push (push (mkEmpty (0 + 1)) b) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1 + 1) this r) =
    pure (push (mkEmpty 0) b)
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ (if h : 0 + 1 = 0 + 1 then pure (h ▸ push (mkEmpty (0 + 1)) b)
    else
      let_fun this := (_ : 0 + 1 < 0 + 1);
      do
      let __do_lift ← f { val := 0 + 1, isLt := this } (push empty a)[0 + 1]
      let r : SizedArray β (0 + 1 + 1) := push (push (mkEmpty (0 + 1)) b) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1 + 1) this r) =
    pure (push (mkEmpty 0) b)
Tactic:
rw [dif_pos rfl]
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ pure ((_ : 0 + 1 = 0 + 1) ▸ push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ pure ((_ : 0 + 1 = 0 + 1) ▸ push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)
Tactic:
rfl
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 β
⊢ ¬0 = 0 + 1
Tactic:
decide
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✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ mapMIdx f (push (cons a x) a✝) = do
    let y ← mapMIdx (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) (cons a x)
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (push y b)
Tactic:
simp only [push_cons_eq_cons_push, mapMIdx_cons, bind_assoc, 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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ (do
      let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (n✝ + 1)) } a
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f { val := 0, isLt := (_ : ↑{ val := 0, isLt := (_ : 0 < Nat.succ n✝) } < Nat.succ (n✝ + 1)) } a
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons x_1 (push x 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✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ (do
      let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (n✝ + 1)) } a
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f { val := 0, isLt := (_ : ↑{ val := 0, isLt := (_ : 0 < Nat.succ n✝) } < Nat.succ (n✝ + 1)) } a
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons x_1 (push x b))
Tactic:
apply bind_congr
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ ∀ (a : β),
    (do
        let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
      let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
      pure (cons a (push x b))
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ ∀ (a : β),
    (do
        let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
      let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
      pure (cons a (push x b))
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Tactic:
rw [IH]
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ←
        do
          let y ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
          let b ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ←
        do
          let y ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
          let b ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Tactic:
simp only [bind_assoc, pure_bind]
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let x ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let x_1 ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Theorem: SizedArray.mapMIdx_push
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✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let x ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let x_1 ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.mapM_eq_mapMIdx
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
n✝ : Nat
a : α
x : SizedArray α n✝
IH : mapM f x = mapMIdx (fun x => f) x
⊢ mapM f (cons a x) = mapMIdx (fun x => f) (cons a x)
Tactic:
rw [mapM_cons, mapMIdx_cons, IH]
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
n✝ : Nat
a : α
x : SizedArray α n✝
IH : mapM f x = mapMIdx (fun x => f) x
⊢ (do
      let b ← f a
      let y ← mapMIdx (fun x => f) x
      pure (cons b y)) =
    do
    let b ← f a
    let y ← mapMIdx ((fun x => f) ∘ Fin.succ) x
    pure (cons b y)
Theorem: SizedArray.mapM_eq_mapMIdx
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
n✝ : Nat
a : α
x : SizedArray α n✝
IH : mapM f x = mapMIdx (fun x => f) x
⊢ (do
      let b ← f a
      let y ← mapMIdx (fun x => f) x
      pure (cons b y)) =
    do
    let b ← f a
    let y ← mapMIdx ((fun x => f) ∘ Fin.succ) x
    pure (cons b y)
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.map_id
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ map id (push x a) = push x a
Tactic:
rw [map_push, IH]
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ push x (id a) = push x a
Theorem: SizedArray.map_id
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ push x (id a) = push x a
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.comp_map
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
g : β → γ
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map (g ∘ f) x = map g (map f x)
⊢ map (g ∘ f) (push x a) = map g (map f (push x a))
Tactic:
simp only [map_push, IH]
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
g : β → γ
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map (g ∘ f) x = map g (map f x)
⊢ push (map g (map f x)) ((g ∘ f) a) = push (map g (map f x)) (g (f a))
Theorem: SizedArray.comp_map
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
g : β → γ
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map (g ∘ f) x = map g (map f x)
⊢ push (map g (map f x)) ((g ∘ f) a) = push (map g (map f x)) (g (f a))
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.map_eq_mapM
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ map f (push x a) = mapM f (push x a)
Tactic:
rw [map_push, mapM_push, IH]
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ push (mapM f x) (f a) = do
    let y ← mapM f x
    let b ← f a
    pure (push y b)
Theorem: SizedArray.map_eq_mapM
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ push (mapM f x) (f a) = do
    let y ← mapM f x
    let b ← f a
    pure (push y b)
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.get_mapIdx
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : Fin n → α → β
x : SizedArray α n
i : Nat
hi : i < n
⊢ (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
Tactic:
induction x using cons_induction generalizing i with
| empty => cases hi
| cons a x IH =>
  simp only [mapIdx_cons]
  cases i with
  | zero => simp only [Nat.zero_eq, get_cons_zero]
  | succ i =>
    simp only [Nat.zero_eq, Nat.succ_eq_add_one]
    rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
    rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
    exact IH ..
Proof state after:
no goals
Theorem: SizedArray.get_mapIdx
Proof state before:
case empty
α : Type u
β : Type v
γ : Type w
n : Nat
f : Fin 0 → α → β
i : Nat
hi : i < 0
⊢ (mapIdx f empty)[i] = f { val := i, isLt := hi } empty[i]
Tactic:
cases hi
Proof state after:
no goals
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : i < n✝ + 1
⊢ (mapIdx f (cons a x))[i] = f { val := i, isLt := hi } (cons a x)[i]
Tactic:
simp only [mapIdx_cons]
Proof state after:
case cons
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i] =
    f { val := i, isLt := hi } (cons a x)[i]
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i] =
    f { val := i, isLt := hi } (cons a x)[i]
Tactic:
cases i with
| zero => simp only [Nat.zero_eq, get_cons_zero]
| succ i =>
  simp only [Nat.zero_eq, Nat.succ_eq_add_one]
  rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
  rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
  exact IH ..
Proof state after:
no goals
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons.zero
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
hi : Nat.zero < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[Nat.zero] =
    f { val := Nat.zero, isLt := hi } (cons a x)[Nat.zero]
Tactic:
simp only [Nat.zero_eq, get_cons_zero]
Proof state after:
no goals