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

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
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
by_cases hij : j = i
no goals
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
simp only [lie_of_of_eq R ι L hij x y, hij, dif_pos, not_false_iff, lieAlgebraOf_apply]
no goals
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
simp only [lie_of_of_ne R ι L hij x y, hij, dif_neg, not_false_iff]