[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
suffices mkAlgHom R L (ιₜ ⁅x, y⁆ + ιₜ y * ιₜ x) = mkAlgHom R L (ιₜ x * ιₜ y) by rw [AlgHom.map_mul] at this ;
  simp [LieRing.of_associative_ring_bracket, ← this]
[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
this : ↑(mkAlgHom R L) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(mkAlgHom R L) (↑ιₜ x * ↑ιₜ y)
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
rw [AlgHom.map_mul] at this 
[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
this : ↑(mkAlgHom R L) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(mkAlgHom R L) (↑ιₜ x) * ↑(mkAlgHom R L) (↑ιₜ y)
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
simp [LieRing.of_associative_ring_bracket, ← this]
[GOAL]
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
src✝ : L →ₗ[R] UniversalEnvelopingAlgebra R L := LinearMap.comp (AlgHom.toLinearMap (mkAlgHom R L)) ιₜ
x y : L
⊢ ↑(mkAlgHom R L) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(mkAlgHom R L) (↑ιₜ x * ↑ιₜ y)
[PROOFSTEP]
exact RingQuot.mkAlgHom_rel _ (Rel.lie_compat x y)
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
⊢ ∀ ⦃x y : TensorAlgebra R L⦄, Rel R L x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
h : Rel R L a b
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b
[PROOFSTEP]
induction' h with x y
[GOAL]
case lie_compat
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
x y : L
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) (↑ιₜ ⁅x, y⁆ + ↑ιₜ y * ↑ιₜ x) = ↑(↑(TensorAlgebra.lift R) ↑f) (↑ιₜ x * ↑ιₜ y)
[PROOFSTEP]
simp only [LieRing.of_associative_ring_bracket, map_add, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
  LieHom.map_lie, map_mul, sub_add_cancel]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
⊢ (fun F => LieHom.comp (AlgHom.toLieHom F) (ι R))
      ((fun f =>
          ↑(RingQuot.liftAlgHom R)
            { val := ↑(TensorAlgebra.lift R) ↑f,
              property :=
                (_ :
                  ∀ ⦃a b : TensorAlgebra R L⦄,
                    Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
        f) =
    f
[PROOFSTEP]
ext
  -- Porting note: was
      -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
      --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_toLieHom,
      --   LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
      --   RingQuot.liftAlgHom_mkAlgHom_apply]
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ↑((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R))
          ((fun f =>
              ↑(RingQuot.liftAlgHom R)
                { val := ↑(TensorAlgebra.lift R) ↑f,
                  property :=
                    (_ :
                      ∀ ⦃a b : TensorAlgebra R L⦄,
                        Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom, UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ↑(↑(RingQuot.liftAlgHom R)
          { val := ↑(TensorAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ ⦃a b : TensorAlgebra R L⦄,
                  Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
      (↑(RingQuot.mkAlgHom R (Rel R L)) (↑ιₜ x✝)) =
    ↑f x✝
[PROOFSTEP]
rw [RingQuot.liftAlgHom_mkAlgHom_apply]
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) (↑ιₜ x✝) = ↑f x✝
[PROOFSTEP]
simp only [TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ (fun f =>
        ↑(RingQuot.liftAlgHom R)
          { val := ↑(TensorAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ ⦃a b : TensorAlgebra R L⦄,
                  Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
      ((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R)) F) =
    F
[PROOFSTEP]
apply RingQuot.ringQuot_ext'
[GOAL]
case w
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ AlgHom.comp
      ((fun f =>
          ↑(RingQuot.liftAlgHom R)
            { val := ↑(TensorAlgebra.lift R) ↑f,
              property :=
                (_ :
                  ∀ ⦃a b : TensorAlgebra R L⦄,
                    Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
        ((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R)) F))
      (RingQuot.mkAlgHom R (Rel R L)) =
    AlgHom.comp F (RingQuot.mkAlgHom R (Rel R L))
[PROOFSTEP]
ext
  -- Porting note: was
      -- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
      --   LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_linearMap_comp,
      --   AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply,
      --   RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_toLieHom, LieHom.coe_mk]
[GOAL]
case w.w.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
x✝ : L
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp
              ((fun f =>
                  ↑(RingQuot.liftAlgHom R)
                    { val := ↑(TensorAlgebra.lift R) ↑f,
                      property :=
                        (_ :
                          ∀ ⦃a b : TensorAlgebra R L⦄,
                            Rel R L a b → ↑(↑(TensorAlgebra.lift R) ↑f) a = ↑(↑(TensorAlgebra.lift R) ↑f) b) })
                ((fun F => LieHom.comp (AlgHom.toLieHom F) (ι R)) F))
              (RingQuot.mkAlgHom R (Rel R L))))
          ιₜ)
      x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp F (RingQuot.mkAlgHom R (Rel R L)))) ιₜ) x✝
[PROOFSTEP]
simp [mkAlgHom]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ↑(↑(lift R) f) (↑(ι R) x) = ↑f x
[PROOFSTEP]
rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ↑(↑(lift R) f) (↑(mkAlgHom R L) (↑ιₜ x)) = ↑f x
[PROOFSTEP]
simpa using lift_ι_apply R f x
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f ↔ g = ↑(lift R) f
[PROOFSTEP]
refine' Iff.trans _ (lift R).symm_apply_eq
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f ↔ ↑(lift R).symm g = f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f → ↑(lift R).symm g = f
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑g ∘ ↑(ι R) = ↑f
⊢ ↑(lift R).symm g = f
[PROOFSTEP]
ext
[GOAL]
case mp.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑g ∘ ↑(ι R) = ↑f
x✝ : L
⊢ ↑(↑(lift R).symm g) x✝ = ↑f x✝
[PROOFSTEP]
simp [← h]
[GOAL]
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑(lift R).symm g = f → ↑g ∘ ↑(ι R) = ↑f
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
⊢ ↑g ∘ ↑(ι R) = ↑f
[PROOFSTEP]
ext
[GOAL]
case mpr.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
x✝ : L
⊢ (↑g ∘ ↑(ι R)) x✝ = ↑f x✝
[PROOFSTEP]
simp [← h]
[GOAL]
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
⊢ ↑(lift R).symm g₁ = ↑(lift R).symm g₂
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
x✝ : L
⊢ ↑(↑(lift R).symm g₁) x✝ = ↑(↑(lift R).symm g₂) x✝
[PROOFSTEP]
simp [h]
