∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : IsLieAbelian L]
  (ψ : Module.Dual R L), LieAlgebra.lieCharacterEquivLinearDual.symm ψ = { toLinearMap := ψ, map_lie' := ⋯ }