-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
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
⊢ {
      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' := ⋯ } =
    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 }
have a : ∀ (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' := sorry, map_smul' := sorry } ∘ₗ
                  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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry : 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: ext