-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairing_smul_root_eq_of_not_linInd [NeZero (2 : R)] [NoZeroSMulDivisors R M]
    (h : ¬ LinearIndependent R ![P.root i, P.root j]) :
    P.pairing j i • P.root i = (2 : R) • 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : s • P.root i = -t • P.root j
h₄ : s * 2 = -(t * P.pairing j i)
⊢ 2 • s • P.root i = 2 • -t • P.root j

Tactic:
rw [h₁]

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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
t : R
h₁ : 0 • P.root i + t • P.root j = 0
h₂ : 0 = 0 → t ≠ 0
⊢ t • P.root j = 0

Tactic:
simpa using h₁

Result:
no goals

Proof state:
case intro.intro.intro
ι : 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ : 2 • s • P.root i = 2 • -t • P.root j
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
rw [smul_smul, mul_comm, h₄, smul_comm, ← neg_mul, ← smul_smul] at h₁

Result:
case intro.intro.intro
ι : 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ : -t • P.pairing j i • P.root i = -t • 2 • P.root j
⊢ P.pairing j i • P.root i = 2 • 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : s • P.root i = -t • P.root j
⊢ s * 2 = -(t * P.pairing j i)

Tactic:
simpa using congr_arg (P.coroot' i) h₁

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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s = 0 → t ≠ 0
⊢ s ≠ 0

Tactic:
rcases eq_or_ne s 0 with rfl | hs

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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
t : R
h₁ : 0 • P.root i + t • P.root j = 0
h₂ : 0 = 0 → t ≠ 0
⊢ 0 ≠ 0

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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s = 0 → t ≠ 0
hs : s ≠ 0
⊢ s ≠ 0

Proof state:
case intro.intro.intro
ι : 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ : -t • P.pairing j i • P.root i = -t • 2 • P.root j
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
exact smul_right_injective M (neg_ne_zero.mpr h₃) h₁

Result:
no goals

Proof state:
case intro.intro.intro
ι : 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
replace h₁ : s • P.root i = -t • P.root j := by rwa [← eq_neg_iff_add_eq_zero, ← neg_smul] at h₁

Result:
case intro.intro.intro
ι : 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : s • P.root i = -t • P.root j
⊢ P.pairing j i • P.root i = 2 • 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
rw [LinearIndependent.pair_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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
h : ¬∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
⊢ P.pairing j i • P.root i = 2 • P.root j

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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s : R
h₂ : s ≠ 0
h₁ : s • P.root i + 0 • P.root j = 0
⊢ 0 ≠ 0

Tactic:
exact False.elim <| h₂ <| (smul_eq_zero_iff_left <| P.ne_zero i).mp <| by simpa using h₁

Result:
no goals

Proof state:
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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s = 0 → t ≠ 0
hs : s ≠ 0
⊢ s ≠ 0

Tactic:
assumption

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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s : R
h₂ : s ≠ 0
h₁ : s • P.root i + 0 • P.root j = 0
⊢ s • P.root i = 0

Tactic:
simpa using h₁

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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
h : ∃ s t, s • P.root i + t • P.root j = 0 ∧ (s = 0 → t ≠ 0)
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
obtain ⟨s, t, h₁, h₂⟩ := h

Result:
case intro.intro.intro
ι : 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✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s = 0 → t ≠ 0
⊢ P.pairing j i • P.root i = 2 • P.root j