English
If B.form(α i, α i) = B.form(α j, α j), then (P.pairingIn i j, P.pairingIn j i) lies in a small set { (0,0), (1,1), (−1,−1), (2,2), (−2,−2) }.
Русский
Если B.form(α i, α i) = B.form(α j, α j), то пара (P.pairingIn i j, P.pairingIn j i) принадлежит { (0,0), (1,1), (−1,−1), (2,2), (−2,−2) }.
LaTeX
$$(P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(0,0),(1,1),(-1,-1),(2,2),(-2,-2)} : Set (ℤ × ℤ))$$
Lean4
theorem rootLength_lt_of_pairingIn_notMem (B : P.RootPositiveForm ℤ) {i j : ι} (hne : α i ≠ α j) (hne' : α i ≠ -α j)
(hij : P.pairingIn ℤ i j ∉ ({-1, 0, 1} : Set ℤ)) : B.rootLength j < B.rootLength i :=
by
have hij' :
P.pairingIn ℤ i j = -3 ∨
P.pairingIn ℤ i j = -2 ∨
P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4 :=
by
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
have aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1 :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
have aux₂ := B.pairingIn_mul_eq_pairingIn_mul_swap i j
have hi := B.rootLength_pos i
rcases aux₁ with hji | hji <;> rcases hij' with hij' | hij' | hij' | hij' | hij' | hij' <;> rw [hji, hij'] at aux₂ <;>
omega
