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

Tactic:
have h₄ : s * 2 = - (t * P.pairing j i) := by simpa using congr_arg (P.coroot' i) 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
h₄ : s * 2 = -(t * P.pairing j i)
⊢ 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 : ¬∀ (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

Tactic:
push_neg 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, 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 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
h₄ : s * 2 = -(t * P.pairing j i)
⊢ P.pairing j i • P.root i = 2 • P.root j

Tactic:
replace h₁ : (2 : R) • (s • P.root i) = (2 : R) • (-t • P.root j) := by rw [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₁ : 2 • s • P.root i = 2 • -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
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s ≠ 0
⊢ t ≠ 0

Tactic:
rcases eq_or_ne t 0 with rfl | ht

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
s : R
h₂ : s ≠ 0
h₁ : s • P.root i + 0 • P.root j = 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
ht : t ≠ 0
⊢ t ≠ 0

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
ht : t ≠ 0
⊢ t ≠ 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 t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ s • P.root i = -t • P.root j

Tactic:
rwa [← eq_neg_iff_add_eq_zero, ← neg_smul] at h₁

Result:
no goals

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
t : R
h₁ : 0 • P.root i + t • P.root j = 0
h₂ : 0 = 0 → t ≠ 0
⊢ 0 ≠ 0

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

Result:
no goals