English
Two holors are equal if and only if all their slices are equal.
Русский
Два Holor равны тогда и только тогда, когда равны все их срезы.
LaTeX
$$$\forall x,y : Holor\, \alpha\, (d::ds),\ slice\ x = slice\ y \Rightarrow x = y$$$
Lean4
/-- Two holors are equal if all their slices are equal. -/
theorem slice_eq (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) (h : slice x = slice y) : x = y :=
funext fun t : HolorIndex (d :: ds) =>
holor_index_cons_decomp (fun t => x t = y t) t fun i is hiis =>
have hiisdds : Forall₂ (· < ·) (i :: is) (d :: ds) := by rw [← hiis]; exact t.2
have hid : i < d := (forall₂_cons.1 hiisdds).1
have hisds : Forall₂ (· < ·) is ds := (forall₂_cons.1 hiisdds).2
calc
x ⟨i :: is, _⟩ = slice x i hid ⟨is, hisds⟩ := congr_arg x (Subtype.eq rfl)
_ = slice y i hid ⟨is, hisds⟩ := by rw [h]
_ = y ⟨i :: is, _⟩ := congr_arg y (Subtype.eq rfl)
