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

State before:
α : Type u
β : Type v
γ : Type w
as : List α
f : Fin (length as) → α → β
i : Nat
hi : i < length (mapIdx' as f)
⊢ (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
Tactic:
induction as generalizing i with
| nil => cases hi
| cons a as IH =>
  simp only [mapIdx'_cons]
  cases i with
  | zero => rfl
  | succ i => simp only [cons_getElem_succ, IH]; rfl
State after:
no goals

State before:
case nil
α : Type u
β : Type v
γ : Type w
f : Fin (length []) → α → β
i : Nat
hi : i < length (mapIdx' [] f)
⊢ (mapIdx' [] f)[i] = f { val := i, isLt := (_ : i < length []) } [][i]
Tactic:
cases hi
State after:
no goals

State before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (mapIdx' (a :: as) f)[i] = f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]
Tactic:
simp only [mapIdx'_cons]
State after:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[i] =
    f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]

State before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[i] =
    f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]
Tactic:
cases i with
| zero => rfl
| succ i => simp only [cons_getElem_succ, IH]; rfl
State after:
no goals

State before:
case cons.zero
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
hi : Nat.zero < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[Nat.zero] =
    f { val := Nat.zero, isLt := (_ : Nat.zero < length (a :: as)) } (a :: as)[Nat.zero]
Tactic:
rfl
State after:
no goals

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : Nat.succ i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[Nat.succ i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < length (a :: as)) } (a :: as)[Nat.succ i]
Tactic:
simp only [cons_getElem_succ, IH]
State after:
case cons.succ
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : Nat.succ i < length (mapIdx' (a :: as) f)
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < length as) } as[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < length (a :: as)) } as[i]

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : Nat.succ i < length (mapIdx' (a :: as) f)
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < length as) } as[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < length (a :: as)) } as[i]
Tactic:
rfl
State after:
no goals