English
liftAux_spec asserts that liftAux respects the defining relation of the FreeLieAlgebra construction.
Русский
LiftAux_spec утверждает, что liftAux сохраняет определяющее отношение построения FreeLieAlgebra.
LaTeX
$$$\mathrm{liftAux\_spec}(R,f) : \forall a,b\ (h : \mathrm{Rel}(R,X,a,b) \\Rightarrow \mathrm{liftAux}(R,f)(a) = \mathrm{liftAux}(R,f)(b))$$$
Lean4
theorem liftAux_spec (f : X → L) (a b : lib R X) (h : FreeLieAlgebra.Rel R X a b) : liftAux R f a = liftAux R f b := by
induction h with
| lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]
| leibniz_lie a' b' c' => simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
| smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
| add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
| mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
| mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
