English
Equality in the dependent sigma-type Σ c:Composition n, Π i: Fin c.length, Composition (c.blocksFun i) holds if and only if the corresponding block lists are equal componentwise.
Русский
Равенство в зависимом сигма-типе Σ c:Composition n, Π i: Fin c.length, Composition (c.blocksFun i) эквивалентно тому, что соответствующие списки блоков равны по компонентам.
LaTeX
$$$i=j \\iff i.1.blocks = j.1.blocks \\land i.2.blocks = j.2.blocks$$$
Lean4
/-- Rewriting equality in the dependent type `Σ (a : Composition n), Composition a.length)` in
non-dependent terms with lists, requiring that the blocks coincide. -/
theorem sigma_composition_eq_iff (i j : Σ a : Composition n, Composition a.length) :
i = j ↔ i.1.blocks = j.1.blocks ∧ i.2.blocks = j.2.blocks :=
by
refine ⟨by rintro rfl; exact ⟨rfl, rfl⟩, ?_⟩
rcases i with ⟨a, b⟩
rcases j with ⟨a', b'⟩
rintro ⟨h, h'⟩
obtain rfl : a = a' := by ext1; exact h
obtain rfl : b = b' := by ext1; exact h'
rfl
