[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]


[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
⊢ AddHom.toFun src✝.toAddHom ⁅T, S⁆ = ⁅AddHom.toFun src✝.toAddHom T, AddHom.toFun src✝.toAddHom S⁆
[PROOFSTEP]
let f := @LinearMap.toMatrix' R _ n n _ _
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ AddHom.toFun src✝.toAddHom ⁅T, S⁆ = ⁅AddHom.toFun src✝.toAddHom T, AddHom.toFun src✝.toAddHom S⁆
[PROOFSTEP]
change f (T.comp S - S.comp T) = f T * f S - f S * f T
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ ↑f (LinearMap.comp T S - LinearMap.comp S T) = ↑f T * ↑f S - ↑f S * ↑f T
[PROOFSTEP]
have h : ∀ T S : Module.End R _, f (T.comp S) = f T * f S := LinearMap.toMatrix'_comp
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h : ∀ (T S : Module.End R (n → R)), ↑f (LinearMap.comp T S) = ↑f T * ↑f S
⊢ ↑f (LinearMap.comp T S - LinearMap.comp S T) = ↑f T * ↑f S - ↑f S * ↑f T
[PROOFSTEP]
rw [LinearEquiv.map_sub, h, h]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ ↑(lieConj P h) A = P * A * P⁻¹
[PROOFSTEP]
simp [LinearEquiv.conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp, LinearMap.toMatrix'_toLin']
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ ↑(LieEquiv.symm (lieConj P h)) A = P⁻¹ * A * P
[PROOFSTEP]
simp [LinearEquiv.symm_conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp, LinearMap.toMatrix'_toLin']
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type w₁
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
src✝ : Matrix n n R ≃ₗ[R] Matrix m m R := reindexLinearEquiv R R e e
x✝¹ x✝ : Matrix n n R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(reindex e e),
              map_add' :=
                (_ :
                  ∀ (x y : Matrix n n R),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : Matrix n n R),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x✝¹, x✝⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(reindex e e),
                map_add' :=
                  (_ :
                    ∀ (x y : Matrix n n R),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : Matrix n n R),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x✝¹,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(reindex e e),
                map_add' :=
                  (_ :
                    ∀ (x y : Matrix n n R),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : Matrix n n R),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x✝⁆
[PROOFSTEP]
simp only [LieRing.of_associative_ring_bracket, Matrix.reindex_apply, Matrix.submatrix_mul_equiv, Matrix.submatrix_sub,
  Pi.sub_apply]


[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ (m.fst - 1, m.snd) ∈ Finset.erase b m
[PROOFSTEP]
rw [mem_right] at h
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst - 1, m.snd) ∈ b
⊢ (m.fst - 1, m.snd) ∈ Finset.erase b m
[PROOFSTEP]
apply Finset.mem_erase_of_ne_of_mem _ h.2
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst - 1, m.snd) ∈ b
⊢ (m.fst - 1, m.snd) ≠ m
[PROOFSTEP]
exact ne_of_apply_ne Prod.fst (pred_ne_self m.1)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ (m.fst, m.snd - 1) ∈ Finset.erase b m
[PROOFSTEP]
rw [mem_left] at h
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst, m.snd - 1) ∈ b
⊢ (m.fst, m.snd - 1) ∈ Finset.erase b m
[PROOFSTEP]
apply Finset.mem_erase_of_ne_of_mem _ h.2
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst, m.snd - 1) ∈ b
⊢ (m.fst, m.snd - 1) ≠ m
[PROOFSTEP]
exact ne_of_apply_ne Prod.snd (pred_ne_self m.2)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₂ : (m.1, m.2 - 1) ∈ b.erase m := snd_pred_mem_erase_of_mem_left h
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.fst, m.snd - 1) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₁ := Finset.card_erase_lt_of_mem w₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.fst, m.snd - 1) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.fst, m.snd - 1) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
i₂ : 0 < Finset.card (Finset.erase b m)
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
exact Nat.lt_of_le_of_lt i₂ i₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₂ := fst_pred_mem_erase_of_mem_right h
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.fst - 1, m.snd) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₁ := Finset.card_erase_lt_of_mem w₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.fst - 1, m.snd) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.fst - 1, m.snd) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
i₂ : 0 < Finset.card (Finset.erase b m)
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
exact Nat.lt_of_le_of_lt i₂ i₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (moveLeft b m) + 2 = Finset.card b
[PROOFSTEP]
dsimp [moveLeft]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (Finset.erase (Finset.erase b m) (m.fst, m.snd - 1)) + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (snd_pred_mem_erase_of_mem_left h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (Finset.erase b m) - 1 + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b
[PROOFSTEP]
exact tsub_add_cancel_of_le (card_of_mem_left h)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (moveRight b m) + 2 = Finset.card b
[PROOFSTEP]
dsimp [moveRight]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (Finset.erase (Finset.erase b m) (m.fst - 1, m.snd)) + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (fst_pred_mem_erase_of_mem_right h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (Finset.erase b m) - 1 + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b
[PROOFSTEP]
exact tsub_add_cancel_of_le (card_of_mem_right h)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (moveLeft b m) / 2 < Finset.card b / 2
[PROOFSTEP]
simp [← moveLeft_card h, lt_add_one]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (moveRight b m) / 2 < Finset.card b / 2
[PROOFSTEP]
simp [← moveRight_card h, lt_add_one]
[GOAL]
s✝ t✝ : Board
m : t✝ ∈ (fun s => Finset.image (moveLeft s) (left s)) s✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
simp only [Finset.mem_image, Prod.exists] at m
[GOAL]
s✝ t✝ : Board
m : ∃ a b, (a, b) ∈ left s✝ ∧ moveLeft s✝ (a, b) = t✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
rcases m with ⟨_, _, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro.intro
s✝ : Board
w✝¹ w✝ : ℤ
h : (w✝¹, w✝) ∈ left s✝
⊢ (fun s => Finset.card s / 2) (moveLeft s✝ (w✝¹, w✝)) < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
exact moveLeft_smaller h
[GOAL]
s✝ t✝ : Board
m : t✝ ∈ (fun s => Finset.image (moveRight s) (right s)) s✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
simp only [Finset.mem_image, Prod.exists] at m
[GOAL]
s✝ t✝ : Board
m : ∃ a b, (a, b) ∈ right s✝ ∧ moveRight s✝ (a, b) = t✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
rcases m with ⟨_, _, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro.intro
s✝ : Board
w✝¹ w✝ : ℤ
h : (w✝¹, w✝) ∈ right s✝
⊢ (fun s => Finset.card s / 2) (moveRight s✝ (w✝¹, w✝)) < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
exact moveRight_smaller h
[GOAL]
b : Domineering.Board
⊢ Short (domineering b)
[PROOFSTEP]
dsimp [domineering]
[GOAL]
b : Domineering.Board
⊢ Short (ofState b)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short domineering.one
[PROOFSTEP]
dsimp [domineering.one]
[GOAL]
⊢ Short (domineering (List.toFinset [(0, 0), (0, 1)]))
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short domineering.L
[PROOFSTEP]
dsimp [domineering.L]
[GOAL]
⊢ Short (domineering (List.toFinset [(0, 2), (0, 1), (0, 0), (1, 0)]))
[PROOFSTEP]
infer_instance