internlm/Lean-Github huggingface dataset:
Theorem: Array.size_mapM'
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (do
      let x_1 ← y
      let x_2 ← f a
      let a_1 ← pure { val := push x_1.val x_2, property := (_ : size (push x_1.val x_2) = size (push x a)) }
      pure a_1.val) =
    do
    let x_1 ← y
    let y ← pure x_1.val
    let b ← f a
    pure (push y b)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ ∀ (a_1 : { a // size a = size x }),
    (do
        let x_1 ← f a
        let a_2 ← pure { val := push a_1.val x_1, property := (_ : size (push a_1.val x_1) = size (push x a)) }
        pure a_2.val) =
      do
      let y ← pure a_1.val
      let b ← f a
      pure (push y b)
Theorem: Array.size_mapM'
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ ∀ (a_1 : { a // size a = size x }),
    (do
        let x_1 ← f a
        let a_2 ← pure { val := push a_1.val x_1, property := (_ : size (push a_1.val x_1) = size (push x a)) }
        pure a_2.val) =
      do
      let y ← pure a_1.val
      let b ← f a
      pure (push y b)
Tactic:
intro y
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y✝ : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y✝ = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
y : { a // size a = size x }
⊢ (do
      let x_1 ← f a
      let a_1 ← pure { val := push y.val x_1, property := (_ : size (push y.val x_1) = size (push x a)) }
      pure a_1.val) =
    do
    let y ← pure y.val
    let b ← f a
    pure (push y b)
Theorem: Array.size_mapM'
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y✝ : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y✝ = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
y : { a // size a = size x }
⊢ (do
      let x_1 ← f a
      let a_1 ← pure { val := push y.val x_1, property := (_ : size (push y.val x_1) = size (push x a)) }
      pure a_1.val) =
    do
    let y ← pure y.val
    let b ← f a
    pure (push y b)
Tactic:
simp only [pure_bind]
Proof state after:
no goals
Theorem: Array.getElem_map'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (map f arr)[i] = f arr[i]
Tactic:
show (arr.map f).data[i] = f (arr[i]' _)
Proof state after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (map f arr).data[i] = f arr[i]
Theorem: Array.getElem_map'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (map f arr).data[i] = f arr[i]
Tactic:
rw [getElem_eq (arr.map_data' f) (Eq.refl i)]
Proof state after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (List.map f arr.data)[i] = f arr[i]
Theorem: Array.getElem_map'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (List.map f arr.data)[i] = f arr[i]
Tactic:
exact List.get_map f
Proof state after:
no goals
Theorem: Array.mapIdxM.map_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i j : Nat
h : i + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
Tactic:
induction i generalizing j y with
| zero => dsimp [map]
| succ i IH =>
  unfold map; dsimp
  apply bind_congr; intro b
  exact IH (j+1) _ (push y b)
Proof state after:
no goals
Theorem: Array.mapIdxM.map_cons
Proof state before:
case zero
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
j : Nat
h : Nat.zero + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f Nat.zero (j + 1) h y = map x (f ∘ Fin.succ) Nat.zero j (_ : Nat.zero + j = size x) y
Tactic:
dsimp [map]
Proof state after:
no goals
Theorem: Array.mapIdxM.map_cons
Proof state before:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f (Nat.succ i) (j + 1) h y = map x (f ∘ Fin.succ) (Nat.succ i) j (_ : Nat.succ i + j = size x) y
Tactic:
unfold map
Proof state after:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ (let_fun this := (_ : j + 1 < size (cons a x));
    let idx := { val := j + 1, isLt := this };
    let_fun this := (_ : i + (j + 1 + 1) = size (cons a x));
    do
    let __do_lift ← f idx (get (cons a x) idx)
    map (cons a x) f i (j + 1 + 1) this (push y __do_lift)) =
    let_fun this := (_ : j < size x);
    let idx := { val := j, isLt := this };
    let_fun this := (_ : i + (j + 1) = size x);
    do
    let __do_lift ← (f ∘ Fin.succ) idx (get x idx)
    map x (f ∘ Fin.succ) i (j + 1) this (push y __do_lift)
Theorem: Array.mapIdxM.map_cons
Proof state before:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ (let_fun this := (_ : j + 1 < size (cons a x));
    let idx := { val := j + 1, isLt := this };
    let_fun this := (_ : i + (j + 1 + 1) = size (cons a x));
    do
    let __do_lift ← f idx (get (cons a x) idx)
    map (cons a x) f i (j + 1 + 1) this (push y __do_lift)) =
    let_fun this := (_ : j < size x);
    let idx := { val := j, isLt := this };
    let_fun this := (_ : i + (j + 1) = size x);
    do
    let __do_lift ← (f ∘ Fin.succ) idx (get x idx)
    map x (f ∘ Fin.succ) i (j + 1) this (push y __do_lift)
Tactic:
dsimp
Proof state after:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ (do
      let __do_lift ← f { val := j + 1, isLt := (_ : j + 1 < Nat.succ (size x)) } x[j]
      map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y __do_lift)) =
    do
    let __do_lift ← f { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (size x)) } x[j]
    map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y __do_lift)
Theorem: Array.mapIdxM.map_cons
Proof state before:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ (do
      let __do_lift ← f { val := j + 1, isLt := (_ : j + 1 < Nat.succ (size x)) } x[j]
      map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y __do_lift)) =
    do
    let __do_lift ← f { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (size x)) } x[j]
    map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y __do_lift)
Tactic:
apply bind_congr
Proof state after:
case succ.h
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ ∀ (a_1 : β),
    map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y a_1) =
      map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y a_1)
Theorem: Array.mapIdxM.map_cons
Proof state before:
case succ.h
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ ∀ (a_1 : β),
    map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y a_1) =
      map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y a_1)
Tactic:
intro b
Proof state after:
case succ.h
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
b : β
⊢ map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y b) =
    map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y b)
Theorem: Array.mapIdxM.map_cons
Proof state before:
case succ.h
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
b : β
⊢ map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y b) =
    map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y b)
Tactic:
exact IH (j+1) _ (push y b)
Proof state after:
no goals
Theorem: Array.mapIdxM_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ mapIdxM (cons a x) f = do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM x (f ∘ Fin.succ)
    pure (cons b y)
Tactic:
unfold mapIdxM
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ mapIdxM.map (cons a x) f (size (cons a x)) 0 (_ : size (cons a x) + 0 = size (cons a x) + 0)
      (mkEmpty (size (cons a x))) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ mapIdxM.map (cons a x) f (size (cons a x)) 0 (_ : size (cons a x) + 0 = size (cons a x) + 0)
      (mkEmpty (size (cons a x))) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
conv => lhs; unfold mapIdxM.map; dsimp [cons]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ (match size { data := a :: x.data }, (_ : size { data := a :: x.data } + 0 = size { data := a :: x.data } + 0) with
    | 0, x => pure #[]
    | Nat.succ i, inv => do
      let __do_lift ← f 0 { data := a :: x.data }[0]
      mapIdxM.map { data := a :: x.data } f i (0 + 1) (_ : i + (0 + 1) = size { data := a :: x.data })
          (push #[] __do_lift)) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ (match size { data := a :: x.data }, (_ : size { data := a :: x.data } + 0 = size { data := a :: x.data } + 0) with
    | 0, x => pure #[]
    | Nat.succ i, inv => do
      let __do_lift ← f 0 { data := a :: x.data }[0]
      mapIdxM.map { data := a :: x.data } f i (0 + 1) (_ : i + (0 + 1) = size { data := a :: x.data })
          (push #[] __do_lift)) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
        (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] a_1) =
      do
      let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
      pure (cons a_1 y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
        (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] a_1) =
      do
      let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
      pure (cons a_1 y)
Tactic:
intro b
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
      (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] b) =
    do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
      (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] b) =
    do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
show mapIdxM.map (cons a x) f x.size 1 rfl #[b] = _
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map (cons a x) f (size x) 1 (_ : size x + 1 = size x + 1) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map (cons a x) f (size x) 1 (_ : size x + 1 = size x + 1) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
rw [mapIdxM.map_cons]
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
generalize f ∘ Fin.succ = f'
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
clear f
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
suffices ∀ (i j) (h : i + j = x.size) (y : Array β), mapIdxM.map x f' i j h (cons b y) = (mapIdxM.map x f' i j h y >>= λ y => pure (cons b y))
from this x.size 0 rfl #[]
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ ∀ (i j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ ∀ (i j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
Tactic:
intro i j h y
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i j : Nat
h : i + j = size x
y : Array β
⊢ mapIdxM.map x f' i j h (cons b y) = do
    let y ← mapIdxM.map x f' i j h y
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i j : Nat
h : i + j = size x
y : Array β
⊢ mapIdxM.map x f' i j h (cons b y) = do
    let y ← mapIdxM.map x f' i j h y
    pure (cons b y)
Tactic:
induction i generalizing j y with
| zero => dsimp [mapIdxM.map]; rw [pure_bind]
| succ i IH =>
  dsimp [mapIdxM.map]; simp only [bind_assoc]
  apply bind_congr; intro b'
  dsimp [push, cons, List.concat]
  exact IH ..
Proof state after:
no goals
Theorem: Array.mapIdxM_cons
Proof state before:
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ mapIdxM.map x f' Nat.zero j h (cons b y) = do
    let y ← mapIdxM.map x f' Nat.zero j h y
    pure (cons b y)
Tactic:
dsimp [mapIdxM.map]
Proof state after:
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
Tactic:
rw [pure_bind]
Proof state after:
no goals
Theorem: Array.mapIdxM_cons
Proof state before:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ mapIdxM.map x f' (Nat.succ i) j h (cons b y) = do
    let y ← mapIdxM.map x f' (Nat.succ i) j h y
    pure (cons b y)
Tactic:
dsimp [mapIdxM.map]
Proof state after:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
        mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y __do_lift)
    pure (cons b y)