case h
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h₁ : ∀ (x y : L₁), ↑f (x + y) = ↑f x + ↑f y
h₂ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := ↑f, map_add' := h₁ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := ↑f, map_add' := h₁ } x
h₃ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom y⁆
x✝ : L₁
⊢ ↑{ toLinearMap := { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }, map_lie' := h₃ } x✝ = ↑f x✝
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h₁ : ∀ (x y : L₁), ↑f (x + y) = ↑f x + ↑f y
h₂ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := ↑f, map_add' := h₁ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := ↑f, map_add' := h₁ } x
h₃ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom y⁆
⊢ { toLinearMap := { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }, map_lie' := h₃ } = f
ext
no goals
case h
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h₁ : ∀ (x y : L₁), ↑f (x + y) = ↑f x + ↑f y
h₂ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := ↑f, map_add' := h₁ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := ↑f, map_add' := h₁ } x
h₃ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom y⁆
x✝ : L₁
⊢ ↑{ toLinearMap := { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }, map_lie' := h₃ } x✝ = ↑f x✝
rfl