English
Same as above, with a standard simplification form for the single-case under sigma-curry.
Русский
То же самое в стандартной форме упрощения для случая с одним элементом по σ-куррированию.
LaTeX
$$$\sigma\text{-Curry}(\text{single } (i,j) x) = \text{single } i (\text{single } j x)$$$
Lean4
@[simp]
theorem sigmaCurry_single [∀ i, DecidableEq (α i)] [∀ i j, Zero (δ i j)] (ij : Σ i, α i) (x : δ ij.1 ij.2) :
sigmaCurry (single ij x) = single ij.1 (single ij.2 x : Π₀ j, δ ij.1 j) :=
by
obtain ⟨i, j⟩ := ij
ext i' j'
dsimp only
rw [sigmaCurry_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, single_eq_of_ne hj]
simpa using hj
· simp [hi]
