[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑⁅x + y, m⁆ x✝ = ↑(⁅x, m⁆ + ⁅y, m⁆) x✝
[PROOFSTEP]
simp only [mapRange_apply, add_apply, add_lie]
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x : L
m n : ⨁ (i : ι), M i
⊢ ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x : L
m n : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑⁅x, m + n⁆ x✝ = ↑(⁅x, m⁆ + ⁅x, n⁆) x✝
[PROOFSTEP]
simp only [mapRange_apply, add_apply, lie_add]
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑⁅x, ⁅y, m⁆⁆ x✝ = ↑(⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆) x✝
[PROOFSTEP]
simp only [mapRange_apply, lie_lie, add_apply, sub_add_cancel]
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext i`
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑⁅t • x, m⁆ x✝ = ↑(t • ⁅x, m⁆) x✝
[PROOFSTEP]
simp only [smul_lie, lie_module_bracket_apply, smul_apply]
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext i`
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑⁅x, t • m⁆ x✝ = ↑(t • ⁅x, m⁆) x✝
[PROOFSTEP]
simp only [lie_smul, lie_module_bracket_apply, smul_apply]
[GOAL]
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
src✝ : M j →ₗ[R] ⨁ (i : ι), M i := lof R ι M j
x : L
m : M j
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M j),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, m⁆ =
    ⁅x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M j),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        m⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun i =>
    _
      -- Porting note: Originally `ext i`
[GOAL]
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
src✝ : M j →ₗ[R] ⨁ (i : ι), M i := lof R ι M j
x : L
m : M j
i : ι
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : M j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, m⁆)
      i =
    ↑⁅x,
          AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : M j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            m⁆
      i
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
src✝ : M j →ₗ[R] ⨁ (i : ι), M i := lof R ι M j
x : L
m : M j
i : ι
h : j = i
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : M j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, m⁆)
      i =
    ↑⁅x,
          AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : M j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            m⁆
      i
[PROOFSTEP]
rw [← h]
[GOAL]
case pos
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
src✝ : M j →ₗ[R] ⨁ (i : ι), M i := lof R ι M j
x : L
m : M j
i : ι
h : j = i
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : M j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, m⁆)
      j =
    ↑⁅x,
          AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : M j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            m⁆
      j
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
src✝ : M j →ₗ[R] ⨁ (i : ι), M i := lof R ι M j
x : L
m : M j
i : ι
h : ¬j = i
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : M j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, m⁆)
      i =
    ↑⁅x,
          AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : M j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            m⁆
      i
[PROOFSTEP]
simp [lof, lsingle, h]
[GOAL]
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
j : ι
src✝ : (⨁ (i : ι), M i) →ₗ[R] M j := component R ι M j
x : L
m : ⨁ (i : ι), M i
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨁ (i : ι), M i),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, m⁆ =
    ⁅x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), M i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        m⁆
[PROOFSTEP]
simp [component, lapply]
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
x✝ : ι
⊢ ↑⁅x + y, z⁆ x✝ = ↑(⁅x, z⁆ + ⁅y, z⁆) x✝
[PROOFSTEP]
simp only [zipWith_apply, add_apply, add_lie]
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
x✝ : ι
⊢ ↑⁅x, y + z⁆ x✝ = ↑(⁅x, y⁆ + ⁅x, z⁆) x✝
[PROOFSTEP]
simp only [zipWith_apply, add_apply, lie_add]
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x : ⨁ (i : ι), L i
⊢ ⁅x, x⁆ = 0
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x : ⨁ (i : ι), L i
x✝ : ι
⊢ ↑⁅x, x⁆ x✝ = ↑0 x✝
[PROOFSTEP]
simp only [zipWith_apply, add_apply, lie_self, zero_apply]
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
x✝ : ι
⊢ ↑⁅x, ⁅y, z⁆⁆ x✝ = ↑(⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆) x✝
[PROOFSTEP]
simp only [sub_apply, zipWith_apply, add_apply, zero_apply]
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : AddCommGroup (⨁ (i : ι), L i) := inferInstance
x y z : ⨁ (i : ι), L i
x✝ : ι
⊢ ⁅↑x x✝, ⁅↑y x✝, ↑z x✝⁆⁆ = ⁅⁅↑x x✝, ↑y x✝⁆, ↑z x✝⁆ + ⁅↑y x✝, ⁅↑x x✝, ↑z x✝⁆⁆
[PROOFSTEP]
apply leibniz_lie
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : Module R (⨁ (i : ι), L i) := inferInstance
c : R
x y : ⨁ (i : ι), L i
⊢ ⁅x, c • y⁆ = c • ⁅x, y⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun _ =>
    _
      -- Porting note: Originally `ext`
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
src✝ : Module R (⨁ (i : ι), L i) := inferInstance
c : R
x y : ⨁ (i : ι), L i
x✝ : ι
⊢ ↑⁅x, c • y⁆ x✝ = ↑(c • ⁅x, y⁆) x✝
[PROOFSTEP]
simp only [zipWith_apply, smul_apply, bracket_apply, lie_smul]
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
j : ι
src✝ : L j →ₗ[R] ⨁ (i : ι), L i := lof R ι L j
x y : L j
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(of L j),
              map_add' :=
                (_ :
                  ∀ (x y : L j),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L j),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(of L j),
                map_add' :=
                  (_ :
                    ∀ (x y : L j),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L j),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(of L j),
                map_add' :=
                  (_ :
                    ∀ (x y : L j),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L j),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
refine'
  DFinsupp.ext fun i =>
    _
      -- Porting note: Originally `ext i`
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
j : ι
src✝ : L j →ₗ[R] ⨁ (i : ι), L i := lof R ι L j
x y : L j
i : ι
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(of L j),
                  map_add' :=
                    (_ :
                      ∀ (x y : L j),
                        AddHom.toFun src✝.toAddHom (x + y) =
                          AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, y⁆)
      i =
    ↑⁅AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            x,
          AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            y⁆
      i
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
j : ι
src✝ : L j →ₗ[R] ⨁ (i : ι), L i := lof R ι L j
x y : L j
i : ι
h : j = i
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(of L j),
                  map_add' :=
                    (_ :
                      ∀ (x y : L j),
                        AddHom.toFun src✝.toAddHom (x + y) =
                          AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, y⁆)
      i =
    ↑⁅AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            x,
          AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            y⁆
      i
[PROOFSTEP]
rw [← h]
[GOAL]
case pos
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
j : ι
src✝ : L j →ₗ[R] ⨁ (i : ι), L i := lof R ι L j
x y : L j
i : ι
h : j = i
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(of L j),
                  map_add' :=
                    (_ :
                      ∀ (x y : L j),
                        AddHom.toFun src✝.toAddHom (x + y) =
                          AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, y⁆)
      j =
    ↑⁅AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            x,
          AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            y⁆
      j
[PROOFSTEP]
simp [of, singleAddHom]
[GOAL]
case neg
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
j : ι
src✝ : L j →ₗ[R] ⨁ (i : ι), L i := lof R ι L j
x y : L j
i : ι
h : ¬j = i
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(of L j),
                  map_add' :=
                    (_ :
                      ∀ (x y : L j),
                        AddHom.toFun src✝.toAddHom (x + y) =
                          AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L j),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, y⁆)
      i =
    ↑⁅AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            x,
          AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(of L j),
                    map_add' :=
                      (_ :
                        ∀ (x y : L j),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L j),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            y⁆
      i
[PROOFSTEP]
simp [of, singleAddHom, h]
[GOAL]
R : Type u
ι : Type v
inst✝² : CommRing R
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : (i : ι) → LieAlgebra R (L i)
j : ι
src✝ : (⨁ (i : ι), L i) →ₗ[R] L j := component R ι L j
x y : ⨁ (i : ι), L i
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(component R ι L j),
              map_add' :=
                (_ :
                  ∀ (x y : ⨁ (i : ι), L i),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨁ (i : ι), L i),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(component R ι L j),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(component R ι L j),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
simp [component, lapply]
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = 0
[PROOFSTEP]
apply lieAlgebra_ext R ι L
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
⊢ ∀ (i_1 : ι), ↑(lieAlgebraComponent R ι L i_1) ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(lieAlgebraComponent R ι L i_1) 0
[PROOFSTEP]
intro k
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ↑(lieAlgebraComponent R ι L k) ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(lieAlgebraComponent R ι L k) 0
[PROOFSTEP]
rw [LieHom.map_lie]
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ⁅↑(lieAlgebraComponent R ι L k) (↑(of L i) x), ↑(lieAlgebraComponent R ι L k) (↑(of L j) y)⁆ =
    ↑(lieAlgebraComponent R ι L k) 0
[PROOFSTEP]
simp only [of, singleAddHom, AddMonoidHom.coe_mk, ZeroHom.coe_mk, lieAlgebraComponent_apply, component, lapply,
  LinearMap.coe_mk, AddHom.coe_mk, single_apply, LieHom.map_zero]
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
[PROOFSTEP]
by_cases hik : i = k
[GOAL]
case pos
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
hik : i = k
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
[PROOFSTEP]
simp only [dif_neg, not_false_iff, lie_zero, hik.symm, hij]
[GOAL]
case neg
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
hik : ¬i = k
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
[PROOFSTEP]
simp only [dif_neg, not_false_iff, zero_lie, hik]
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j = i
x : L i
y : L j
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(of L i) ⁅x, Eq.recOn hij y⁆
[PROOFSTEP]
have : of L j y = of L i (hij.recOn y) := Eq.rec (Eq.refl _) hij
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j = i
x : L i
y : L j
this : ↑(of L j) y = ↑(of L i) (Eq.recOn hij y)
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(of L i) ⁅x, Eq.recOn hij y⁆
[PROOFSTEP]
rw [this, ← lieAlgebraOf_apply R ι L i ⁅x, hij.recOn y⁆, LieHom.map_lie, lieAlgebraOf_apply, lieAlgebraOf_apply]
[GOAL]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = if hij : j = i then ↑(lieAlgebraOf R ι L i) ⁅x, Eq.recOn hij y⁆ else 0
[PROOFSTEP]
by_cases hij : j = i
[GOAL]
case pos
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : j = i
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = if hij : j = i then ↑(lieAlgebraOf R ι L i) ⁅x, Eq.recOn hij y⁆ else 0
[PROOFSTEP]
simp only [lie_of_of_eq R ι L hij x y, hij, dif_pos, not_false_iff, lieAlgebraOf_apply]
[GOAL]
case neg
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : ¬j = i
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = if hij : j = i then ↑(lieAlgebraOf R ι L i) ⁅x, Eq.recOn hij y⁆ else 0
[PROOFSTEP]
simp only [lie_of_of_ne R ι L hij x y, hij, dif_neg, not_false_iff]
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
              map_add' :=
                (_ :
                  ∀ (x y : ⨁ (i : ι), L i),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨁ (i : ι), L i),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
let f' i :=
  (f i : L i →ₗ[R] L')
    /- The goal is linear in `y`. We can use this to reduce to the case that `y` has only one
            non-zero component. -/
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
              map_add' :=
                (_ :
                  ∀ (x y : ⨁ (i : ι), L i),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨁ (i : ι), L i),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
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
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
              map_add' :=
                (_ :
                  ∀ (x y : ⨁ (i : ι), L i),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨁ (i : ι), L i),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(toModule R ι L' fun i => ↑(f i)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨁ (i : ι), L i),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨁ (i : ι), L i),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
simp only [← LieAlgebra.ad_apply R]
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
⊢ ↑(toModule R ι L' fun i => ↑(f i)) (↑(↑(LieAlgebra.ad R (⨁ (i : ι), L i)) x) y) =
    ↑(↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) x)) (↑(toModule R ι L' fun i => ↑(f i)) y)
[PROOFSTEP]
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
⊢ ↑(LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) x)) y =
    ↑(LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) x)) (toModule R ι L' fun i => ↑(f i))) y
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
⊢ LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) x) =
    LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) x)) (toModule R ι L' fun i => ↑(f i))
[PROOFSTEP]
clear y
[GOAL]
case e_a
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
⊢ LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) x) =
    LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) x)) (toModule R ι L' fun i => ↑(f i))
[PROOFSTEP]
ext i y
[GOAL]
case e_a.H.h
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
⊢ ↑(LinearMap.comp (LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) x))
          (lof R ι (fun i => L i) i))
      y =
    ↑(LinearMap.comp
          (LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) x))
            (toModule R ι L' fun i => ↑(f i)))
          (lof R ι (fun i => L i) i))
      y
[PROOFSTEP]
exact this i y
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
⊢ ∀ (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)⁆
[PROOFSTEP]
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 [LinearMap.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
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
⊢ ∀ (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)⁆
[PROOFSTEP]
intro i y
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
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)⁆
[PROOFSTEP]
rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
⊢ ↑(toModule R ι L' f') (-⁅↑(of L i) y, x⁆) = -⁅↑(toModule R ι L' f') (↑(of L i) y), ↑(toModule R ι L' f') x⁆
[PROOFSTEP]
simp only [LinearMap.map_neg, neg_inj, ← LieAlgebra.ad_apply R]
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
⊢ ↑(toModule R ι L' fun i => ↑(f i)) (↑(↑(LieAlgebra.ad R (⨁ (i : ι), L i)) (↑(of L i) y)) x) =
    ↑(↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) (↑(of L i) y))) (↑(toModule R ι L' fun i => ↑(f i)) x)
[PROOFSTEP]
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
⊢ ↑(LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) (↑(of L i) y))) x =
    ↑(LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) (↑(of L i) y)))
          (toModule R ι L' fun i => ↑(f i)))
      x
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
⊢ LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) (↑(of L i) y)) =
    LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) (↑(of L i) y)))
      (toModule R ι L' fun i => ↑(f i))
[PROOFSTEP]
clear x
[GOAL]
case e_a
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
⊢ LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) (↑(of L i) y)) =
    LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) (↑(of L i) y)))
      (toModule R ι L' fun i => ↑(f i))
[PROOFSTEP]
ext j x
[GOAL]
case e_a.H.h
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
this :
  ∀ (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)⁆
i : ι
y : L i
j : ι
x : L j
⊢ ↑(LinearMap.comp
          (LinearMap.comp (toModule R ι L' fun i => ↑(f i)) (↑(LieAlgebra.ad R (⨁ (i : ι), L i)) (↑(of L i) y)))
          (lof R ι (fun i => L i) j))
      x =
    ↑(LinearMap.comp
          (LinearMap.comp (↑(LieAlgebra.ad R L') (↑(toModule R ι L' fun i => ↑(f i)) (↑(of L i) y)))
            (toModule R ι L' fun i => ↑(f i)))
          (lof R ι (fun i => L i) j))
      x
[PROOFSTEP]
exact this j i x y
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
⊢ ∀ (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)⁆
[PROOFSTEP]
intro i j y x
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
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)⁆
[PROOFSTEP]
simp only [lie_of R, lieAlgebraOf_apply, LieHom.coe_toLinearMap, toAddMonoid_of, coe_toModule_eq_coe_toAddMonoid,
  LinearMap.toAddMonoidHom_coe]
  -- And finish with trivial case analysis.
[GOAL]
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
i j : ι
y : L i
x : L j
⊢ ↑(toAddMonoid fun i => LinearMap.toAddMonoidHom ↑(f i)) (if h : i = j then ↑(of L j) ⁅x, (_ : i = j) ▸ y⁆ else 0) =
    ⁅↑(f j) x, ↑(f i) y⁆
[PROOFSTEP]
rcases eq_or_ne i j with (h | h)
[GOAL]
case inl
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
i j : ι
y : L i
x : L j
h : i = j
⊢ ↑(toAddMonoid fun i => LinearMap.toAddMonoidHom ↑(f i)) (if h : i = j then ↑(of L j) ⁅x, (_ : i = j) ▸ y⁆ else 0) =
    ⁅↑(f j) x, ↑(f i) y⁆
[PROOFSTEP]
have h' : f j (h.recOn y) = f i y := Eq.rec (Eq.refl _) h
[GOAL]
case inl
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
i j : ι
y : L i
x : L j
h : i = j
h' : ↑(f j) (Eq.recOn h y) = ↑(f i) y
⊢ ↑(toAddMonoid fun i => LinearMap.toAddMonoidHom ↑(f i)) (if h : i = j then ↑(of L j) ⁅x, (_ : i = j) ▸ y⁆ else 0) =
    ⁅↑(f j) x, ↑(f i) y⁆
[PROOFSTEP]
simp only [h, h', LieHom.coe_toLinearMap, dif_pos, LieHom.map_lie, toAddMonoid_of, LinearMap.toAddMonoidHom_coe]
[GOAL]
case inr
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0
src✝ : (⨁ (i : ι), L i) →ₗ[R] L' := toModule R ι L' fun i => ↑(f i)
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i => ↑(f i)
i j : ι
y : L i
x : L j
h : i ≠ j
⊢ ↑(toAddMonoid fun i => LinearMap.toAddMonoidHom ↑(f i)) (if h : i = j then ↑(of L j) ⁅x, (_ : i = j) ▸ y⁆ else 0) =
    ⁅↑(f j) x, ↑(f i) y⁆
[PROOFSTEP]
simp only [h, hf j i h.symm x y, dif_neg, not_false_iff, AddMonoidHom.map_zero]
