Theorem: List.mapIdx'_cons (Algdata/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ mapIdx' (a :: as) f = f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ)
Tactic:
suffices ∀ (l : List α) (b : β) (acc : Array β) (h : l.length + (acc.size + 1) = as.length + 1), mapIdx'.go (a :: as) f l ⟨b :: acc.data⟩ h = b :: mapIdx'.go as (f ∘ Fin.succ) l acc (Nat.succ.inj h)
by
  dsimp [mapIdx', mapIdx'.go, Array.push, concat]
  exact this as _ #[] _
State after:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)

State before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
Tactic:
intros l b acc h
State after:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
l : List α
b : β
acc : Array β
h : length l + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)

State before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
l : List α
b : β
acc : Array β
h : length l + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
Tactic:
induction l generalizing acc with
| nil => dsimp [mapIdx'.go]; simp only [Array.toList_eq]
| cons a' tl IH =>
  dsimp [mapIdx'.go, Array.push, concat]
  exact IH (acc.push (f _ a')) _
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
this :
  ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
⊢ mapIdx' (a :: as) f = f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ)
Tactic:
dsimp [mapIdx', mapIdx'.go, Array.push, concat]
State after:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
this :
  ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
⊢ mapIdx'.go (a :: as) f as { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] }
      (_ :
        length as +
            Array.size { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] } =
          Nat.succ (length as)) =
    f 0 a :: mapIdx'.go as (f ∘ Fin.succ) as #[] (_ : length as + Array.size #[] = length as + Array.size #[])

State before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
this :
  ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
⊢ mapIdx'.go (a :: as) f as { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] }
      (_ :
        length as +
            Array.size { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] } =
          Nat.succ (length as)) =
    f 0 a :: mapIdx'.go as (f ∘ Fin.succ) as #[] (_ : length as + Array.size #[] = length as + Array.size #[])
Tactic:
exact this as _ #[] _
State after:
no goals

State before:
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f [] { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) [] acc (_ : length [] + Array.size acc = length as)
Tactic:
dsimp [mapIdx'.go]
State after:
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ Array.toList { data := b :: acc.data } = b :: Array.toList acc

State before:
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ Array.toList { data := b :: acc.data } = b :: Array.toList acc
Tactic:
simp only [Array.toList_eq]
State after:
no goals

State before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
a' : α
tl : List α
IH :
  ∀ (acc : Array β) (h : length tl + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f tl { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) tl acc (_ : length tl + Array.size acc = length as)
acc : Array β
h : length (a' :: tl) + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f (a' :: tl) { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) (a' :: tl) acc (_ : length (a' :: tl) + Array.size acc = length as)
Tactic:
dsimp [mapIdx'.go, Array.push, concat]
State after:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
a' : α
tl : List α
IH :
  ∀ (acc : Array β) (h : length tl + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f tl { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) tl acc (_ : length tl + Array.size acc = length as)
acc : Array β
h : length (a' :: tl) + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f tl
      {
        data :=
          b ::
            concat acc.data
              (f
                { val := Array.size { data := b :: acc.data },
                  isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                a') }
      (_ :
        length tl +
            Array.size
              {
                data :=
                  b ::
                    concat acc.data
                      (f
                        { val := Array.size { data := b :: acc.data },
                          isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                        a') } =
          Nat.succ (length as)) =
    b ::
      mapIdx'.go as (f ∘ Fin.succ) tl
        {
          data :=
            concat acc.data
              (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) } a') }
        (_ :
          length tl +
              Array.size
                {
                  data :=
                    concat acc.data
                      (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) }
                        a') } =
            length as)

State before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
a' : α
tl : List α
IH :
  ∀ (acc : Array β) (h : length tl + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f tl { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) tl acc (_ : length tl + Array.size acc = length as)
acc : Array β
h : length (a' :: tl) + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f tl
      {
        data :=
          b ::
            concat acc.data
              (f
                { val := Array.size { data := b :: acc.data },
                  isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                a') }
      (_ :
        length tl +
            Array.size
              {
                data :=
                  b ::
                    concat acc.data
                      (f
                        { val := Array.size { data := b :: acc.data },
                          isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                        a') } =
          Nat.succ (length as)) =
    b ::
      mapIdx'.go as (f ∘ Fin.succ) tl
        {
          data :=
            concat acc.data
              (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) } a') }
        (_ :
          length tl +
              Array.size
                {
                  data :=
                    concat acc.data
                      (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) }
                        a') } =
            length as)
Tactic:
exact IH (acc.push (f _ a')) _
State after:
no goals