-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
lemma root_sub_root_mem_of_pairingIn_pos (h : 0 < P.pairingIn ℤ i j) (h' : i ≠ j) :
    α i - α j ∈ Φ

Proof state:
case neg.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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rw [(P.pairingIn_one_four_iff ℤ i j).mp hij, two_smul, sub_add_cancel_right]

Result:
case neg.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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4
⊢ -P.root i ∈ range ⇑P.root

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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
have _i : NoZeroSMulDivisors ℤ M := NoZeroSMulDivisors.int_of_charZero R M

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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
⊢ P.root i - P.root j ∈ range ⇑P.root

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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : LinearIndependent R ![P.root i, P.root j]
aux₁ : P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}
⊢ P.coxeterWeightIn ℤ i j ∈ {1, 2, 3}

Tactic:
have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli

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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : LinearIndependent R ![P.root i, P.root j]
aux₁ : P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}
aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
⊢ P.coxeterWeightIn ℤ i j ∈ {1, 2, 3}

Proof state:
case neg
ι : 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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
have : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(1, 4), (2, 2), (4, 1)} : Set _) := by
  have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
  replace hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4 :=
    (P.coxeterWeightIn_eq_four_iff_not_linearIndependent ℤ).mpr hli
  aesop

Result:
case neg
ι : 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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : ¬LinearIndependent R ![P.root i, P.root j]
this : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(1, 4), (2, 2), (4, 1)}
⊢ P.root i - P.root j ∈ range ⇑P.root

Proof state:
case neg.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
i j : ι
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
_i : NoZeroSMulDivisors ℤ M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : i = j
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
contradiction

Result:
no goals