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

Tactic:
rw [h₂, show (4 : R) = 2 * 2 by norm_num, mul_smul] at 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 : 2 • 2 • P.root i = 2 • P.root j
⊢ P.root j = 2 • 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
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

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

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
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

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 : 2 • 2 • P.root i = 2 • P.root j
⊢ P.root j = 2 • P.root i

Tactic:
exact smul_right_injective M two_ne_zero this.symm

Result:
no goals

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 j) = 1 ∧ (P.root' j) (2 • P.coroot j) = 4

Tactic:
norm_num

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

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
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ ?_⟩

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
⊢ P.root j = 2 • P.root i

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

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
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

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

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
⊢ P.root j = 2 • P.root i

Tactic:
have : ¬ LinearIndependent R ![P.root i, P.root j] := by
  rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; norm_num

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 : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root j = 2 • P.root i