English
Uncurrying a nested single yields a single at the pair: sigmaUncurry (single i (single j x)) = single ⟨i,j⟩ x.
Русский
Развёртывание вложенного одинарного элемента даёт единичный элемент на паре: sigmaUncurry (single i (single j x)) = single ⟨i,j⟩ x.
LaTeX
$$$\sigma\text{-Uncurry}(\text{single } i (\text{single } j x)) = \text{single } \langle i,j\rangle x$$$
Lean4
@[simp]
theorem sigmaUncurry_single [∀ i j, Zero (δ i j)] [∀ i, DecidableEq (α i)] (i) (j : α i) (x : δ i j) :
sigmaUncurry (single i (single j x : Π₀ j : α i, δ i j)) = single ⟨i, j⟩ (by exact x) :=
by
ext ⟨i', j'⟩
dsimp only
rw [sigmaUncurry_apply]
obtain rfl | hi := eq_or_ne i i'
· rw [single_eq_same]
obtain rfl | hj := eq_or_ne j' j
· rw [single_eq_same, single_eq_same]
· rw [single_eq_of_ne hj, single_eq_of_ne]
simpa using hj
· simp [hi]
