-- 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 pos
ι : 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.coxeterWeightIn ℤ i j ∈ {1, 2, 3}
⊢ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1

Tactic:
simp_rw [coxeterWeightIn, Int.mul_mem_one_two_three_iff, mem_insert_iff, mem_singleton_iff,
  Prod.mk.injEq] at this

Result:
case pos
ι : 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.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
        P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 1 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
            P.pairingIn ℤ i j = -2 ∧ P.pairingIn ℤ j i = -1 ∨
              P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
                P.pairingIn ℤ i j = 3 ∧ P.pairingIn ℤ j i = 1 ∨
                  P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -3 ∧ P.pairingIn ℤ j i = -1
⊢ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1

Proof state:
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

Tactic:
replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]

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.pairing i j = 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]
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)}
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(1, 4), (2, 2), (4, 1)}

Tactic:
replace hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4 :=
  (P.coxeterWeightIn_eq_four_iff_not_linearIndependent ℤ).mpr 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
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)}

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]
this : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(1, 4), (2, 2), (4, 1)}
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk.injEq] at this

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

Proof state:
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.pairing i j = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
exact ⟨P.reflection_perm j i, by simpa [h₁] using P.reflection_apply_root j i⟩

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]
h₁ : P.pairing j i = 1
⊢ P.root ((P.reflection_perm i) j) = P.root j - P.root i

Tactic:
simpa [h₁] using P.reflection_apply_root i j

Result:
no goals