English
Let α be nontrivial. The map sending a line to its toFun function is injective: if l.toFun = m.toFun then l = m.
Русский
Пусть α ненулевой. Отображение линии к её функции toFun инъективно: если l.toFun = m.toFun, то l = m.
LaTeX
$$$[Nontrivial\\ α] \\Rightarrow \\forall l,m : Line\\, α\\,\\iota,\\ l.toFun = m.toFun \\Rightarrow l = m.$$$
Lean4
theorem coe_injective [Nontrivial α] : Injective ((⇑) : Line α ι → α → ι → α) :=
by
rintro l m hlm
ext i a
obtain ⟨b, hba⟩ := exists_ne a
simp only [funext_iff] at hlm ⊢
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· cases hi : idxFun m i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i
· cases hi : idxFun l i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i