Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case e'_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  (m * m * (P.pairing i j * lsq j)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j
⊢ lsq j • (m * m * P.pairing i j + m * n * (P.pairing i j * P.pairing j i) + n * n * P.pairing j i) • P.coroot k =
    (m * m * (P.pairing i j * lsq j)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k

pp: case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  (m * m * (P.pairing i j * lsq j)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j
⊢ lsq j • (m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j) =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j

Tactic:
· module

Goal state after:
case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  (m * m * (P.pairing i j * lsq j)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j
⊢ lsq j • (m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j) =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j