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⁆
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⁆
have : of L j y = of L i (hij.recOn y) := Eq.rec (Eq.refl _) hij
no goals
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⁆
rw [this, ← lieAlgebraOf_apply R ι L i ⁅x, hij.recOn y⁆, LieHom.map_lie, lieAlgebraOf_apply,
  lieAlgebraOf_apply]