Theorem: List.Index.val_unsigma (Extra/Index/Sigma.lean)

State before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
k : (xs.sigma f).Index
⊢ ⟨k.unsigma.fst.val, k.unsigma.snd.val⟩ = k.val
Tactic:
rw [←sigma_unsigma k, val_sigma, unsigma_sigma]
State after:
no goals