-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairing_one_four_iff' (h2 : IsSMulRegular R (2 : R)) :
    P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = (2 : R) • P.root i

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : 4 • P.root i = 2 • P.root j
⊢ 4 = 2 * 2

Tactic:
norm_num

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ ¬LinearIndependent R ![P.root i, P.root j]

Tactic:
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ 1 * 4 = 4

Proof state:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ P.pairing i j = 1

Tactic:
suffices (2 : R) • P.pairing i j = (2 : R) • 1 from h2 this

Result:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ 2 • P.pairing i j = 2 • 1

Proof state:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ 2 • P.pairing i j = 2 • 1

Tactic:
rw [pairing, ← map_smul, ← h]

Result:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (P.coroot i) = 2 • 1

Proof state:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (P.coroot i) = 2 • 1

Tactic:
simp

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ 1 * 4 = 4

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_1
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root j = 2 • P.root i

Tactic:
replace this := P.pairing_smul_root_eq_of_not_linInd this

Result:
case refine_1
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : P.pairing j i • P.root i = 2 • P.root j
⊢ P.root j = 2 • P.root i

Proof state:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.root j = 2 • P.root i
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4

Tactic:
rw [← coroot_eq_smul_coroot_iff] at h

Result:
case refine_2
ι : 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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4