-- 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
let let₁ let₂ :
  (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
    HAdd.hAdd (α := 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))
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
let₃ :
  let 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),
    (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
      HAdd.hAdd (α := 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))
        (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
let₄ :
  let 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),
    (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
      HAdd.hAdd (α := 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))
        (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
let₅ :
  let 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),
    (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
      HAdd.hAdd (α := 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))
        (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
let₆ :
  let 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))
⊢ (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
    HAdd.hAdd (α := 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))
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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:
classical
        let u : Finset A := (F x).support ∪ (F y).support
        have hu₁ : (F x).support ⊆ u := Finset.subset_union_left
        have hu₂ : (F y).support ⊆ u := Finset.subset_union_right
        have hu₃ : (F (x + y)).support ⊆ u := fun a ha ↦ by
          replace ha : F x a + F y a ≠ 0 := by simpa using ha
          grind
        rw [sum_of_support_subset _ hu₃ _ (by simp), sum_of_support_subset _ hu₁ _ (by simp),
          sum_of_support_subset _ hu₂ _ (by simp)]
        simp [Finset.sum_add_distrib, u]

Premises used: Finset.sum_add_distrib