awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
refine : Finset.map (Equiv.toEmbedding (Equiv.neg A)) s ⊆ s
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ s,
      HSMul.hSMul (β := R) x
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) x : L) :
          R))
    0

Tactic:
refine Function.Odd.finsetSum_eq_zero (fun n ↦ by simp [hΦ.eq]) (Finset.map_eq_of_subset ?_)

Premises used: Function.Odd.finsetSum_eq_zero, Finset.map_eq_of_subset
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
rw :
  Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x
⊢ x ∈ s

Tactic:
rw [Finset.mem_union]

Premises used: Finset.mem_union
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∨
    Membership.mem (γ := Finset A)
      (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)

Tactic:
simpa [hs] using hx
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∨
    Membership.mem (γ := Finset A)
      (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)

Tactic:
replace hx : -x ∈ (F f).support ∨ -x ∈ (F f).support.image Neg.neg := by simpa [hs] using hx
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx :
  Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∨
    Membership.mem (γ := Finset A)
      (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)
inl :
  ∀
    (h :
      Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
        (-x)),
    Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
      Membership.mem (γ := Finset A)
        (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
          (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
        x
inr :
  ∀
    (h :
      Membership.mem (γ := Finset A)
        (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)),
    Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
      Membership.mem (γ := Finset A)
        (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
          (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
        x
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x

Tactic:
obtain (h | h) := hx
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
h : Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x)
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∧
    (Equiv.neg A : (a : A) → A) (-x) = x

Tactic:
simp [h]
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
h : Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x)
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x

Tactic:
exact Or.inr <| Finset.mem_image.mpr ⟨-x, by simp [h]⟩

Premises used: Iff.mpr, Finset.mem_image, Exists.intro, Neg.neg, Or.inr
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
h :
  Membership.mem (γ := Finset A)
    (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x

Tactic:
simpa using h
-- 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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
h :
  Membership.mem (γ := Finset A)
    (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x

Tactic:
exact Or.inl <| by simpa using h

Premises used: Or.inl
-- 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Φ : Φ.IsSymm
x y : loopAlgebra R A L
⊢ Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
    ((((twoCochainOfBilinear R A L Φ hΦ :
                (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
              x :
            loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
          (a : loopAlgebra R A L) → TrivialLieModule R (loopAlgebra R A L) R)
        y :
      TrivialLieModule R (loopAlgebra R A L) R)
    (((LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R) :
            R ≃ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
          (a : R) → TrivialLieModule R (loopAlgebra R A L) R)
        ((((residuePairing R A L Φ : (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] R) x :
                loopAlgebra R A L →ₗ[R] R) :
              (a : loopAlgebra R A L) → R)
            y :
          R) :
      TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- 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
pos :
  ∀ (h0 : a + b + c = 0),
    HSMul.hSMul (β := R) b
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R)
            y :
          R) =
      HSMul.hSMul (β := R) c
          ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
              z :
            R) +
        HSMul.hSMul (β := R) a
          ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
              x :
            R)
neg :
  ∀ (h0 : ¬a + b + c = 0),
    HSMul.hSMul (β := R) b
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R)
            y :
          R) =
      HSMul.hSMul (β := R) c
          ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
              z :
            R) +
        HSMul.hSMul (β := R) a
          ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
              x :
            R)
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)

Tactic:
by_cases h0 : a + b + c = 0
-- 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
this :
  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)
⊢ a + b = -c

Tactic:
grind
-- 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
this :
  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)
⊢ a + c = -b

Tactic:
grind
-- 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
this :
  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)
⊢ b + c = -a

Tactic:
grind
-- 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
this :
  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)
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)

Tactic:
simpa only [show a + b = -c by grind, show a + c = -b by grind, show b + c = -a by grind,
          Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same
-- 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) ⁅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)
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)

Tactic:
suffices b • Φ ⁅x, z⁆ y = c • Φ ⁅x, y⁆ z + a • Φ ⁅y, z⁆ x by
        simpa only [show a + b = -c by grind, show a + c = -b by grind, show b + c = -a by grind,
          Finsupp.single_eq_same]
-- 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
⊢ b = -(a + c)

Tactic:
grind
-- 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
⊢ -b ≠ a + c

Tactic:
grind
-- 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
⊢ -c ≠ a + b

Tactic:
grind
-- 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
⊢ -a ≠ b + c

Tactic:
grind
-- 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
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)

Tactic:
simp [Finsupp.single_eq_of_ne (a := a + c) (a' := -b) (by grind),
        Finsupp.single_eq_of_ne (a := a + b) (a' := -c) (by grind),
        Finsupp.single_eq_of_ne (a := b + c) (a' := -a) (by grind)]

Premises used: Finsupp.single_eq_of_ne