-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
/-- This is Lemma 2.5 (a) from [Geck](Geck2017). -/
lemma root_sub_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ)
    (hkj : k ≠ j) (hk' : α k + α i ∈ Φ) :
    α k - α j ∈ Φ

Proof state:
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ i k ≤ -2
hk' : P.root i ≠ -P.root k
aux : P.pairingIn ℤ i k = -2 → ¬P.pairingIn ℤ k i = -2
⊢ P.pairingIn ℤ k i = -1

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i k

Result:
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ i k ≤ -2
hk' : P.root i ≠ -P.root k
aux : P.pairingIn ℤ i k = -2 → ¬P.pairingIn ℤ k i = -2
this :
  (P.pairingIn ℤ i k, P.pairingIn ℤ k i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
⊢ P.pairingIn ℤ k i = -1

Proof state:
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
l : ι
hli : l ≠ i
hkj : l ≠ j
hk' : P.root l + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j l ≤ 0
hl : P.root l = P.root l + P.root i - P.root j
⊢ False

Tactic:
exact hij <| by simpa [add_sub_assoc, sub_eq_zero] using hl

Result:
no goals

Proof state:
case h.e'_3
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ 1 - P.pairing j i = -1 + 2 - P.pairing j i

Tactic:
ring

Result:
no goals

Proof state:
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : l ≠ k
⊢ P.root l - P.root k = P.root i - P.root j

Tactic:
rw [hl]

Result:
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : l ≠ k
⊢ P.root k + P.root i - P.root j - P.root k = P.root i - P.root j

Proof state:
case inr.intro
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
⊢ 0 < P.pairingIn ℤ l i

Tactic:
have hkl : l ≠ k := by rintro rfl; exact hij <| by simpa [add_sub_assoc, sub_eq_zero] using hl

Result:
case inr.intro
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : l ≠ k
⊢ 0 < P.pairingIn ℤ l i

Proof state:
case inr.intro
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ k i = -1
⊢ 0 < P.pairingIn ℤ l i

Tactic:
replace hki : P.pairing k i = -1 := by rw [← P.algebraMap_pairingIn ℤ, hki]; simp

Result:
case inr.intro
ι : 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✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ 0 < P.pairingIn ℤ l i