awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ Membership.mem (γ := LieSubalgebra R (LieDerivation R L L)) ⊤ D

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ Membership.mem (γ := LieSubalgebra R (LieDerivation R L L)) ⊤ D

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x y : L
m : ⨁ (i : ι), M i
w :
  ∀ (i : ι),
    (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x + y, m'⁆) ⋯ m : (a : ι) → M a) i =
      (HAdd.hAdd (α := ⨁ (i : ι), M i)
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m) :
          (a : ι) → M a)
        i
⊢ mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x + y, m'⁆) ⋯ m =
    HAdd.hAdd (α := ⨁ (i : ι), M i)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x y : L
m : ⨁ (i : ι), M i
i : ι
⊢ (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x + y, m'⁆) ⋯ m : (a : ι) → M a) i =
    (HAdd.hAdd (α := ⨁ (i : ι), M i)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m) :
        (a : ι) → M a)
      i

Tactic:
simp only [mapRange_apply, add_apply, add_lie]

Premises used: DFinsupp.mapRange_apply, DirectSum.add_apply, add_lie
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x : L
m n : ⨁ (i : ι), M i
w :
  ∀ (i : ι),
    (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ (m + n) : (a : ι) → M a) i =
      (HAdd.hAdd (α := ⨁ (i : ι), M i)
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ n) :
          (a : ι) → M a)
        i
⊢ mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ (m + n) =
    HAdd.hAdd (α := ⨁ (i : ι), M i)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ n)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x : L
m n : ⨁ (i : ι), M i
i : ι
⊢ (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ (m + n) : (a : ι) → M a) i =
    (HAdd.hAdd (α := ⨁ (i : ι), M i)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ n) :
        (a : ι) → M a)
      i

Tactic:
simp only [mapRange_apply, add_apply, lie_add]

Premises used: DFinsupp.mapRange_apply, DirectSum.add_apply, lie_add
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x y : L
m : ⨁ (i : ι), M i
w :
  ∀ (i : ι),
    (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m) :
          (a : ι) → M a)
        i =
      (HAdd.hAdd (α := ⨁ (i : ι), M i)
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅⁅x, y⁆, m'⁆) ⋯ m)
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯
              (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)) :
          (a : ι) → M a)
        i
⊢ mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m) =
    HAdd.hAdd (α := ⨁ (i : ι), M i)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅⁅x, y⁆, m'⁆) ⋯ m)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯
        (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x y : L
m : ⨁ (i : ι), M i
i : ι
⊢ (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m) :
        (a : ι) → M a)
      i =
    (HAdd.hAdd (α := ⨁ (i : ι), M i)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅⁅x, y⁆, m'⁆) ⋯ m)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)) :
        (a : ι) → M a)
      i

Tactic:
simp only [mapRange_apply, lie_lie, add_apply, sub_add_cancel]

Premises used: DFinsupp.mapRange_apply, sub_add_cancel, lie_lie, DirectSum.add_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
ι : Type v
L : Type w₁
M : ι → Type w
inst : LieRing L
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → LieRingModule.{w₁, w} L (M i)
x : L
m : ⨁ (i : ι), M i
i : ι
⊢ (⁅x, m⁆ : (a : ι) → M a) i = ⁅x, (m : (a : ι) → M a) i⁆

Tactic:
mapRange_apply _ _ m i

Premises used: DFinsupp.mapRange_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
w : ∀ (i : ι), (⁅t • x, m⁆ : (a : ι) → M a) i = (t • ⁅x, m⁆ : (a : ι) → M a) i
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
i : ι
⊢ (⁅t • x, m⁆ : (a : ι) → M a) i = (t • ⁅x, m⁆ : (a : ι) → M a) i

Tactic:
simp only [smul_lie, lie_module_bracket_apply, smul_apply]

Premises used: DirectSum.lie_module_bracket_apply, smul_lie, DirectSum.smul_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
w : ∀ (i : ι), (⁅x, t • m⁆ : (a : ι) → M a) i = (t • ⁅x, m⁆ : (a : ι) → M a) i
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
i : ι
⊢ (⁅x, t • m⁆ : (a : ι) → M a) i = (t • ⁅x, m⁆ : (a : ι) → M a) i

Tactic:
simp only [lie_smul, lie_module_bracket_apply, smul_apply]

Premises used: DirectSum.lie_module_bracket_apply, lie_smul, DirectSum.smul_apply
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
w :
  ∀ (i : ι),
    (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
      (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
⊢ Eq (α := ⨁ (i : ι), M i) (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆)
    ⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆

Tactic:
ext i
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
pos :
  ∀ (h : j = i),
    (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
      (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
neg :
  ∀ (h : ¬j = i),
    (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
      (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
⊢ (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i

Tactic:
by_cases h : j = i
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : j = i
pos :
  (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) j =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) j
⊢ (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : j = i
⊢ (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) j =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) j

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
neg :
  ((({ toFun := single (β := M) j, map_add' := ⋯ : M j →ₙ+ Π₀ (i : ι), M i } : (a : M j) → ⨁ (i : ι), M i) ⁅x, m⁆ :
          ⨁ (i : ι), M i) :
        (a : ι) → M a)
      i =
    ⁅x,
      ((({ toFun := single (β := M) j, map_add' := ⋯ } : (a : M j) → ⨁ (i : ι), M i) m : ⨁ (i : ι), M i) :
          (a : ι) → M a)
        i⁆
⊢ (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i

Tactic:
simp only [lof, lsingle, AddHom.toFun_eq_coe, lie_module_bracket_apply]

Premises used: DirectSum.lie_module_bracket_apply, AddHom.toFun_eq_coe, DirectSum.lof, DFinsupp.lsingle
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
neg : (single (β := M) j ⁅x, m⁆ : (a : ι) → M a) i = ⁅x, (single (β := M) j m : (a : ι) → M a) i⁆
⊢ ((({ toFun := single (β := M) j, map_add' := ⋯ : M j →ₙ+ Π₀ (i : ι), M i } : (a : M j) → ⨁ (i : ι), M i) ⁅x, m⁆ :
          ⨁ (i : ι), M i) :
        (a : ι) → M a)
      i =
    ⁅x,
      ((({ toFun := single (β := M) j, map_add' := ⋯ } : (a : M j) → ⨁ (i : ι), M i) m : ⨁ (i : ι), M i) :
          (a : ι) → M a)
        i⁆

Tactic:
erw [AddHom.coe_mk]

Premises used: AddHom.coe_mk
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ (single (β := M) j ⁅x, m⁆ : (a : ι) → M a) i = ⁅x, (single (β := M) j m : (a : ι) → M a) i⁆

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
j : ι
x : L
m : ⨁ (i : ι), M i
⊢ AddHom.toFun (LinearMap.toAddHom (component R ι M j)) ⁅x, m⁆ =
    ⁅x, AddHom.toFun (LinearMap.toAddHom (component R ι M j)) m⁆

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 z : ⨁ (i : ι), L i
w :
  ∀ (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 + 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⁆) ⋯ x 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 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 + y) z =
    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⁆) ⋯ x 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 z)

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)
x y z : ⨁ (i : ι), L i
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 + 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⁆) ⋯ x 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 z) :
        (a : ι) → L a)
      i

Tactic:
simp only [zipWith_apply, add_apply, add_lie]

Premises used: DFinsupp.zipWith_apply, DirectSum.add_apply, add_lie
-- 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
w :
  ∀ (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 (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⁆) ⋯ x 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
⊢ 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) =
    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⁆) ⋯ x 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)

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)
x y z : ⨁ (i : ι), L i
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 (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⁆) ⋯ x 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, lie_add]

Premises used: DFinsupp.zipWith_apply, DirectSum.add_apply, lie_add
-- 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 : ⨁ (i : ι), L i
w :
  ∀ (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 x :
          (a : ι) → L a)
        i =
      (0 : (a : ι) → L a) i
⊢ Eq (α := ⨁ (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⁆) ⋯ x x)
    0

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)
x : ⨁ (i : ι), L i
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 x :
        (a : ι) → L a)
      i =
    (0 : (a : ι) → L a) i

Tactic:
simp only [zipWith_apply, lie_self, zero_apply]

Premises used: lie_self, DFinsupp.zipWith_apply, DirectSum.zero_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
w :
  ∀ (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
⊢ 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) =
    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))

Tactic:
ext