-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
/-- See also `RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four`. -/
lemma linearIndependent_iff_coxeterWeight_ne_four :
    LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.coxeterWeight i j = 4

Tactic:
suffices P.coxeterWeight i j • P.root i = (4 : R) • P.root i from
  smul_left_injective R (P.ne_zero i) this

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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.coxeterWeight i j • P.root i = 4 • 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
⊢ LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4

Tactic:
have : 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
this : NoZeroSMulDivisors ℤ M
⊢ LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 4

Tactic:
rw [LinearIndependent.pair_symm_iff] at 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 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
this : NoZeroSMulDivisors ℤ M
h : P.coxeterWeight i j ≠ 4
⊢ LinearIndependent R ![P.root i, P.root j]

Tactic:
contrapose! 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.coxeterWeight i j = 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.pairing i j • 2 • P.root j = 4 • P.root i

Tactic:
rw [smul_comm, h₂, ← mul_smul]

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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (2 * 2) • P.root i = 4 • 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
this : NoZeroSMulDivisors ℤ M
⊢ LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4

Tactic:
refine ⟨coxeterWeight_ne_four_of_linearIndependent P, fun 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
this : NoZeroSMulDivisors ℤ M
h : P.coxeterWeight i j ≠ 4
⊢ LinearIndependent R ![P.root i, P.root 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
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.coxeterWeight i j • P.root i = 4 • P.root i

Tactic:
calc P.coxeterWeight i j • P.root i
    = (P.pairing i j * P.pairing j i) • P.root i := by rfl
  _ = P.pairing i j • (2 : R) • P.root j := by rw [mul_smul, h₁]
  _ = (4 : R) • P.root i := by rw [smul_comm, h₂, ← mul_smul]; 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.coxeterWeight i j = 4

Tactic:
have h₁ := P.pairing_smul_root_eq_of_not_linInd 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 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
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (P.pairing i j * P.pairing j i) • P.root i = P.pairing i j • 2 • P.root j

Tactic:
rw [mul_smul, h₁]

Result:
no goals