English
Same idea as injectivity of snoc under weaker assumptions.
Русский
Та же идея инъективности snoc под слабее допущения.
LaTeX
$$$\\\\text{snoc}_{x}(x_0) \\text{ injective} \\Leftrightarrow \\text{Injective}(snoc x x_0)$$$
Lean4
theorem snoc_injective_of_injective {α} {x₀ : α} {x : Fin n → α} (hx : Function.Injective x) (hx₀ : x₀ ∉ Set.range x) :
Function.Injective (snoc x x₀ : Fin n.succ → α) := fun i j h ↦ by
induction i using lastCases with
| cast i =>
induction j using lastCases with
| cast j => simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
| last =>
simp only [snoc_castSucc, snoc_last] at h
rw [← h] at hx₀
apply hx₀.elim (Set.mem_range_self i)
| last =>
induction j using lastCases with
| cast j =>
simp only [snoc_castSucc, snoc_last] at h
rw [h] at hx₀
apply hx₀.elim (Set.mem_range_self j)
| last => simp
