-- 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:
ι : 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
this :
  (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), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(1, 4), (2, 2), (4, 1)}

Tactic:
aesop

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
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
aux₃ : P.coxeterWeightIn ℤ i j ≠ 0
⊢ P.coxeterWeightIn ℤ i j ∈ {1, 2, 3}

Tactic:
aesop

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
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 = 1 ∨ P.pairingIn ℤ j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rcases this with h₁ | h₁

Result:
case 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]
h₁ : P.pairingIn ℤ i j = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

case 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
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]
h₁ : P.pairingIn ℤ j i = 1
⊢ 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}
aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
⊢ P.coxeterWeightIn ℤ i j ∈ {1, 2, 3}

Tactic:
have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by
  simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'

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
aux₃ : P.coxeterWeightIn ℤ i j ≠ 0
⊢ P.coxeterWeightIn ℤ i j ∈ {1, 2, 3}

Proof state:
case neg.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
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 = 4 ∧ P.pairingIn ℤ j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rw [and_comm] at hij

Result:
case neg.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
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 ℤ j i = 1 ∧ P.pairingIn ℤ i j = 4
⊢ 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 : P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 2
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rw [P.pairingIn_two_two_iff] at hij

Result:
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

Proof state:
case neg.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
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 ℤ j i = 1 ∧ P.pairingIn ℤ i j = 4
⊢ P.root i - P.root j ∈ range ⇑P.root

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

Result:
no goals