Theorem: Schema.get_map_nths_eq_get_get (Table/SchemaFunctions.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get (List.map Prod.fst (nths xs (n :: ns)))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [nths, map, get]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
rw [nth_eq_get]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) } ::
          map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) } ::
          map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [List.get]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) }).fst =
    List.get (List.map Prod.fst xs) { val := n.val, isLt := (_ : n.val < List.length (List.map Prod.fst xs)) }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) }).fst =
    List.get (List.map Prod.fst xs) { val := n.val, isLt := (_ : n.val < List.length (List.map Prod.fst xs)) }
Tactic:
rw [List.get_map Prod.fst]
State after:
no goals

State before:
η : 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)
⊢ List.get (List.map Prod.fst (nths xs (n :: ns)))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [nths, map, get]
State after:
η : 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)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }

State before:
η : 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)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
have ih := get_map_nths_eq_get_get xs ns i (Nat.lt_of_succ_lt_succ hi)
State after:
η : 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
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }

State before:
η : 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
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [List.get]
State after:
η : 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)) }

State before:
η : 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)) }
Tactic:
rw [←ih]
State after:
no goals