ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ PointedMap.f (proj i) (ListBlank.nth L n) = ListBlank.nth L n i
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ ListBlank.nth (ListBlank.map (proj i) L) n = ListBlank.nth L n i
rw [ListBlank.nth_map]
no goals
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ PointedMap.f (proj i) (ListBlank.nth L n) = ListBlank.nth L n i
rfl