rw [←ih]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
ih :
  List.get (List.map Prod.fst (nths xs ns))
      { val := i, isLt := (_ : i < List.length (List.map Prod.fst (nths xs ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val,
        isLt :=
          (_ : (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val < List.length (List.map Prod.fst xs)) }
⊢ List.get (List.map Prod.fst (map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := i,
        isLt :=
          (_ :
            Nat.succ i ≤ List.length (List.map Prod.fst (map (fun n => nth xs n.val (_ : n.val < length xs)) ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : Nat.succ i ≤ List.length ns) }).val,
        isLt :=
          (_ :
            (List.get ns { val := i, isLt := (_ : Nat.succ i ≤ List.length ns) }).val <
              List.length (List.map Prod.fst xs)) }
no goals