[Merged by Bors] - feat: add supporting API for Geck's final root system lemma

Mathlib/LinearAlgebra/RootSystem/Base.lean

@@ -54,8 +54,8 @@ doc string for further remarks. -/
 structure Base (P : RootPairing ι R M N) where
   /-- The set of roots / coroots belonging to the base. -/
   support : Set ι
-  linInd_root : LinearIndependent R fun i : support ↦ P.root i
-  linInd_coroot : LinearIndependent R fun i : support ↦ P.coroot i
+  linInd_root : LinearIndepOn R P.root support
+  linInd_coroot : LinearIndepOn R P.coroot support
   root_mem_or_neg_mem (i : ι) : P.root i ∈ AddSubmonoid.closure (P.root '' support) ∨
                               - P.root i ∈ AddSubmonoid.closure (P.root '' support)
   coroot_mem_or_neg_mem (i : ι) : P.coroot i ∈ AddSubmonoid.closure (P.coroot '' support) ∨
@@ -76,6 +76,16 @@ variable {P : RootPairing ι R M N} (b : P.Base)
   root_mem_or_neg_mem := b.coroot_mem_or_neg_mem
   coroot_mem_or_neg_mem := b.root_mem_or_neg_mem
 
+include b in
+lemma root_ne_neg_of_ne [Nontrivial R] {i j : ι}
+    (hi : i ∈ b.support) (hj : j ∈ b.support) (hij : i ≠ j) :
+    P.root i ≠ - P.root j := by
+  classical
+  intro contra
+  have := linearIndepOn_iff'.mp b.linInd_root ({i, j} : Finset ι) 1
+    (by simp [Set.insert_subset_iff, hi, hj]) (by simp [Finset.sum_pair hij, contra])
+  aesop
+
 lemma root_mem_span_int (i : ι) :
     P.root i ∈ span ℤ (P.root '' b.support) := by
   have := b.root_mem_or_neg_mem i

Mathlib/LinearAlgebra/RootSystem/Chain.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
+import Mathlib.LinearAlgebra.RootSystem.Finite.g2
 import Mathlib.Order.Interval.Set.OrdConnectedLinear
 
 /-!
@@ -166,7 +167,7 @@ lemma root_sub_zsmul_mem_range_iff {z : ℤ} :
 
 omit h
 
-private lemma chainCoeff_relfection_perm_aux :
+private lemma chainCoeff_relfection_perm_left_aux :
     letI := P.indexNeg
     Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) =
       Icc (-P.chainBotCoeff (-i) j : ℤ) (P.chainTopCoeff (-i) j) := by
@@ -181,28 +182,65 @@ private lemma chainCoeff_relfection_perm_aux :
     simp only [chainTopCoeff_of_not_linInd h, chainTopCoeff_of_not_linInd h',
       chainBotCoeff_of_not_linInd h, chainBotCoeff_of_not_linInd h']
 
+private lemma chainCoeff_relfection_perm_right_aux :
+    letI := P.indexNeg
+    Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) =
+      Icc (-P.chainBotCoeff i (-j) : ℤ) (P.chainTopCoeff i (-j)) := by
+  letI := P.indexNeg
+  by_cases h : LinearIndependent R ![P.root i, P.root j]
+  · have h' : LinearIndependent R ![P.root i, P.root (-j)] := by simpa
+    ext z
+    rw [← P.root_add_zsmul_mem_range_iff h', indexNeg_neg, root_reflection_perm, mem_Icc,
+      reflection_apply_self, ← sub_neg_eq_add, ← neg_sub', neg_mem_range_root_iff,
+      P.root_sub_zsmul_mem_range_iff h, mem_Icc]
+  · have h' : ¬ LinearIndependent R ![P.root i, P.root (-j)] := by simpa
+    simp only [chainTopCoeff_of_not_linInd h, chainTopCoeff_of_not_linInd h',
+      chainBotCoeff_of_not_linInd h, chainBotCoeff_of_not_linInd h']
+
 @[simp]
-lemma chainTopCoeff_relfection_perm :
+lemma chainTopCoeff_relfection_perm_left :
     P.chainTopCoeff (P.reflection_perm i i) j = P.chainBotCoeff i j := by
   letI := P.indexNeg
   have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
       z ∈ Icc (-P.chainBotCoeff (-i) j : ℤ) (P.chainTopCoeff (-i) j) := by
-    rw [P.chainCoeff_relfection_perm_aux]
+    rw [P.chainCoeff_relfection_perm_left_aux]
   refine le_antisymm ?_ ?_
   · simpa using this (P.chainTopCoeff (-i) j)
   · simpa using this (P.chainBotCoeff i j)
 
 @[simp]
-lemma chainBotCoeff_relfection_perm :
+lemma chainBotCoeff_relfection_perm_left :
     P.chainBotCoeff (P.reflection_perm i i) j = P.chainTopCoeff i j := by
   letI := P.indexNeg
   have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
       z ∈ Icc (-P.chainBotCoeff (-i) j : ℤ) (P.chainTopCoeff (-i) j) := by
-    rw [P.chainCoeff_relfection_perm_aux]
+    rw [P.chainCoeff_relfection_perm_left_aux]
   refine le_antisymm ?_ ?_
   · simpa using this (-P.chainBotCoeff (-i) j)
   · simpa using this (-P.chainTopCoeff i j)
 
+@[simp]
+lemma chainTopCoeff_relfection_perm_right :
+    P.chainTopCoeff i (P.reflection_perm j j) = P.chainBotCoeff i j := by
+  letI := P.indexNeg
+  have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
+      z ∈ Icc (-P.chainBotCoeff i (-j) : ℤ) (P.chainTopCoeff i (-j)) := by
+    rw [P.chainCoeff_relfection_perm_right_aux]
+  refine le_antisymm ?_ ?_
+  · simpa using this (P.chainTopCoeff i (-j))
+  · simpa using this (P.chainBotCoeff i j)
+
+@[simp]
+lemma chainBotCoeff_relfection_perm_right :
+    P.chainBotCoeff i (P.reflection_perm j j) = P.chainTopCoeff i j := by
+  letI := P.indexNeg
+  have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
+      z ∈ Icc (-P.chainBotCoeff i (-j) : ℤ) (P.chainTopCoeff i (-j)) := by
+    rw [P.chainCoeff_relfection_perm_right_aux]
+  refine le_antisymm ?_ ?_
+  · simpa using this (-P.chainBotCoeff i (-j))
+  · simpa using this (-P.chainTopCoeff i j)
+
 variable (i j)
 
 open scoped Classical in
@@ -255,7 +293,7 @@ lemma chainBotCoeff_sub_chainTopCoeff :
       P.chainBotCoeff i j - P.chainTopCoeff i j ≤ P.pairingIn ℤ j i by
     refine le_antisymm (this i j h) ?_
     specialize this (P.reflection_perm i i) j (by simpa)
-    simp only [chainBotCoeff_relfection_perm, chainTopCoeff_relfection_perm,
+    simp only [chainBotCoeff_relfection_perm_left, chainTopCoeff_relfection_perm_left,
       pairingIn_reflection_perm_self_right] at this
     omega
   intro i j h
@@ -308,22 +346,33 @@ lemma chainTopCoeff_chainTopIdx :
     P.chainTopCoeff i (P.chainTopIdx i j) = 0 :=
   chainCoeff_chainTopIdx_aux.2
 
-lemma chainBotCoeff_add_chainTopCoeff_le [P.IsReduced] :
-    P.chainBotCoeff i j + P.chainTopCoeff i j ≤ 3 := by
-  by_cases h : LinearIndependent R ![P.root i, P.root j]
-  swap; · simp [chainTopCoeff_of_not_linInd, chainBotCoeff_of_not_linInd, h]
+include h in
+lemma chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx :
+    P.chainBotCoeff i j + P.chainTopCoeff i j = P.pairingIn ℤ (P.chainTopIdx i j) i := by
   replace h : LinearIndependent R ![P.root i, P.root (P.chainTopIdx i j)] := by
     rwa [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
       LinearIndependent.pair_add_smul_right_iff]
-  rw [← Int.ofNat_le]
-  calc (↑(P.chainBotCoeff i j + P.chainTopCoeff i j) : ℤ)
+  calc (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
     _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
     _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
     _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]
-    _ ≤ 3 := ?_
-  have _i := P.reflexive_left
+
+lemma chainBotCoeff_add_chainTopCoeff_le_three [P.IsReduced] :
+    P.chainBotCoeff i j + P.chainTopCoeff i j ≤ 3 := by
+  by_cases h : LinearIndependent R ![P.root i, P.root j]
+  swap; · simp [chainTopCoeff_of_not_linInd, chainBotCoeff_of_not_linInd, h]
+  rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat,
+    chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]
   have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i (P.chainTopIdx i j)
-  simp only [mem_insert_iff, mem_singleton_iff, Prod.mk.injEq] at this
-  omega
+  aesop
+
+lemma chainBotCoeff_add_chainTopCoeff_le_two [P.IsNotG2] :
+    P.chainBotCoeff i j + P.chainTopCoeff i j ≤ 2 := by
+  by_cases h : LinearIndependent R ![P.root i, P.root j]
+  swap; · simp [chainTopCoeff_of_not_linInd, chainBotCoeff_of_not_linInd, h]
+  rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat,
+    chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]
+  have := IsNotG2.pairingIn_mem_zero_one_two (P := P) (P.chainTopIdx i j) i
+  aesop
 
 end RootPairing

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -170,6 +170,12 @@ lemma ne_zero [NeZero (2 : R)] : (P.root i : M) ≠ 0 :=
 lemma ne_zero' [NeZero (2 : R)] : (P.coroot i : N) ≠ 0 :=
   P.flip.ne_zero i
 
+lemma zero_nmem_range_root [NeZero (2 : R)] : 0 ∉ range P.root := by
+  simpa only [mem_range, not_exists] using fun i ↦ P.ne_zero i
+
+lemma zero_nmem_range_coroot [NeZero (2 : R)] : 0 ∉ range P.coroot :=
+  P.flip.zero_nmem_range_root
+
 lemma exists_ne_zero [Nonempty ι] [NeZero (2 : R)] : ∃ i, P.root i ≠ 0 := by
   obtain ⟨i⟩ := inferInstanceAs (Nonempty ι)
   exact ⟨i, P.ne_zero i⟩

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

@@ -330,7 +330,7 @@ section IsValuedInOrdered
 
 variable (S : Type*) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S]
   [Algebra S R] [FaithfulSMul S R] [Module S M]
-  [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] {i j : ι}
+  [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] {i j : ι}
 
 /-- The bilinear form of a finite root pairing taking values in a linearly-ordered ring, as a
 root-positive form. -/
@@ -343,21 +343,18 @@ def posRootForm : P.RootPositiveForm S where
     refine ⟨∑ k, P.pairingIn S i k ^ 2, ?_, by simp [sq, rootForm_apply_apply]⟩
     exact Finset.sum_pos' (fun j _ ↦ sq_nonneg _) ⟨i, by simp⟩
 
-omit [Module S N] [IsScalarTower S R N] in
 lemma algebraMap_posRootForm_posForm (x y : span S (range P.root)) :
     (algebraMap S R) ((P.posRootForm S).posForm x y) = P.RootForm x y := by
   rw [RootPositiveForm.algebraMap_posForm]
   exact rfl
 
-omit [Module S N] [IsScalarTower S R N] in
 @[simp]
 lemma posRootForm_eq :
     (P.posRootForm S).posForm = P.RootFormIn S := by
   ext
   apply FaithfulSMul.algebraMap_injective S R
   simp only [algebraMap_posRootForm_posForm, algebraMap_rootFormIn]
 
-omit [Module S N] [IsScalarTower S R N] in
 theorem exists_ge_zero_eq_rootForm (x : M) (hx : x ∈ span S (range P.root)) :
     ∃ s ≥ 0, algebraMap S R s = P.RootForm x x := by
   refine ⟨(P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩, IsSumSq.nonneg ?_, by simp [posRootForm]⟩
@@ -368,26 +365,40 @@ theorem exists_ge_zero_eq_rootForm (x : M) (hx : x ∈ span S (range P.root)) :
   simp only [posRootForm, RootPositiveForm.algebraMap_posForm, map_sum, map_mul]
   simp [← Algebra.linearMap_apply, hs, rootForm_apply_apply]
 
-omit [Module S N] [IsScalarTower S R N] in
 lemma posRootForm_posForm_apply_apply (x y : P.rootSpan S) : (P.posRootForm S).posForm x y =
     ∑ i, P.coroot'In S i x * P.coroot'In S i y := by
   refine (FaithfulSMul.algebraMap_injective S R) ?_
   simp [posRootForm, rootForm_apply_apply]
 
-omit [Module S N] [IsScalarTower S R N] in
 lemma zero_le_posForm (x : span S (range P.root)) :
     0 ≤ (P.posRootForm S).posForm x x := by
   obtain ⟨s, _, hs⟩ := P.exists_ge_zero_eq_rootForm S x.1 x.2
   have : s = (P.posRootForm S).posForm x x :=
     FaithfulSMul.algebraMap_injective S R <| (P.algebraMap_posRootForm_posForm S x x) ▸ hs
   rwa [← this]
 
-omit [Fintype ι] [Module S N] [IsScalarTower S R N] in
-lemma zero_lt_pairingIn_iff' [Finite ι] :
+omit [Fintype ι]
+variable [Finite ι]
+
+lemma zero_lt_pairingIn_iff' :
     0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i :=
   let _i : Fintype ι := Fintype.ofFinite ι
   zero_lt_pairingIn_iff (P.posRootForm S) i j
 
+lemma pairingIn_lt_zero_iff :
+    P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0 := by
+  simpa using P.zero_lt_pairingIn_iff' S (i := i) (j := P.reflection_perm j j)
+
+lemma pairingIn_le_zero_iff [NeZero (2 : R)] [NoZeroSMulDivisors R M] :
+    P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0 := by
+  rcases eq_or_ne (P.pairingIn S i j) 0 with hij | hij <;>
+  rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji
+  · rw [hij, hji]
+  · rw [hij, P.pairingIn_zero_iff.mp hij]
+  · rw [hji, P.pairingIn_zero_iff.mp hji]
+  · rw [le_iff_eq_or_lt, le_iff_eq_or_lt, or_iff_right hij, or_iff_right hji]
+    exact P.pairingIn_lt_zero_iff S
+
 end IsValuedInOrdered
 
 end RootPairing

Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

@@ -50,8 +50,8 @@ lemma coxeterWeightIn_le_four (S : Type*)
   have : Fintype ι := Fintype.ofFinite ι
   let ri : span S Φ := ⟨α i, Submodule.subset_span (mem_range_self _)⟩
   let rj : span S Φ := ⟨α j, Submodule.subset_span (mem_range_self _)⟩
-  set li := (P.posRootForm S).posForm ri ri
-  set lj := (P.posRootForm S).posForm rj rj
+  set li := (P.posRootForm S).rootLength i
+  set lj := (P.posRootForm S).rootLength j
   set lij := (P.posRootForm S).posForm ri rj
   obtain ⟨si, hsi, hsi'⟩ := (P.posRootForm S).exists_pos_eq i
   obtain ⟨sj, hsj, hsj'⟩ := (P.posRootForm S).exists_pos_eq j
@@ -99,26 +99,59 @@ lemma pairingIn_pairingIn_mem_set_of_isCrystallographic :
     (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)
   simpa [← P.algebraMap_pairingIn ℤ] using P.pairing_zero_iff' (i := i) (j := j)
 
-lemma pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed
-    [P.IsReduced] [NoZeroSMulDivisors R M] :
+lemma pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed [P.IsReduced] :
     (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
       ({(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3),
         (-3, -1), (2, 2), (-2, -2)} : Set (ℤ × ℤ)) := by
+  have := P.reflexive_left
   rcases eq_or_ne i j with rfl | h₁; · simp
   rcases eq_or_ne (P.root i) (-P.root j) with h₂ | h₂; · aesop
   have aux₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
   have aux₂ : P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4 := P.coxeterWeightIn_ne_four ℤ h₁ h₂
   aesop
 
-lemma pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'
-    [P.IsReduced] [NoZeroSMulDivisors R M]
+lemma pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' [P.IsReduced]
     (hij : P.root i ≠ P.root j) (hij' : P.root i ≠ - P.root j) :
     (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
       ({(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3),
         (-3, -1)} : Set (ℤ × ℤ)) := by
+  have := P.reflexive_left
   have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
   aesop
 
+variable {P} in
+lemma RootPositiveForm.rootLength_le_of_pairingIn_eq (B : P.RootPositiveForm ℤ) {i j : ι}
+    (hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1) :
+    B.rootLength i ≤ B.rootLength j := by
+  have h : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
+      ({(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)} : Set (ℤ × ℤ)) := by
+    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
+    aesop
+  simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at h
+  have h' := B.pairingIn_mul_eq_pairingIn_mul_swap i j
+  have hi := B.rootLength_pos i
+  rcases h with hij' | hij' | hij' | hij' | hij' | hij' | hij' | hij' <;>
+  rw [hij'.1, hij'.2] at h' <;> omega
+
+variable {P} in
+lemma RootPositiveForm.rootLength_lt_of_pairingIn_nmem
+    (B : P.RootPositiveForm ℤ) {i j : ι}
+    (hne : P.root i ≠ P.root j) (hne' : P.root i ≠ - P.root 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
+  have aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1 := by
+    have _i := P.reflexive_left
+    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
+    aesop
+  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
+
 variable {i j} in
 lemma pairingIn_pairingIn_mem_set_of_length_eq {B : P.InvariantForm}
     (len_eq : B.form (P.root i) (P.root i) = B.form (P.root j) (P.root j)) :
@@ -131,10 +164,11 @@ lemma pairingIn_pairingIn_mem_set_of_length_eq {B : P.InvariantForm}
   aesop
 
 variable {i j} in
-lemma pairingIn_pairingIn_mem_set_of_length_eq_of_ne [NoZeroSMulDivisors R M] {B : P.InvariantForm}
+lemma pairingIn_pairingIn_mem_set_of_length_eq_of_ne {B : P.InvariantForm}
     (len_eq : B.form (P.root i) (P.root i) = B.form (P.root j) (P.root j))
     (ne : i ≠ j) (ne' : P.root i ≠ -P.root j) :
     (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(0, 0), (1, 1), (-1, -1)} : Set (ℤ × ℤ)) := by
+  have := P.reflexive_left
   have := P.pairingIn_pairingIn_mem_set_of_length_eq len_eq
   aesop
 
@@ -280,6 +314,48 @@ lemma apply_eq_or_of_apply_ne
 
 end InvariantForm
 
+lemma forall_pairing_eq_swap_or [P.IsReduced] [P.IsIrreducible] :
+    (∀ i j, P.pairing i j = P.pairing j i ∨
+            P.pairing i j = 2 * P.pairing j i ∨
+            P.pairing j i = 2 * P.pairing i j) ∨
+    (∀ i j, P.pairing i j = P.pairing j i ∨
+            P.pairing i j = 3 * P.pairing j i ∨
+            P.pairing j i = 3 * P.pairing i j) := by
+  have : Fintype ι := Fintype.ofFinite ι
+  have B := (P.posRootForm ℤ).toInvariantForm
+  by_cases h : ∀ i j, B.form (P.root i) (P.root i) = B.form (P.root j) (P.root j)
+  · refine Or.inl fun i j ↦ Or.inl ?_
+    have := B.pairing_mul_eq_pairing_mul_swap j i
+    rwa [h i j, mul_left_inj' (B.ne_zero j)] at this
+  push_neg at h
+  obtain ⟨i, j, hij⟩ := h
+  have key := B.apply_eq_or_of_apply_ne hij
+  set li := B.form (P.root i) (P.root i)
+  set lj := B.form (P.root j) (P.root j)
+  have : (li = 2 * lj ∨ lj = 2 * li) ∨ (li = 3 * lj ∨ lj = 3 * li) := by
+    have := B.apply_eq_or i j; tauto
+  rcases this with this | this
+  · refine Or.inl fun k₁ k₂ ↦ ?_
+    have hk := B.pairing_mul_eq_pairing_mul_swap k₁ k₂
+    rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
+    simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk <;>
+    aesop
+  · refine Or.inr fun k₁ k₂ ↦ ?_
+    have hk := B.pairing_mul_eq_pairing_mul_swap k₁ k₂
+    rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
+    simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk <;>
+    aesop
+
+lemma forall_pairingIn_eq_swap_or [P.IsReduced] [P.IsIrreducible] :
+    (∀ i j, P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
+            P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨
+            P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) ∨
+    (∀ i j, P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
+            P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨
+            P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j) := by
+  simpa only [← P.algebraMap_pairingIn ℤ, eq_intCast, ← Int.cast_mul, Int.cast_inj,
+    ← map_ofNat (algebraMap ℤ R)] using P.forall_pairing_eq_swap_or
+
 namespace Base
 
 variable {P}