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)
x y z : ⨁ (i : ι), L i
i : ι
w :
  ⁅(x : (a : ι) → L a) i, ⁅(y : (a : ι) → L a) i, (z : (a : ι) → L a) i⁆⁆ =
    ⁅⁅(x : (a : ι) → L a) i, (y : (a : ι) → L a) i⁆, (z : (a : ι) → L a) i⁆ +
      ⁅(y : (a : ι) → L a) i, ⁅(x : (a : ι) → L a) i, (z : (a : ι) → L a) i⁆⁆
⊢ (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
          (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) ⋯ x
          (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
            (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) ⋯ y z) :
        (a : ι) → L a)
      i =
    (HAdd.hAdd (α := ⨁ (i : ι), L i)
          (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
            (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) ⋯
            (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
              (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) ⋯ x y)
            z)
          (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
            (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) ⋯ y
            (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
              (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) ⋯ x z)) :
        (a : ι) → L a)
      i

Tactic:
simp only [zipWith_apply, add_apply]

Premises used: DFinsupp.zipWith_apply, DirectSum.add_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)
x y z : ⨁ (i : ι), L i
i : ι
⊢ ⁅(x : (a : ι) → L a) i, ⁅(y : (a : ι) → L a) i, (z : (a : ι) → L a) i⁆⁆ =
    ⁅⁅(x : (a : ι) → L a) i, (y : (a : ι) → L a) i⁆, (z : (a : ι) → L a) i⁆ +
      ⁅(y : (a : ι) → L a) i, ⁅(x : (a : ι) → L a) i, (z : (a : ι) → L a) i⁆⁆

Tactic:
apply leibniz_lie

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
x y : ⨁ (i : ι), L i
i : ι
⊢ (⁅x, y⁆ : (a : ι) → L a) i = ⁅(x : (a : ι) → L a) i, (y : (a : ι) → L a) i⁆

Tactic:
zipWith_apply _ _ x y i

Premises used: DFinsupp.zipWith_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i : ι
x y : L i
⊢ Eq (α := ⨁ (i : ι), L i)
    (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
        ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
      ⨁ (i : ι), L i)
    ((of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, y⁆ : ⨁ (i : ι), L i)

Tactic:
DFinsupp.zipWith_single_single _ _ _ _

Premises used: DFinsupp.zipWith_single_single, DFinsupp.single, DirectSum
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
w :
  ∀ (k : ι),
    ((Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L j : (a : L j) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
          (a : ι) → L a)
        k =
      (0 : (a : ι) → L a) k
⊢ Eq (α := ⨁ (i : ι), L i)
    (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
        ((of L j : (a : L j) → ⨁ (i : ι), L i) y) :
      ⨁ (i : ι), L i)
    (0 : ⨁ (i : ι), L i)

Tactic:
ext k
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
w :
  ⁅(((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k,
      (((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k⁆ =
    (0 : (a : ι) → L a) k
⊢ ((Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L j : (a : L j) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
        (a : ι) → L a)
      k =
    (0 : (a : ι) → L a) k

Tactic:
rw [bracket_apply]

Premises used: DirectSum.bracket_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
w :
  ∀ (hij : k ≠ j) (x : L k),
    ⁅(((of L k : (a : L k) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k,
        (((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k⁆ =
      (0 : (a : ι) → L a) k
w₁ :
  ∀ (hik : k ≠ i),
    ⁅(((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k,
        (((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k⁆ =
      (0 : (a : ι) → L a) k
⊢ ⁅(((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k,
      (((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k⁆ =
    (0 : (a : ι) → L a) k

Tactic:
obtain rfl | hik := Decidable.eq_or_ne k i

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
j : ι
y : L j
k : ι
hij : k ≠ j
x : L k
w : ⁅(((of L k : (a : L k) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k, 0⁆ = (0 : (a : ι) → L a) k
w₁ : 0 = (0 : (a : ι) → L a) k
w₂ w₃ : Eq.{w + 1} (α := L k) 0 0
⊢ ⁅(((of L k : (a : L k) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k,
      (((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k⁆ =
    (0 : (a : ι) → L a) k

Tactic:
rw [of_eq_of_ne _ _ _ hij, lie_zero, zero_apply]

Premises used: lie_zero, DirectSum.zero_apply, DirectSum.of_eq_of_ne
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
w :
  Bracket.bracket (L := L k) 0 ((((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k) =
    (0 : (a : ι) → L a) k
w₁ : 0 = (0 : (a : ι) → L a) k
w₂ w₃ : Eq.{w + 1} (α := L k) 0 0
⊢ ⁅(((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k,
      (((of L j : (a : L j) → ⨁ (i : ι), L i) y : ⨁ (i : ι), L i) : (a : ι) → L a) k⁆ =
    (0 : (a : ι) → L a) k

Tactic:
rw [of_eq_of_ne _ _ _ hik, zero_lie, zero_apply]

Premises used: zero_lie, DirectSum.zero_apply, DirectSum.of_eq_of_ne
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
x : L i
y : L j
inl :
  ∀ (y : L i),
    Eq (α := ⨁ (i : ι), L i)
      (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
          ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
        ⨁ (i : ι), L i)
      (if hij : i = i then
          (of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ L x) ⋯ y⁆
        else 0 :
        ⨁ (i : ι), L i)
inr :
  ∀ (hij : i ≠ j),
    Eq (α := ⨁ (i : ι), L i)
      (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
          ((of L j : (a : L j) → ⨁ (i : ι), L i) y) :
        ⨁ (i : ι), L i)
      (if hij : i = j then
          (of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ L x) ⋯ y⁆
        else 0 :
        ⨁ (i : ι), L i)
⊢ Eq (α := ⨁ (i : ι), L i)
    (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
        ((of L j : (a : L j) → ⨁ (i : ι), L i) y) :
      ⨁ (i : ι), L i)
    (if hij : i = j then
        (of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ L x) ⋯ y⁆
      else 0 :
      ⨁ (i : ι), L i)

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i : ι
x y : L i
⊢ Eq (α := ⨁ (i : ι), L i)
    (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
        ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
      ⨁ (i : ι), L i)
    (if hij : i = i then
        (of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ L x) ⋯ y⁆
      else 0 :
      ⨁ (i : ι), L i)

Tactic:
simp only [lie_of_same L x y, dif_pos]

Premises used: dif_pos, DirectSum.lie_of_same
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ Eq (α := ⨁ (i : ι), L i)
    (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
        ((of L j : (a : L j) → ⨁ (i : ι), L i) y) :
      ⨁ (i : ι), L i)
    (if hij : i = j then
        (of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ L x) ⋯ y⁆
      else 0 :
      ⨁ (i : ι), L i)

Tactic:
simp only [lie_of_of_ne L hij x y, hij, dite_false]

Premises used: dite_false, DirectSum.lie_of_of_ne
-- 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)
c : R
x y : ⨁ (i : ι), L i
w : ∀ (i : ι), (⁅x, c • y⁆ : (a : ι) → L a) i = (c • ⁅x, y⁆ : (a : ι) → L a) i
⊢ ⁅x, c • y⁆ = c • ⁅x, y⁆

Tactic:
ext
-- 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)
c : R
x y : ⨁ (i : ι), L i
i : ι
⊢ (⁅x, c • y⁆ : (a : ι) → L a) i = (c • ⁅x, y⁆ : (a : ι) → L a) i

Tactic:
simp only [smul_apply, bracket_apply, lie_smul]

Premises used: DirectSum.bracket_apply, lie_smul, DirectSum.smul_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)
j : ι
x y : ⨁ (i : ι), L i
⊢ Eq.{w + 1} (α := L j) ((component R ι L j : (a : ⨁ (i : ι), L i) → L j) ⁅x, y⁆ : L j)
    (Bracket.bracket (L := L j) ((component R ι L j : (a : ⨁ (i : ι), L i) → L j) x : L j)
        ((component R ι L j : (a : ⨁ (i : ι), L i) → L j) y) :
      L j)

Tactic:
simp [component, lapply]

Premises used: DirectSum.component, DFinsupp.lapply
-- 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)
x y : ⨁ (i : ι), L i
h :
  ∀ (i : ι),
    Eq.{w + 1} (α := L i) ((lieAlgebraComponent R ι L i : (a : ⨁ (i : ι), L i) → L i) x : L i)
      ((lieAlgebraComponent R ι L i : (a : ⨁ (i : ι), L i) → L i) y : L i)
⊢ x = y

Tactic:
DFinsupp.ext h

Premises used: DFinsupp.ext, DirectSum
-- 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')
this :
  ∀ (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')
simp :
  Eq (α := L')
    ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L')
        ((((LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x :
                Module.End R (⨁ (i : ι), L i)) :
              (a : ⨁ (i : ι), L i) → ⨁ (i : ι), L i)
            y :
          ⨁ (i : ι), L i) :
      L')
    ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
              ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') x : L') :
            Module.End R L') :
          (a : L') → L')
        ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') y : L') :
      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:
simp only [← LieAlgebra.ad_apply R]

Premises used: LieAlgebra.ad_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 : ⨁ (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 : ι) (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')
rw :
  Eq.{w₁ + 1} (α := L')
    (((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
            (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x :
          (a : ⨁ (i : ι), L i) → L')
        y :
      L')
    (((LieAlgebra.ad R L' : (a : L') → Module.End R 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')
⊢ Eq (α := L')
    ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L')
        ((((LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x :
                Module.End R (⨁ (i : ι), L i)) :
              (a : ⨁ (i : ι), L i) → ⨁ (i : ι), L i)
            y :
          ⨁ (i : ι), L i) :
      L')
    ((((LieAlgebra.ad R L' : (a : L') → Module.End R L')
              ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') x : L') :
            Module.End R L') :
          (a : L') → L')
        ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L') : (a : ⨁ (i : ι), L i) → L') y : 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 : ⨁ (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 : ι) (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')
e_a :
  Eq (α := (⨁ (i : ι), L i) →ₗ[R] L')
    ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
      (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x)
    ((LieAlgebra.ad R L' : (a : L') → Module.End R 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'))
⊢ Eq.{w₁ + 1} (α := L')
    (((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
            (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x :
          (a : ⨁ (i : ι), L i) → L')
        y :
      L')
    (((LieAlgebra.ad R L' : (a : L') → Module.End R 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:
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')
x : ⨁ (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 : ι) (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')
e_a :
  ∀ (i : ι) (y : L i),
    Eq.{w₁ + 1} (α := L')
      (((((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
                  (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x) ∘ₗ
                lof R ι L i :
              LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L') :
            (a : L i) → L')
          y :
        L')
      (((((LieAlgebra.ad R L' : (a : L') → Module.End R 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')) ∘ₗ
                lof R ι L i :
              LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L') :
            (a : L i) → L')
          y :
        L')
⊢ Eq (α := (⨁ (i : ι), L i) →ₗ[R] L')
    ((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
      (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x)
    ((LieAlgebra.ad R L' : (a : L') → Module.End R 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'))

Tactic:
ext 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 : ⨁ (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 : ι) (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')
i : ι
y : L i
⊢ Eq.{w₁ + 1} (α := L')
    (((((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
                (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x) ∘ₗ
              lof R ι L i :
            LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L') :
          (a : L i) → L')
        y :
      L')
    (((((LieAlgebra.ad R L' : (a : L') → Module.End R 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')) ∘ₗ
              lof R ι L i :
            LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L') :
          (a : L i) → L')
        y :
      L')

Tactic:
this i y

Premises used: 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')
x : ⨁ (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 : ι) (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')
i : ι
y : L i
⊢ Eq.{w₁ + 1} (α := L')
    (((((toModule R ι (M := L) L' fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')) ∘ₗ
                (LieAlgebra.ad R (⨁ (i : ι), L i) : (a : ⨁ (i : ι), L i) → Module.End R (⨁ (i : ι), L i)) x) ∘ₗ
              lof R ι L i :
            LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L') :
          (a : L i) → L')
        y :
      L')
    (((((LieAlgebra.ad R L' : (a : L') → Module.End R 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')) ∘ₗ
              lof R ι L i :
            LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L') :
          (a : L i) → L')
        y :
      L')

Tactic:
exact this i y