English
If cmp(o1, o2) = Ordering.eq, then o1 = o2.
Русский
Если сравнение cmp(o1, o2) равно Ordering.eq, то o1 = o2.
LaTeX
$$$\mathrm{cmp}(o_1,o_2) = \mathrm{Ordering.eq} \Rightarrow o_1 = o_2$$$
Lean4
theorem eq_of_cmp_eq : ∀ {o₁ o₂}, cmp o₁ o₂ = Ordering.eq → o₁ = o₂
| 0, 0, _ => rfl
| oadd e n a, 0, h => by injection h
| 0, oadd e n a, h => by injection h
| oadd e₁ n₁ a₁, oadd e₂ n₂ a₂, h => by
revert h; simp only [cmp]
cases h₁ : cmp e₁ e₂ <;> intro h <;> try cases h
obtain rfl := eq_of_cmp_eq h₁
revert h; cases h₂ : _root_.cmp (n₁ : ℕ) n₂ <;> intro h <;> try cases h
obtain rfl := eq_of_cmp_eq h
rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂
obtain rfl := Subtype.eq h₂
simp
