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₁
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) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
have 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
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
have neg : ((({ toFun := single (β := M) j, map_add' := sorry : 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' := sorry } : (a : M j) → ⨁ (i : ι), M i) m : ⨁ (i : ι), M i) : (a : ι) → M a)
      i⁆
Tactic: simp only [lof, lsingle, AddHom.toFun_eq_coe, lie_module_bracket_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ((({ 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⁆
have neg : (single (β := M) j ⁅x, m⁆ : (a : ι) → M a) i = ⁅x, (single (β := M) j m : (a : ι) → M a) i⁆
Tactic: erw [AddHom.coe_mk]
-- 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)
x y z : ⨁ (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) 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)
have 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⁆) sorry (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⁆) sorry 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⁆) sorry y z) :
        (a : ι) → L a)
      i
Tactic: ext
-- 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)
x y z : ⨁ (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 + 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)
have 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⁆) sorry 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⁆) sorry 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⁆) sorry x z) :
        (a : ι) → L a)
      i
Tactic: ext
-- 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)
x : ⨁ (i : ι), L 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
have 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⁆) sorry x x :
        (a : ι) → L a)
      i =
    (0 : (a : ι) → L a) i
Tactic: ext
-- 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)
x y z : ⨁ (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
      (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))
have 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⁆) sorry x
          (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
            (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) sorry 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⁆) sorry
            (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
              (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) sorry 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⁆) sorry y
            (zipWith (β := fun (i : ι) ↦ L i) (β₁ := fun (i : ι) ↦ L i) (β₂ := fun (i : ι) ↦ L i)
              (fun (x : ι) (x_1 y : L x) ↦ ⁅x_1, y⁆) sorry x z)) :
        (a : ι) → L a)
      i
Tactic: ext
-- 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)
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
          (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
have 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⁆⁆
Tactic: simp only [zipWith_apply, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ 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)
have 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
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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 : ι
⊢ ((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
have 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
Tactic: rw [bracket_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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 : ι
⊢ ⁅(((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
have 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
Tactic: obtain rfl | hik := Decidable.eq_or_ne k i
Cleared hypotheses: i, hij, x
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have 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
Tactic: obtain rfl | hik := Decidable.eq_or_ne k i
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have w : ⁅(((of L k : (a : L k) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i) : (a : ι) → L a) k, 0⁆ = (0 : (a : ι) → L a) k
Tactic: rw [of_eq_of_ne _ _ _ hij, lie_zero, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have w₁ : 0 = (0 : (a : ι) → L a) k
Tactic: rw [of_eq_of_ne _ _ _ hij, lie_zero, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have w₂ : Eq.{w + 1} (α := L k) 0 0
Tactic: rw [of_eq_of_ne _ _ _ hij, lie_zero, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have 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
Tactic: rw [of_eq_of_ne _ _ _ hik, zero_lie, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have w₁ : 0 = (0 : (a : ι) → L a) k
Tactic: rw [of_eq_of_ne _ _ _ hik, zero_lie, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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
⊢ ⁅(((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
have w₂ : Eq.{w + 1} (α := L k) 0 0
Tactic: rw [of_eq_of_ne _ _ _ hik, zero_lie, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
ι : Type v
L : ι → Type w
inst : (i : ι) → LieRing (L i)
inst_1 : DecidableEq ι
i j : ι
x : L i
y : L 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)
have 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) sorry y⁆
      else 0 :
      ⨁ (i : ι), L i)
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j, y
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
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)
⊢ 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)
have 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) sorry y⁆
      else 0 :
      ⨁ (i : ι), L i)
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- 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)
c : R
x y : ⨁ (i : ι), L i
⊢ ⁅x, c • y⁆ = c • ⁅x, y⁆
have w : ∀ (i : ι), (⁅x, c • y⁆ : (a : ι) → L a) i = (c • ⁅x, y⁆ : (a : ι) → L a) i
Tactic: ext
-- 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') : (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 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')
Tactic: simp only [← 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 : ⨁ (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 (α := 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')
have 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')
Tactic: rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]