English
There exist two indices i and j such that for every k, the self-pairing B(α_k, α_k) equals either B(α_i, α_i) or B(α_j, α_j). In other words, the root lengths take only two possible values.
Русский
Существуют такие i, j, что для каждого k B(α_k, α_k) равен либо B(α_i, α_i), либо B(α_j, α_j). Иными словами, длины корней принимает не более двух значений.
LaTeX
$$$\exists i,j,\, \forall k,\ B(α_k, α_k) = B(α_i, α_i) \lor B(α_k, α_k) = B(α_j, α_j)$$$
Lean4
/-- A reduced irreducible finite crystallographic root system has roots of at most two different
lengths. -/
theorem exists_apply_eq_or [Nonempty ι] :
∃ i j, ∀ k, B.form (α k) (α k) = B.form (α i) (α i) ∨ B.form (α k) (α k) = B.form (α j) (α j) :=
by
obtain ⟨i⟩ := inferInstanceAs (Nonempty ι)
by_cases h : (∀ j, B.form (α j) (α j) = B.form (α i) (α i))
· refine ⟨i, i, fun j ↦ by simp [h j]⟩
· push_neg at h
obtain ⟨j, hji_ne⟩ := h
refine ⟨i, j, fun k ↦ ?_⟩
by_contra! hk
obtain ⟨hki_ne, hkj_ne⟩ := hk
have hij := (B.apply_eq_or i j).resolve_left hji_ne.symm
have hik := (B.apply_eq_or i k).resolve_left hki_ne.symm
have hjk := (B.apply_eq_or j k).resolve_left hkj_ne.symm
grind
