-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₁ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₂ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅y, x⁆ : R)
pos₃ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) (-⁅x, y⁆) : R)
pos₄ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) (-⁅x, y⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
pos₅ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (- -(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₆ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₇ :
  HSMul.hSMul (β := R) (-(a + c)) (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₈ :
  -HSMul.hSMul (β := R) (a + c) (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₉ :
  - -HSMul.hSMul (β := R) (a + c) ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₁₀ :
  HSMul.hSMul (β := R) (a + c) ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₁₁ :
  HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
pos₁₂ pos₁₃ :
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)

Tactic:
rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]

Premises used: neg_smul, Bracket.bracket, LinearMap.BilinForm.IsSymm.eq, neg_neg, smul_neg, LinearMap.BilinForm.neg_left, add_comm, lie_skew, add_smul