awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x y : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
suffices :
  ∀ (i : ι) (y : L i),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (⁅x, (of L i : (a : L i) → ⨁ (i : ι), L i) y⁆ : ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L') ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x : L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L')
        ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') x : L')
        ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') y) :
      L')

Tactic:
suffices ∀ (i : ι) (y : L i),
          toModule R ι L' f' ⁅x, of L i y⁆ =
            ⁅toModule R ι L' f' x, toModule R ι L' f' (of L i y)⁆ by
        simp only [← LieAlgebra.ad_apply R]
        rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
        congr; clear y; ext i y; exact this i y
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
rw :
  Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
        (-Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) x) :
      L')
    (-Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
        (⁅x, (of L i : (a : L i) → ⨁ (i : ι), L i) y⁆ : ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x : L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
      L')

Tactic:
rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]

Premises used: lie_skew, DirectSum.toModule, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
simp :
  Eq (α := L')
    ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
        ((((LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
                Module.End R (⨁ (i : ι), L i)) :
              (a : ⨁ (i : ι), L i) → ⨁ (i : ι), L i)
            x :
          ⨁ (i : ι), L i) :
      L')
    ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
              ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                L') :
            Module.End R L') :
          (a : L') → L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x : L') :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
        (-Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) x) :
      L')
    (-Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x) :
      L')

Tactic:
simp only [map_neg, neg_inj, ← LieAlgebra.ad_apply R]

Premises used: map_neg, LieAlgebra.ad_apply, neg_inj
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
rw :
  Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' f' ∘ₗ
            (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          (a : ⨁ (i : ι), L i) → L')
        x :
      L')
    (((LieAlgebra.ad R L' : (a : L') → Module.End R L')
              ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                L') ∘ₗ
            toModule R ι (M := L) L' f' :
          (a : ⨁ (i : ι), L i) → L')
        x :
      L')
⊢ Eq (α := L')
    ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
        ((((LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
                Module.End R (⨁ (i : ι), L i)) :
              (a : ⨁ (i : ι), L i) → ⨁ (i : ι), L i)
            x :
          ⨁ (i : ι), L i) :
      L')
    ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
              ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                L') :
            Module.End R L') :
          (a : L') → L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x : L') :
      L')

Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
e_a :
  toModule R ι (M := L) L' f' ∘ₗ
      (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
        ((of L i : (a : L i) → ⨁ (i : ι), L i) y) =
    (LieAlgebra.ad R L' : (a : L') → Module.End R L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
          L') ∘ₗ
      toModule R ι (M := L) L' f'
⊢ Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' f' ∘ₗ
            (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          (a : ⨁ (i : ι), L i) → L')
        x :
      L')
    (((LieAlgebra.ad R L' : (a : L') → Module.End R L')
              ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                L') ∘ₗ
            toModule R ι (M := L) L' f' :
          (a : ⨁ (i : ι), L i) → L')
        x :
      L')

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
e_a :
  ∀ (j : ι) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((((toModule R ι (M := L) L' f' ∘ₗ
                  (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
                    ((of L i : (a : L i) → ⨁ (i : ι), L i) y)) ∘ₗ
                lof R ι L j :
              LinearMap.{u, u, w, w₁} (RingHom.id R) (L j) L') :
            (a : L j) → L')
          x :
        L')
      ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
                  ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                      ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                    L') ∘ₗ
                toModule R ι (M := L) L' f') ∘ₗ
              lof R ι L j :
            (a : L j) → L')
          x :
        L')
⊢ toModule R ι (M := L) L' f' ∘ₗ
      (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
        ((of L i : (a : L i) → ⨁ (i : ι), L i) y) =
    (LieAlgebra.ad R L' : (a : L') → Module.End R L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
          L') ∘ₗ
      toModule R ι (M := L) L' f'

Tactic:
ext j x
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
j : ι
x : L j
⊢ Eq.{w₁ + 1} (α := L')
    ((((toModule R ι (M := L) L' f' ∘ₗ
                (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y)) ∘ₗ
              lof R ι L j :
            LinearMap.{u, u, w, w₁} (RingHom.id R) (L j) L') :
          (a : L j) → L')
        x :
      L')
    ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
                ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                    ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                  L') ∘ₗ
              toModule R ι (M := L) L' f') ∘ₗ
            lof R ι L j :
          (a : L j) → L')
        x :
      L')

Tactic:
this j i x y

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
i : ι
y : L i
j : ι
x : L j
⊢ Eq.{w₁ + 1} (α := L')
    ((((toModule R ι (M := L) L' f' ∘ₗ
                (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i))
                  ((of L i : (a : L i) → ⨁ (i : ι), L i) y)) ∘ₗ
              lof R ι L j :
            LinearMap.{u, u, w, w₁} (RingHom.id R) (L j) L') :
          (a : L j) → L')
        x :
      L')
    ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
                ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
                    ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) :
                  L') ∘ₗ
              toModule R ι (M := L) L' f') ∘ₗ
            lof R ι L j :
          (a : L j) → L')
        x :
      L')

Tactic:
exact this j i x y
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x y : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
suffices :
  ∀ (i j : ι) (y : L i) (x : L j),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
              ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
            L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')
⊢ ∀ (i : ι) (y : L i),
    Eq.{w₁ + 1} (α := L')
      ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          (⁅x, (of L i : (a : L i) → ⨁ (i : ι), L i) y⁆ : ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L') ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L') x : L')
          ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
        L')

Tactic:
suffices ∀ (i j) (y : L i) (x : L j),
          toModule R ι L' f' ⁅of L j x, of L i y⁆ =
            ⁅toModule R ι L' f' (of L j x), toModule R ι L' f' (of L i y)⁆ by
        intro i y
        rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]
        simp only [map_neg, neg_inj, ← LieAlgebra.ad_apply R]
        rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
        congr; clear x; ext j x; exact this j i x y
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
simp :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
            ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) :
          L')
        ((toModule R ι (M := L) L' f' : (a : ⨁ (i : ι), L i) → L')
          ((of L i : (a : L i) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i)) :
      L')

Tactic:
simp only [f', coe_toModule_eq_coe_toAddMonoid, toAddMonoid_of]

Premises used: DirectSum.coe_toModule_eq_coe_toAddMonoid, DirectSum.toAddMonoid_of