-- 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
set set₁ :
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0
set₂ :
  let 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))),
    Eq.{u_1 + 1} (α := R)
      (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
        HSMul.hSMul (β := R) a
          ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                  L →ₗ[R] R) :
                (a : L) → R)
              v :
            R))
      0
set₃ :
  let 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),
    Eq.{u_1 + 1} (α := R)
      (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
        HSMul.hSMul (β := R) a
          ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                  L →ₗ[R] R) :
                (a : L) → R)
              v :
            R))
      0
set₄ :
  let 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),
    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
set₅ :
  let 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),
    Finset.map (Equiv.toEmbedding (Equiv.neg A)) s ⊆ s
set₆ :
  let 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), x ∈ s
set₇ :
  let 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 (α := 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
set₈ :
  let 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)),
    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
inl :
  let 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
inr inr₁ :
  let 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
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0

Tactic:
classical
    set s := (F f).support ∪ (F f).support.image (Equiv.neg A) with hs
    have hs' : (F f).support ⊆ s := Finset.subset_union_left
    rw [Finsupp.sum_of_support_subset _ hs' _ (by simp)]
    refine Function.Odd.finsetSum_eq_zero (fun n ↦ by simp [hΦ.eq]) (Finset.map_eq_of_subset ?_)
    intro x hx
    rw [Finset.mem_union]
    replace hx : -x ∈ (F f).support ∨ -x ∈ (F f).support.image Neg.neg := by simpa [hs] using hx
    obtain (h | h) := hx
    · exact Or.inr <| Finset.mem_image.mpr ⟨-x, by simp [h]⟩
    · exact Or.inl <| by simpa using h

Premises used: Finsupp.support, Function.Odd.finsetSum_eq_zero, Finset.map_eq_of_subset, Finset.mem_union, Or.inl, DFunLike.coe, Or.inr