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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
hu₃ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) ⊆ u
⊢ ∑ x_1 ∈ u,
      HSMul.hSMul (β := R) x_1
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((((F : (a : loopAlgebra R A L) → A →₀ L) (x + y) : A →₀ L) : (a : A) → L) x_1 : L) :
          R) =
    HAdd.hAdd (α := R)
      (∑ x_1 ∈ u,
        HSMul.hSMul (β := R) x_1
          ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                  L →ₗ[R] R) :
                (a : L) → R)
              ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
            R))
      (∑ x ∈ u,
        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) y : A →₀ L) : (a : A) → L) x : L) :
            R))

Tactic:
simp [Finset.sum_add_distrib, u]

Premises used: Finset.sum_add_distrib
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ ∀ (i : A),
    Membership.mem (γ := Finset A) (support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x)) i →
      HSMul.hSMul (β := R) i
          ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-i)) :
                  L →ₗ[R] R) :
                (a : L) → R)
              0 :
            R) =
        0

Tactic:
simp
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x),
      HSMul.hSMul (β := R) x_1
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((HSMul.hSMul (β := A →₀ L) r ((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
          R))
    (∑ x_1 ∈ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x),
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (HSMul.hSMul (β := R) x_1
          ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                  L →ₗ[R] R) :
                (a : L) → R)
              ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
            R)))
⊢ (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (r • x)) 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)) =
    HSMul.hSMul (α := R) (β := R) ((RingHom.id R : (a : R) → R) r : R)
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) x) 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))

Tactic:
rw [map_smul, sum_of_support_subset _ support_smul _ (by simp), sum, Finset.smul_sum]

Premises used: Finsupp.sum, Finsupp.support_smul, Finset.smul_sum, map_smul, Finsupp.sum_of_support_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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x),
      HSMul.hSMul (β := R) x_1
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((HSMul.hSMul (β := A →₀ L) r ((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
          R))
    (∑ x_1 ∈ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x),
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (HSMul.hSMul (β := R) x_1
          ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                  L →ₗ[R] R) :
                (a : L) → R)
              ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
            R)))

Tactic:
simp [-smul_eq_mul, smul_comm]

Premises used: smul_eq_mul, SMulCommClass.smul_comm
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
x y : loopAlgebra R A L
x_1 : A
x_2 : L
⊢ Eq.{u_1 + 1} (α := R)
    ((((TensorProduct.AlgebraTensorModule.curry
                    {
                      toFun := fun (g : loopAlgebra R A L) ↦
                        sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                          HSMul.hSMul (β := R) a
                            ((((Φ : (a : L) → L →ₗ[R] R)
                                      ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) (x + y) : A →₀ L) :
                                          (a : A) → L)
                                        (-a)) :
                                    L →ₗ[R] R) :
                                  (a : L) → R)
                                v :
                              R),
                      map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
                  AddMonoidAlgebra.lsingle x_1 :
                R →ₗ[R] L →ₗ[R] R) :
              (a : R) → L →ₗ[R] R)
            1 :
          (a : L) → R)
        x_2 :
      R)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (HAdd.hAdd (α := loopAlgebra R A L →ₗ[R] R)
                      {
                        toFun := fun (g : loopAlgebra R A L) ↦
                          sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                            HSMul.hSMul (β := R) a
                              ((((Φ : (a : L) → L →ₗ[R] R)
                                        ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) :
                                            (a : A) → L)
                                          (-a)) :
                                      L →ₗ[R] R) :
                                    (a : L) → R)
                                  v :
                                R),
                        map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }
                      {
                        toFun := fun (g : loopAlgebra R A L) ↦
                          sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                            HSMul.hSMul (β := R) a
                              ((((Φ : (a : L) → L →ₗ[R] R)
                                        ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) :
                                            (a : A) → L)
                                          (-a)) :
                                      L →ₗ[R] R) :
                                    (a : L) → R)
                                  v :
                                R),
                        map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }) ∘ₗ
                  AddMonoidAlgebra.lsingle x_1 :
                R →ₗ[R] L →ₗ[R] R) :
              (a : R) → L →ₗ[R] R)
            1 :
          (a : L) → R)
        x_2 :
      R)

Tactic:
simp [sum_add]

Premises used: Finsupp.sum_add
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
r : R
x : loopAlgebra R A L
x_1 : A
x_2 : L
⊢ Eq.{u_1 + 1} (α := R)
    ((((TensorProduct.AlgebraTensorModule.curry
                    {
                      toFun := fun (g : loopAlgebra R A L) ↦
                        sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                          HSMul.hSMul (β := R) a
                            ((((Φ : (a : L) → L →ₗ[R] R)
                                      ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) (r • x) : A →₀ L) :
                                          (a : A) → L)
                                        (-a)) :
                                    L →ₗ[R] R) :
                                  (a : L) → R)
                                v :
                              R),
                      map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
                  AddMonoidAlgebra.lsingle x_1 :
                R →ₗ[R] L →ₗ[R] R) :
              (a : R) → L →ₗ[R] R)
            1 :
          (a : L) → R)
        x_2 :
      R)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (HSMul.hSMul (α := R) (β := loopAlgebra R A L →ₗ[R] R) ((RingHom.id R : (a : R) → R) r : R)
                      {
                        toFun := fun (g : loopAlgebra R A L) ↦
                          sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                            HSMul.hSMul (β := R) a
                              ((((Φ : (a : L) → L →ₗ[R] R)
                                        ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) :
                                            (a : A) → L)
                                          (-a)) :
                                      L →ₗ[R] R) :
                                    (a : L) → R)
                                  v :
                                R),
                        map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }) ∘ₗ
                  AddMonoidAlgebra.lsingle x_1 :
                R →ₗ[R] L →ₗ[R] R) :
              (a : R) → L →ₗ[R] R)
            1 :
          (a : L) → R)
        x_2 :
      R)

Tactic:
simp [-smul_eq_mul, smul_comm]

Premises used: smul_eq_mul, SMulCommClass.smul_comm
-- 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
⊢ Membership.mem (γ :=
    Submodule R (loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R))
    (Cohomology.twoCochain R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))
    (LinearMap.compr₂ (residuePairing R A L Φ)
      (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
        R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R))

Tactic:
Cohomology.mem_twoCochain_iff.mpr fun f ↦ ?_

Premises used: Iff.mpr, Set.Mem, setOf, LieModule.Cohomology.mem_twoCochain_iff
-- 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
refine :
  ∀ (f : loopAlgebra R A L),
    Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
      ((((LinearMap.compr₂ (residuePairing R A L Φ)
                    (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
                      R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                  (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                f :
              loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
            (a : loopAlgebra R A L) → TrivialLieModule R (loopAlgebra R A L) R)
          f :
        TrivialLieModule R (loopAlgebra R A L) R)
      (0 : TrivialLieModule R (loopAlgebra R A L) R)
⊢ Membership.mem (γ :=
    Submodule R (loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R))
    (Cohomology.twoCochain R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))
    (LinearMap.compr₂ (residuePairing R A L Φ)
      (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
        R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R))

Tactic:
refine Cohomology.mem_twoCochain_iff.mpr fun f ↦ ?_

Premises used: Iff.mpr, LieModule.Cohomology.mem_twoCochain_iff
-- 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
this :
  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
⊢ Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
    ((((LinearMap.compr₂ (residuePairing R A L Φ)
                  (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
                    R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
              f :
            loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
          (a : loopAlgebra R A L) → TrivialLieModule R (loopAlgebra R A L) R)
        f :
      TrivialLieModule R (loopAlgebra R A L) R)
    (0 : TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
simpa
-- 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
suffices :
  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
⊢ Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
    ((((LinearMap.compr₂ (residuePairing R A L Φ)
                  (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
                    R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
              f :
            loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
          (a : loopAlgebra R A L) → TrivialLieModule R (loopAlgebra R A L) R)
        f :
      TrivialLieModule R (loopAlgebra R A L) R)
    (0 : TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
suffices ((F f).sum fun a v ↦ a • Φ (F f (-a)) v) = 0 by simpa
-- 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
⊢ 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));
  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))

Tactic:
set s := (F f).support ∪ (F f).support.image (Equiv.neg A) with hs

Premises used: Equiv.neg, Finsupp.support, DFunLike.coe, Finset.image
-- 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))
⊢ Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s

Tactic:
have hs' : (F f).support ⊆ s := Finset.subset_union_left
-- 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
⊢ ∀ i ∈ s,
    HSMul.hSMul (β := R) i
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-i)) :
                L →ₗ[R] R) :
              (a : L) → R)
            0 :
          R) =
      0

Tactic:
simp
-- 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
rw :
  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
⊢ 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:
rw [Finsupp.sum_of_support_subset _ hs' _ (by simp)]

Premises used: Finsupp.sum_of_support_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
n : A
⊢ HSMul.hSMul (β := R) (-n)
      ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (- -n)) :
              L →ₗ[R] R) :
            (a : L) → R)
          ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-n) : L) :
        R) =
    -HSMul.hSMul (β := R) n
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-n)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) n : L) :
          R)

Tactic:
simp [hΦ.eq]

Premises used: LinearMap.BilinForm.IsSymm.eq