Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
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
aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
⊢ B.rootLength j < B.rootLength i

Tactic:
rcases aux₁ with hji | hji <;> rcases hij' with hij' | hij' | hij' | hij' | hij' | hij' <;>
  rw [hji, hij'] at aux₂

Goal state after:
case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i

case inl.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i

case inl.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i

case inl.inr.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i

case inl.inr.inr.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i

case inl.inr.inr.inr.inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i

case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i

case inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i

case inr.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i

case inr.inr.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i

case inr.inr.inr.inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i

case inr.inr.inr.inr.inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i