K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some S))
⊢ Option.iget (Option.map some (List.get? (List.reverse S) n)) = List.get? (List.reverse S) n
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some S))
⊢ ListBlank.nth L n k = List.get? (List.reverse S) n
rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk, List.getI_eq_iget_get?,
  List.get?_map]
no goals
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.reverse (List.map some S))
⊢ Option.iget (Option.map some (List.get? (List.reverse S) n)) = List.get? (List.reverse S) n
cases S.reverse.get? n <;> rfl