[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝² + x✝¹, x✝⁆ = ⁅x✝², x✝⁆ + ⁅x✝¹, x✝⁆
[PROOFSTEP]
simp only [Ring.lie_def, right_distrib, left_distrib]
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝ + x✝¹ * x✝ - (x✝ * x✝² + x✝ * x✝¹) = x✝² * x✝ - x✝ * x✝² + (x✝¹ * x✝ - x✝ * x✝¹)
[PROOFSTEP]
abel
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝ + x✝¹ * x✝ - (x✝ * x✝² + x✝ * x✝¹) = x✝² * x✝ - x✝ * x✝² + (x✝¹ * x✝ - x✝ * x✝¹)
[PROOFSTEP]
abel
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝², x✝¹ + x✝⁆ = ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆
[PROOFSTEP]
simp only [Ring.lie_def, right_distrib, left_distrib]
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝¹ + x✝² * x✝ - (x✝¹ * x✝² + x✝ * x✝²) = x✝² * x✝¹ - x✝¹ * x✝² + (x✝² * x✝ - x✝ * x✝²)
[PROOFSTEP]
abel
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝¹ + x✝² * x✝ - (x✝¹ * x✝² + x✝ * x✝²) = x✝² * x✝¹ - x✝¹ * x✝² + (x✝² * x✝ - x✝ * x✝²)
[PROOFSTEP]
abel
[GOAL]
A : Type v
inst✝ : Ring A
⊢ ∀ (x : A), ⁅x, x⁆ = 0
[PROOFSTEP]
simp only [Ring.lie_def, forall_const, sub_self]
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝², ⁅x✝¹, x✝⁆⁆ = ⁅⁅x✝², x✝¹⁆, x✝⁆ + ⁅x✝¹, ⁅x✝², x✝⁆⁆
[PROOFSTEP]
simp only [Ring.lie_def, mul_sub_left_distrib, mul_sub_right_distrib, mul_assoc]
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * (x✝¹ * x✝) - x✝² * (x✝ * x✝¹) - (x✝¹ * (x✝ * x✝²) - x✝ * (x✝¹ * x✝²)) =
    x✝² * (x✝¹ * x✝) - x✝¹ * (x✝² * x✝) - (x✝ * (x✝² * x✝¹) - x✝ * (x✝¹ * x✝²)) +
      (x✝¹ * (x✝² * x✝) - x✝¹ * (x✝ * x✝²) - (x✝² * (x✝ * x✝¹) - x✝ * (x✝² * x✝¹)))
[PROOFSTEP]
abel
[GOAL]
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * (x✝¹ * x✝) - x✝² * (x✝ * x✝¹) - (x✝¹ * (x✝ * x✝²) - x✝ * (x✝¹ * x✝²)) =
    x✝² * (x✝¹ * x✝) - x✝¹ * (x✝² * x✝) - (x✝ * (x✝² * x✝¹) - x✝ * (x✝¹ * x✝²)) +
      (x✝¹ * (x✝² * x✝) - x✝¹ * (x✝ * x✝²) - (x✝² * (x✝ * x✝¹) - x✝ * (x✝² * x✝¹)))
[PROOFSTEP]
abel
[GOAL]
A : Type v
inst✝² : Ring A
M : Type w
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ ∀ (x y : A) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
[PROOFSTEP]
simp [LieRing.of_associative_ring_bracket, sub_smul, mul_smul, sub_add_cancel]
[GOAL]
A : Type v
inst✝² : Ring A
R : Type u
inst✝¹ : CommRing R
inst✝ : Algebra R A
t : R
x y : A
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket, Algebra.mul_smul_comm,
  Algebra.smul_mul_assoc, smul_sub]
[GOAL]
A : Type v
inst✝⁶ : Ring A
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R A
B : Type w
C : Type w₁
inst✝³ : Ring B
inst✝² : Ring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
src✝ : A →ₗ[R] B := toLinearMap f
x✝¹ x✝ : A
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x✝¹, x✝⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x✝¹,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x✝⁆
[PROOFSTEP]
simp [LieRing.of_associative_ring_bracket]
[GOAL]
A : Type v
inst✝⁶ : Ring A
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R A
B : Type w
C : Type w₁
inst✝³ : Ring B
inst✝² : Ring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f✝ : A →ₐ[R] B
g✝ : B →ₐ[R] C
f g : A →ₐ[R] B
h : toLieHom f = toLieHom g
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case H
A : Type v
inst✝⁶ : Ring A
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R A
B : Type w
C : Type w₁
inst✝³ : Ring B
inst✝² : Ring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f✝ : A →ₐ[R] B
g✝ : B →ₐ[R] C
f g : A →ₐ[R] B
h : toLieHom f = toLieHom g
a : A
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact LieHom.congr_fun h a
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
⊢ (fun x =>
        { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
      (x + y) =
    (fun x =>
          { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
        x +
      (fun x =>
          { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
        y
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
m : M
⊢ ↑((fun x =>
            { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
          (x + y))
      m =
    ↑((fun x =>
              { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
            x +
          (fun x =>
              { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
            y)
      m
[PROOFSTEP]
apply add_lie
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
⊢ AddHom.toFun
      {
        toFun := fun x =>
          { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
        map_add' :=
          (_ :
            ∀ (x y : L),
              (fun x =>
                    {
                      toAddHom :=
                        { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                  (x + y) =
                (fun x =>
                      {
                        toAddHom :=
                          { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                    x +
                  (fun x =>
                      {
                        toAddHom :=
                          { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                    y) }
      (t • x) =
    ↑(RingHom.id R) t •
      AddHom.toFun
        {
          toFun := fun x =>
            { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
          map_add' :=
            (_ :
              ∀ (x y : L),
                (fun x =>
                      {
                        toAddHom :=
                          { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                    (x + y) =
                  (fun x =>
                        {
                          toAddHom :=
                            { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                      x +
                    (fun x =>
                        {
                          toAddHom :=
                            { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                      y) }
        x
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
m : M
⊢ ↑(AddHom.toFun
          {
            toFun := fun x =>
              { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
            map_add' :=
              (_ :
                ∀ (x y : L),
                  (fun x =>
                        {
                          toAddHom :=
                            { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                      (x + y) =
                    (fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                        x +
                      (fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                        y) }
          (t • x))
      m =
    ↑(↑(RingHom.id R) t •
          AddHom.toFun
            {
              toFun := fun x =>
                { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
              map_add' :=
                (_ :
                  ∀ (x y : L),
                    (fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                        (x + y) =
                      (fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                          x +
                        (fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                          y) }
            x)
      m
[PROOFSTEP]
apply smul_lie
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun x =>
                { toAddHom := { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
              map_add' :=
                (_ :
                  ∀ (x y : L),
                    (fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                        (x + y) =
                      (fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                          x +
                        (fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                          y) },
          map_smul' :=
            (_ :
              ∀ (t : R) (x : L),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        {
                          toAddHom :=
                            { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                      map_add' :=
                        (_ :
                          ∀ (x y : L),
                            (fun x =>
                                  {
                                    toAddHom :=
                                      { toFun := fun m => ⁅x, m⁆,
                                        map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                (x + y) =
                              (fun x =>
                                    {
                                      toAddHom :=
                                        { toFun := fun m => ⁅x, m⁆,
                                          map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                  x +
                                (fun x =>
                                    {
                                      toAddHom :=
                                        { toFun := fun m => ⁅x, m⁆,
                                          map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                  y) }
                    (t • x) =
                  ↑(RingHom.id R) t •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                        map_add' :=
                          (_ :
                            ∀ (x y : L),
                              (fun x =>
                                    {
                                      toAddHom :=
                                        { toFun := fun m => ⁅x, m⁆,
                                          map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                  (x + y) =
                                (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    x +
                                  (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    y) }
                      x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun x =>
                  {
                    toAddHom :=
                      { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                map_add' :=
                  (_ :
                    ∀ (x y : L),
                      (fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                          (x + y) =
                        (fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                            x +
                          (fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                            y) },
            map_smul' :=
              (_ :
                ∀ (t : R) (x : L),
                  AddHom.toFun
                      {
                        toFun := fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                        map_add' :=
                          (_ :
                            ∀ (x y : L),
                              (fun x =>
                                    {
                                      toAddHom :=
                                        { toFun := fun m => ⁅x, m⁆,
                                          map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                  (x + y) =
                                (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    x +
                                  (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    y) }
                      (t • x) =
                    ↑(RingHom.id R) t •
                      AddHom.toFun
                        {
                          toFun := fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                          map_add' :=
                            (_ :
                              ∀ (x y : L),
                                (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    (x + y) =
                                  (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      x +
                                    (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      y) }
                        x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun x =>
                  {
                    toAddHom :=
                      { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                map_add' :=
                  (_ :
                    ∀ (x y : L),
                      (fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                          (x + y) =
                        (fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                            x +
                          (fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                            y) },
            map_smul' :=
              (_ :
                ∀ (t : R) (x : L),
                  AddHom.toFun
                      {
                        toFun := fun x =>
                          {
                            toAddHom :=
                              { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                        map_add' :=
                          (_ :
                            ∀ (x y : L),
                              (fun x =>
                                    {
                                      toAddHom :=
                                        { toFun := fun m => ⁅x, m⁆,
                                          map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                  (x + y) =
                                (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    x +
                                  (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    y) }
                      (t • x) =
                    ↑(RingHom.id R) t •
                      AddHom.toFun
                        {
                          toFun := fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                          map_add' :=
                            (_ :
                              ∀ (x y : L),
                                (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    (x + y) =
                                  (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      x +
                                    (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      y) }
                        x) }.toAddHom
        y⁆
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
m : M
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                {
                  toFun := fun x =>
                    {
                      toAddHom :=
                        { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                      map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                  map_add' :=
                    (_ :
                      ∀ (x y : L),
                        (fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                            (x + y) =
                          (fun x =>
                                {
                                  toAddHom :=
                                    { toFun := fun m => ⁅x, m⁆,
                                      map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                              x +
                            (fun x =>
                                {
                                  toAddHom :=
                                    { toFun := fun m => ⁅x, m⁆,
                                      map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                              y) },
              map_smul' :=
                (_ :
                  ∀ (t : R) (x : L),
                    AddHom.toFun
                        {
                          toFun := fun x =>
                            {
                              toAddHom :=
                                { toFun := fun m => ⁅x, m⁆,
                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                          map_add' :=
                            (_ :
                              ∀ (x y : L),
                                (fun x =>
                                      {
                                        toAddHom :=
                                          { toFun := fun m => ⁅x, m⁆,
                                            map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                    (x + y) =
                                  (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      x +
                                    (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      y) }
                        (t • x) =
                      ↑(RingHom.id R) t •
                        AddHom.toFun
                          {
                            toFun := fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                            map_add' :=
                              (_ :
                                ∀ (x y : L),
                                  (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      (x + y) =
                                    (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        x +
                                      (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        y) }
                          x) }.toAddHom
          ⁅x, y⁆)
      m =
    ↑⁅AddHom.toFun
            {
                toAddHom :=
                  {
                    toFun := fun x =>
                      {
                        toAddHom :=
                          { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                    map_add' :=
                      (_ :
                        ∀ (x y : L),
                          (fun x =>
                                {
                                  toAddHom :=
                                    { toFun := fun m => ⁅x, m⁆,
                                      map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                              (x + y) =
                            (fun x =>
                                  {
                                    toAddHom :=
                                      { toFun := fun m => ⁅x, m⁆,
                                        map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                x +
                              (fun x =>
                                  {
                                    toAddHom :=
                                      { toFun := fun m => ⁅x, m⁆,
                                        map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                y) },
                map_smul' :=
                  (_ :
                    ∀ (t : R) (x : L),
                      AddHom.toFun
                          {
                            toFun := fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                            map_add' :=
                              (_ :
                                ∀ (x y : L),
                                  (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      (x + y) =
                                    (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        x +
                                      (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        y) }
                          (t • x) =
                        ↑(RingHom.id R) t •
                          AddHom.toFun
                            {
                              toFun := fun x =>
                                {
                                  toAddHom :=
                                    { toFun := fun m => ⁅x, m⁆,
                                      map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                              map_add' :=
                                (_ :
                                  ∀ (x y : L),
                                    (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        (x + y) =
                                      (fun x =>
                                            {
                                              toAddHom :=
                                                { toFun := fun m => ⁅x, m⁆,
                                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                          x +
                                        (fun x =>
                                            {
                                              toAddHom :=
                                                { toFun := fun m => ⁅x, m⁆,
                                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                          y) }
                            x) }.toAddHom
            x,
          AddHom.toFun
            {
                toAddHom :=
                  {
                    toFun := fun x =>
                      {
                        toAddHom :=
                          { toFun := fun m => ⁅x, m⁆, map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                        map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                    map_add' :=
                      (_ :
                        ∀ (x y : L),
                          (fun x =>
                                {
                                  toAddHom :=
                                    { toFun := fun m => ⁅x, m⁆,
                                      map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                              (x + y) =
                            (fun x =>
                                  {
                                    toAddHom :=
                                      { toFun := fun m => ⁅x, m⁆,
                                        map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                x +
                              (fun x =>
                                  {
                                    toAddHom :=
                                      { toFun := fun m => ⁅x, m⁆,
                                        map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                    map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                y) },
                map_smul' :=
                  (_ :
                    ∀ (t : R) (x : L),
                      AddHom.toFun
                          {
                            toFun := fun x =>
                              {
                                toAddHom :=
                                  { toFun := fun m => ⁅x, m⁆,
                                    map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                            map_add' :=
                              (_ :
                                ∀ (x y : L),
                                  (fun x =>
                                        {
                                          toAddHom :=
                                            { toFun := fun m => ⁅x, m⁆,
                                              map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                          map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                      (x + y) =
                                    (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        x +
                                      (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        y) }
                          (t • x) =
                        ↑(RingHom.id R) t •
                          AddHom.toFun
                            {
                              toFun := fun x =>
                                {
                                  toAddHom :=
                                    { toFun := fun m => ⁅x, m⁆,
                                      map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                  map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) },
                              map_add' :=
                                (_ :
                                  ∀ (x y : L),
                                    (fun x =>
                                          {
                                            toAddHom :=
                                              { toFun := fun m => ⁅x, m⁆,
                                                map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                            map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                        (x + y) =
                                      (fun x =>
                                            {
                                              toAddHom :=
                                                { toFun := fun m => ⁅x, m⁆,
                                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                          x +
                                        (fun x =>
                                            {
                                              toAddHom :=
                                                { toFun := fun m => ⁅x, m⁆,
                                                  map_add' := (_ : ∀ (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆) },
                                              map_smul' := (_ : ∀ (t : R) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆) })
                                          y) }
                            x) }.toAddHom
            y⁆
      m
[PROOFSTEP]
apply lie_lie
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ toEndomorphism R (Module.End R M) M = LieHom.id
[PROOFSTEP]
ext g m
[GOAL]
case h.h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
g : Module.End R M
m : M
⊢ ↑(↑(toEndomorphism R (Module.End R M) M) g) m = ↑(↑LieHom.id g) m
[PROOFSTEP]
simp [lie_eq_smul]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
⊢ Submodule.map (↑(toEndomorphism R L M) x) ↑N ≤ ↑N
[PROOFSTEP]
rintro n ⟨m, hm, rfl⟩
[GOAL]
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑↑N
⊢ ↑(↑(toEndomorphism R L M) x) m ∈ ↑N
[PROOFSTEP]
exact N.lie_mem hm
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑N
⊢ ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N
[PROOFSTEP]
simpa using N.lie_mem hm
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h :
  optParam
    (∀ (m : M) (hm : m ∈ ↑N),
      ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
    (_ :
      ∀ (m : M) (hm : m ∈ ↑N),
        ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
⊢ LinearMap.restrict (↑(toEndomorphism R L M) x) h = ↑(toEndomorphism R L { x // x ∈ ↑N }) x
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h :
  optParam
    (∀ (m : M) (hm : m ∈ ↑N),
      ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
    (_ :
      ∀ (m : M) (hm : m ∈ ↑N),
        ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
x✝ : { x // x ∈ ↑N }
⊢ ↑(↑(LinearMap.restrict (↑(toEndomorphism R L M) x) h) x✝) = ↑(↑(↑(toEndomorphism R L { x // x ∈ ↑N }) x) x✝)
[PROOFSTEP]
simp [LinearMap.restrict_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ ↑(ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R
[PROOFSTEP]
ext a b
[GOAL]
case h.h
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ↑(↑(ad R A) a) b = ↑((LinearMap.mulLeft R - LinearMap.mulRight R) a) b
[PROOFSTEP]
simp [LieRing.of_associative_ring_bracket]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
x : { x // x ∈ K }
⊢ LinearMap.comp (↑(ad R L) ↑x) ↑(incl K) = LinearMap.comp (↑(incl K)) (↑(ad R { x // x ∈ K }) x)
[PROOFSTEP]
ext y
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
x y : { x // x ∈ K }
⊢ ↑(LinearMap.comp (↑(ad R L) ↑x) ↑(incl K)) y = ↑(LinearMap.comp (↑(incl K)) (↑(ad R { x // x ∈ K }) x)) y
[PROOFSTEP]
simp only [ad_apply, LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp, LieSubalgebra.coe_bracket,
  Function.comp_apply]
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : A}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : A}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : A}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
change ⁅x, y⁆ ∈ A'
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : A}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : A}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈ A'
[PROOFSTEP]
change x ∈ A' at hx
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : A}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hx : x ∈ A'
⊢ ⁅x, y⁆ ∈ A'
[PROOFSTEP]
change y ∈ A' at hy
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ ⁅x, y⁆ ∈ A'
[PROOFSTEP]
rw [LieRing.of_associative_ring_bracket]
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ x * y - y * x ∈ A'
[PROOFSTEP]
have hxy := A'.mul_mem hx hy
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hx : x ∈ A'
hy : y ∈ A'
hxy : x * y ∈ A'
⊢ x * y - y * x ∈ A'
[PROOFSTEP]
have hyx := A'.mul_mem hy hx
[GOAL]
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
src✝ : (fun x => Submodule R A) A' := ↑Subalgebra.toSubmodule A'
x y : A
hx : x ∈ A'
hy : y ∈ A'
hxy : x * y ∈ A'
hyx : y * x ∈ A'
⊢ x * y - y * x ∈ A'
[PROOFSTEP]
exact Submodule.sub_mem (Subalgebra.toSubmodule A') hxy hyx
[GOAL]
R : Type u
M₁ : Type v
M₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M₁ ≃ₗ[R] M₂
src✝ : Module.End R M₁ ≃ₗ[R] Module.End R M₂ := conj e
f g : Module.End R M₁
⊢ ↑(conj e) ⁅f, g⁆ = ⁅↑(conj e) f, ↑(conj e) g⁆
[PROOFSTEP]
simp only [LieRing.of_associative_ring_bracket, LinearMap.mul_eq_comp, e.conj_comp, LinearEquiv.map_sub]
[GOAL]
R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
src✝ : A₁ ≃ₗ[R] A₂ := toLinearEquiv e
x y : A₁
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := e.toFun,
              map_add' :=
                (_ :
                  ∀ (x y : A₁),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A₁),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := e.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : A₁),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A₁),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := e.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : A₁),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A₁),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
have : e.toEquiv.toFun = e := rfl
[GOAL]
R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
src✝ : A₁ ≃ₗ[R] A₂ := toLinearEquiv e
x y : A₁
this : e.toFun = ↑e
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := e.toFun,
              map_add' :=
                (_ :
                  ∀ (x y : A₁),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A₁),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := e.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : A₁),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A₁),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := e.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : A₁),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A₁),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
simp_rw [LieRing.of_associative_ring_bracket, this, map_sub, map_mul]