case mk.mk.mk.mk.mk.mk
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₁ → L₂
map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := f, map_add' := map_add'✝¹ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := f, map_add' := map_add'✝¹ } x
map_lie'✝¹ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ }.toAddHom y⁆
g : L₁ → L₂
map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := g, map_add' := map_add'✝ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := g, map_add' := map_add'✝ } x
map_lie'✝ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ }.toAddHom y⁆
h :
  ↑{ toLinearMap := { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ },
        map_lie' := map_lie'✝¹ } =
    ↑{ toLinearMap := { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ },
        map_lie' := map_lie'✝ }
⊢ { toLinearMap := { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ },
      map_lie' := map_lie'✝¹ } =
    { toLinearMap := { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ },
      map_lie' := map_lie'✝ }
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₃
⊢ Injective FunLike.coe
rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h
no goals
case mk.mk.mk.mk.mk.mk
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₁ → L₂
map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := f, map_add' := map_add'✝¹ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := f, map_add' := map_add'✝¹ } x
map_lie'✝¹ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ }.toAddHom y⁆
g : L₁ → L₂
map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (r : R) (x : L₁),
    AddHom.toFun { toFun := g, map_add' := map_add'✝ } (r • x) =
      ↑(RingHom.id R) r • AddHom.toFun { toFun := g, map_add' := map_add'✝ } x
map_lie'✝ :
  ∀ {x y : L₁},
    AddHom.toFun { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ }.toAddHom ⁅x, y⁆ =
      ⁅AddHom.toFun { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ }.toAddHom x,
        AddHom.toFun { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ }.toAddHom y⁆
h :
  ↑{ toLinearMap := { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ },
        map_lie' := map_lie'✝¹ } =
    ↑{ toLinearMap := { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ },
        map_lie' := map_lie'✝ }
⊢ { toLinearMap := { toAddHom := { toFun := f, map_add' := map_add'✝¹ }, map_smul' := map_smul'✝¹ },
      map_lie' := map_lie'✝¹ } =
    { toLinearMap := { toAddHom := { toFun := g, map_add' := map_add'✝ }, map_smul' := map_smul'✝ },
      map_lie' := map_lie'✝ }
congr