awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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')
⊢ 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')
have 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'))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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')
⊢ 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'))
have 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')
Tactic: ext i y
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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')
⊢ 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')
have 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')
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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')
have 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')
Tactic: rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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')
have 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')
Tactic: simp only [map_neg, neg_inj, ← LieAlgebra.ad_apply R]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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')
have 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')
Tactic: rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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')
have 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'
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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'
have 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')
Tactic: ext j x
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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')
⊢ ∀ (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')
have 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')
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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')
have 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')
Tactic: simp only [f', coe_toModule_eq_coe_toAddMonoid, toAddMonoid_of]