English
If P.pairingIn ℤ i j ≠ 0, then among the five possibilities for the invariant form values, one holds: B(α_i, α_i) equals B(α_j, α_j); or equals 2 B(α_j, α_j); or equals 3 B(α_j, α_j); or B(α_j, α_j) equals 2 B(α_i, α_i); or B(α_j, α_j) equals 3 B(α_i, α_i).
Русский
Если P.pairingIn ℤ i j ≠ 0, то выполняется одно из пяти равенств для значений инвариантной формы: B(α_i, α_i) = B(α_j, α_j) или B(α_i, α_i) = 2 B(α_j, α_j) и т. д.
LaTeX
$$$P.pairingIn ℤ i j \neq 0 \Rightarrow \\ B(α_i, α_i) = B(α_j, α_j) \lor B(α_i, α_i) = 2 B(α_j, α_j) \lor B(α_i, α_i) = 3 B(α_j, α_j) \lor B(α_j, α_j) = 2 B(α_i, α_i) \lor B(α_j, α_j) = 3 B(α_i, α_i)$$$
Lean4
theorem apply_eq_or_aux (i j : ι) (h : P.pairingIn ℤ i j ≠ 0) :
B.form (α i) (α i) = B.form (α j) (α j) ∨
B.form (α i) (α i) = 2 * B.form (α j) (α j) ∨
B.form (α i) (α i) = 3 * B.form (α j) (α j) ∨
B.form (α j) (α j) = 2 * B.form (α i) (α i) ∨ B.form (α j) (α j) = 3 * B.form (α i) (α i) :=
by
have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
have h₂ :
algebraMap ℤ R (P.pairingIn ℤ j i) * B.form (α i) (α i) = algebraMap ℤ R (P.pairingIn ℤ i j) * B.form (α j) (α j) :=
by simpa only [algebraMap_pairingIn] using B.pairing_mul_eq_pairing_mul_swap i j
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
