English
Given bounds x1,x2 with xi < d, map(d) x1 = map(d) x2 holds if and only if x1(0) = x2(0) and map(d)(x1 ∘ Fin.succ) = map(d)(x2 ∘ Fin.succ).
Русский
При наличии ограничений x1,i < d и x2,i < d равенство map(d) x1 = map(d) x2 эквивалентно равенству x1(0) = x2(0) и равенству map(d)(x1 ∘ Fin.succ) = map(d)(x2 ∘ Fin.succ).
LaTeX
$$$ map(d) x_1 = map(d) x_2 \\iff x_1(0) = x_2(0) \\land map(d)(x_1 \\circ Fin.succ) = map(d)(x_2 \\circ Fin.succ) $$$
Lean4
theorem map_eq_iff {x₁ x₂ : Fin n.succ → ℕ} (hx₁ : ∀ i, x₁ i < d) (hx₂ : ∀ i, x₂ i < d) :
map d x₁ = map d x₂ ↔ x₁ 0 = x₂ 0 ∧ map d (x₁ ∘ Fin.succ) = map d (x₂ ∘ Fin.succ) :=
by
refine ⟨fun h => ?_, fun h => by rw [map_succ', map_succ', h.1, h.2]⟩
have : x₁ 0 = x₂ 0 := by rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
rw [map_succ, map_succ, this, add_right_inj, mul_eq_mul_right_iff] at h
exact ⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩
