English
Equality of sigma-type elements is determined by equality of their first components and equality of the second components after transporting along Fin.cast.
Русский
Согласование элементов пары сумма-типов определяется равенством их первых компонентов и равенством вторых после переноса через Fin.cast.
LaTeX
$$$\\forall {\\alpha}, \\forall a,b : (i : \\mathbb{N}) \\times (\\mathrm{Fin} i \\to \\alpha),\\ a.fst = b.fst \\rightarrow a.snd = b.snd \\circ \\mathrm{Fin.cast} (h) \\rightarrow a = b$$$
Lean4
/-- To show two sigma pairs of tuples agree, it to show the second elements are related via
`Fin.cast`. -/
theorem sigma_eq_of_eq_comp_cast {α : Type*} :
∀ {a b : Σ ii, Fin ii → α} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b
| ⟨ai, a⟩, ⟨bi, b⟩, hi, h => by
dsimp only at hi
subst hi
simpa using h
