English
A triangle is scalene iff its three sides have pairwise distinct lengths: dist01 ≠ dist02, dist01 ≠ dist12, dist02 ≠ dist12.
Русский
Треугольник скалeнен тогда и только тогда, когда три стороны попарно различны: dist01 ≠ dist02, dist01 ≠ dist12, dist02 ≠ dist12.
LaTeX
$$$\text{Scalene}(t) \iff \big( \operatorname{dist}(t.p0,t.p1) \neq \operatorname{dist}(t.p0,t.p2) \big) \land \big( \operatorname{dist}(t.p0,t.p1) \neq \operatorname{dist}(t.p1,t.p2) \big) \land \big( \operatorname{dist}(t.p0,t.p2) \neq \operatorname{dist}(t.p1,t.p2) \big)$$$
Lean4
theorem scalene_iff_dist_ne_and_dist_ne_and_dist_ne {t : Triangle R P} :
t.Scalene ↔
dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2) :=
by
refine
⟨fun h ↦
⟨h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide) (by decide),
h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide),
h.dist_ne (by decide : (0 : Fin 3) ≠ 2) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide)⟩,
fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩
intro ⟨⟨x₁, x₂⟩, hx⟩ ⟨⟨y₁, y₂⟩, hy⟩ hxy
simp only at hx hy hxy
simp only [Subtype.mk.injEq, Prod.mk.injEq]
fin_cases x₁ <;> fin_cases x₂ <;> simp +decide only at hx <;> fin_cases y₁ <;> fin_cases y₂ <;>
simp +decide only at hy <;>
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢
