case lie_self
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝ : lib R X
⊢ ↑(liftAux R f) (a✝ * a✝) = ↑(liftAux R f) 0

case leibniz_lie
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝ b✝ c✝ : lib R X
⊢ ↑(liftAux R f) (a✝ * (b✝ * c✝)) = ↑(liftAux R f) (a✝ * b✝ * c✝ + b✝ * (a✝ * c✝))

case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t✝ : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (t✝ • a✝¹) = ↑(liftAux R f) (t✝ • b✝)

case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
h : Rel R X a b
⊢ ↑(liftAux R f) a = ↑(liftAux R f) b
induction h
case leibniz_lie
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝ b✝ c✝ : lib R X
⊢ ↑(liftAux R f) (a✝ * (b✝ * c✝)) = ↑(liftAux R f) (a✝ * b✝ * c✝ + b✝ * (a✝ * c✝))

case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t✝ : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (t✝ • a✝¹) = ↑(liftAux R f) (t✝ • b✝)

case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case lie_self
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝ : lib R X
⊢ ↑(liftAux R f) (a✝ * a✝) = ↑(liftAux R f) 0

case leibniz_lie
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝ b✝ c✝ : lib R X
⊢ ↑(liftAux R f) (a✝ * (b✝ * c✝)) = ↑(liftAux R f) (a✝ * b✝ * c✝ + b✝ * (a✝ * c✝))

case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t✝ : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (t✝ • a✝¹) = ↑(liftAux R f) (t✝ • b✝)

case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]
case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t✝ : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (t✝ • a✝¹) = ↑(liftAux R f) (t✝ • b✝)

case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case leibniz_lie
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝ b✝ c✝ : lib R X
⊢ ↑(liftAux R f) (a✝ * (b✝ * c✝)) = ↑(liftAux R f) (a✝ * b✝ * c✝ + b✝ * (a✝ * c✝))

case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t✝ : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (t✝ • a✝¹) = ↑(liftAux R f) (t✝ • b✝)

case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case leibniz_lie a' b' c' =>
  simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case smul
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t✝ : R
a✝¹ b✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (t✝ • a✝¹) = ↑(liftAux R f) (t✝ • b✝)

case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case smul t a' b' _ h₂ => simp only [liftAux_map_smul, h₂]
case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ + c✝) = ↑(liftAux R f) (b✝ + c✝)

case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case add_right a' b' c' _ h₂ => simp only [liftAux_map_add, h₂]
case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
a_ih✝ : ↑(liftAux R f) b✝ = ↑(liftAux R f) c✝
⊢ ↑(liftAux R f) (a✝¹ * b✝) = ↑(liftAux R f) (a✝¹ * c✝)

case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case mul_left a' b' c' _ h₂ => simp only [liftAux_map_mul, h₂]
no goals
case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c✝ : lib R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : ↑(liftAux R f) a✝¹ = ↑(liftAux R f) b✝
⊢ ↑(liftAux R f) (a✝¹ * c✝) = ↑(liftAux R f) (b✝ * c✝)
case mul_right a' b' c' _ h₂ => simp only [liftAux_map_mul, h₂]
no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' : lib R X
⊢ ↑(liftAux R f) (a' * a') = ↑(liftAux R f) 0
simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]
no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' b' c' : lib R X
⊢ ↑(liftAux R f) (a' * (b' * c')) = ↑(liftAux R f) (a' * b' * c' + b' * (a' * c'))
simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b : lib R X
t : R
a' b' : lib R X
a✝ : Rel R X a' b'
h₂ : ↑(liftAux R f) a' = ↑(liftAux R f) b'
⊢ ↑(liftAux R f) (t • a') = ↑(liftAux R f) (t • b')
simp only [liftAux_map_smul, h₂]
no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' b' c' : lib R X
a✝ : Rel R X a' b'
h₂ : ↑(liftAux R f) a' = ↑(liftAux R f) b'
⊢ ↑(liftAux R f) (a' + c') = ↑(liftAux R f) (b' + c')
simp only [liftAux_map_add, h₂]
no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' b' c' : lib R X
a✝ : Rel R X b' c'
h₂ : ↑(liftAux R f) b' = ↑(liftAux R f) c'
⊢ ↑(liftAux R f) (a' * b') = ↑(liftAux R f) (a' * c')
simp only [liftAux_map_mul, h₂]
no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a' b' c' : lib R X
a✝ : Rel R X a' b'
h₂ : ↑(liftAux R f) a' = ↑(liftAux R f) b'
⊢ ↑(liftAux R f) (a' * c') = ↑(liftAux R f) (b' * c')
simp only [liftAux_map_mul, h₂]