awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
⊢ Eq (α := UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
          (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) :
      UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)) :
      UniversalEnvelopingAlgebra R L)

Tactic:
RingQuot.mkAlgHom_rel _ (Rel.lie_compat x y)

Premises used: UniversalEnvelopingAlgebra, RingQuot.mkAlgHom_rel, UniversalEnvelopingAlgebra.Rel.lie_compat
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
⊢ Eq (α := UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
          (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) :
      UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)) :
      UniversalEnvelopingAlgebra R L)

Tactic:
exact RingQuot.mkAlgHom_rel _ (Rel.lie_compat x y)

Premises used: RingQuot.mkAlgHom_rel, UniversalEnvelopingAlgebra.Rel.lie_compat
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f_1 f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
h : Rel R L a b
lie_compat :
  ∀ (x y : L),
    Eq.{u₃ + 1} (α := A)
      ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
              TensorAlgebra R L →ₐ[R] A) :
            (a : TensorAlgebra R L) → A)
          (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
            (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
              ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
              ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) :
        A)
      ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
              TensorAlgebra R L →ₐ[R] A) :
            (a : TensorAlgebra R L) → A)
          (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)) :
        A)
⊢ Eq.{u₃ + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        a :
      A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        b :
      A)

Tactic:
induction h
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f_1 f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
x y : L
⊢ Eq.{u₃ + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
          (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) :
      A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)) :
      A)

Tactic:
simp only [LieRing.of_associative_ring_bracket, map_add, TensorAlgebra.lift_ι_apply,
          LieHom.coe_toLinearMap, LieHom.map_lie, map_mul, sub_add_cancel]

Premises used: LieHom.map_lie, TensorAlgebra.lift_ι_apply, map_add, LieRing.of_associative_ring_bracket, map_mul, LieHom.coe_toLinearMap, sub_add_cancel
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f_1 f : L →ₗ⁅R⁆ A
h :
  ∀ (x : L),
    Eq.{u₃ + 1} (α := A)
      (((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R))
              ((fun (f : L →ₗ⁅R⁆ A) ↦
                  ((RingQuot.liftAlgHom R (s := Rel R L) :
                        (a :
                            { f : TensorAlgebra R L →ₐ[R] A //
                              ∀ ⦃x y : TensorAlgebra R L⦄,
                                Rel R L x y →
                                  (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                          RingQuot (Rel R L) →ₐ[R] A)
                      (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                        ∀ ⦃x y : TensorAlgebra R L⦄,
                          Rel R L x y →
                            Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                              ((f : (a : TensorAlgebra R L) → A) y : A))
                        ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
                    RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
                f) :
            (a : L) → A)
          x :
        A)
      ((f : (a : L) → A) x : A)
⊢ (fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R))
      ((fun (f : L →ₗ⁅R⁆ A) ↦
          ((RingQuot.liftAlgHom R (s := Rel R L) :
                (a :
                    { f : TensorAlgebra R L →ₐ[R] A //
                      ∀ ⦃x y : TensorAlgebra R L⦄,
                        Rel R L x y → (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                  RingQuot (Rel R L) →ₐ[R] A)
              (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                ∀ ⦃x y : TensorAlgebra R L⦄,
                  Rel R L x y →
                    Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                      ((f : (a : TensorAlgebra R L) → A) y : A))
                ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
            RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f_1 f : L →ₗ⁅R⁆ A
x : L
h :
  Eq.{u₃ + 1} (α := A)
    ((((RingQuot.liftAlgHom R (s := Rel R L) :
                (a :
                    { f : TensorAlgebra R L →ₐ[R] A //
                      ∀ ⦃x y : TensorAlgebra R L⦄,
                        Rel R L x y → (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                  RingQuot (Rel R L) →ₐ[R] A)
              (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                ∀ ⦃x y : TensorAlgebra R L⦄,
                  Rel R L x y →
                    Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                      ((f : (a : TensorAlgebra R L) → A) y : A))
                ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
            RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A) :
          (a : UniversalEnvelopingAlgebra R L) → A)
        ((RingQuot.mkAlgHom R (Rel R L) : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          UniversalEnvelopingAlgebra R L) :
      A)
    ((f : (a : L) → A) x : A)
⊢ Eq.{u₃ + 1} (α := A)
    (((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R))
            ((fun (f : L →ₗ⁅R⁆ A) ↦
                ((RingQuot.liftAlgHom R (s := Rel R L) :
                      (a :
                          { f : TensorAlgebra R L →ₐ[R] A //
                            ∀ ⦃x y : TensorAlgebra R L⦄,
                              Rel R L x y →
                                (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                        RingQuot (Rel R L) →ₐ[R] A)
                    (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                      ∀ ⦃x y : TensorAlgebra R L⦄,
                        Rel R L x y →
                          Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                            ((f : (a : TensorAlgebra R L) → A) y : A))
                      ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
                  RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
              f) :
          (a : L) → A)
        x :
      A)
    ((f : (a : L) → A) x : A)

Tactic:
simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom,
      UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]

Premises used: UniversalEnvelopingAlgebra.mkAlgHom, LieHom.coe_comp, UniversalEnvelopingAlgebra.ι_apply, AlgHom.coe_toLieHom, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f_1 f : L →ₗ⁅R⁆ A
x : L
⊢ Eq.{u₃ + 1} (α := A)
    ((((RingQuot.liftAlgHom R (s := Rel R L) :
                (a :
                    { f : TensorAlgebra R L →ₐ[R] A //
                      ∀ ⦃x y : TensorAlgebra R L⦄,
                        Rel R L x y → (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                  RingQuot (Rel R L) →ₐ[R] A)
              (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                ∀ ⦃x y : TensorAlgebra R L⦄,
                  Rel R L x y →
                    Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                      ((f : (a : TensorAlgebra R L) → A) y : A))
                ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
            RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A) :
          (a : UniversalEnvelopingAlgebra R L) → A)
        ((RingQuot.mkAlgHom R (Rel R L) : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          UniversalEnvelopingAlgebra R L) :
      A)
    ((f : (a : L) → A) x : A)

Tactic:
simp only [UniversalEnvelopingAlgebra, RingQuot.liftAlgHom_mkAlgHom_apply,
      TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap]

Premises used: TensorAlgebra.lift_ι_apply, UniversalEnvelopingAlgebra, RingQuot.liftAlgHom_mkAlgHom_apply, LieHom.coe_toLinearMap
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
w :
  AlgHom.comp (B := RingQuot (R := TensorAlgebra R L) (Rel R L))
      ((fun (f : L →ₗ⁅R⁆ A) ↦
          ((RingQuot.liftAlgHom R (s := Rel R L) :
                (a :
                    { f : TensorAlgebra R L →ₐ[R] A //
                      ∀ ⦃x y : TensorAlgebra R L⦄,
                        Rel R L x y → (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                  RingQuot (Rel R L) →ₐ[R] A)
              (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                ∀ ⦃x y : TensorAlgebra R L⦄,
                  Rel R L x y →
                    Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                      ((f : (a : TensorAlgebra R L) → A) y : A))
                ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
            RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
        ((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R)) F))
      (RingQuot.mkAlgHom R (Rel R L)) =
    F.comp (RingQuot.mkAlgHom R (Rel R L))
⊢ (fun (f : L →ₗ⁅R⁆ A) ↦
        ((RingQuot.liftAlgHom R (s := Rel R L) :
              (a :
                  { f : TensorAlgebra R L →ₐ[R] A //
                    ∀ ⦃x y : TensorAlgebra R L⦄,
                      Rel R L x y → (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                RingQuot (Rel R L) →ₐ[R] A)
            (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
              ∀ ⦃x y : TensorAlgebra R L⦄,
                Rel R L x y →
                  Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                    ((f : (a : TensorAlgebra R L) → A) y : A))
              ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
          RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
      ((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R)) F) =
    F

Tactic:
apply RingQuot.ringQuot_ext'

Premises used: RingQuot.ringQuot_ext'
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
w :
  ∀ (x : L),
    Eq.{u₃ + 1} (α := A)
      ((AlgHom.toLinearMap
                (AlgHom.comp (B := RingQuot (R := TensorAlgebra R L) (Rel R L))
                  ((fun (f : L →ₗ⁅R⁆ A) ↦
                      ((RingQuot.liftAlgHom R (s := Rel R L) :
                            (a :
                                { f : TensorAlgebra R L →ₐ[R] A //
                                  ∀ ⦃x y : TensorAlgebra R L⦄,
                                    Rel R L x y →
                                      (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                              RingQuot (Rel R L) →ₐ[R] A)
                          (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                            ∀ ⦃x y : TensorAlgebra R L⦄,
                              Rel R L x y →
                                Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                                  ((f : (a : TensorAlgebra R L) → A) y : A))
                            ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
                        RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
                    ((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R)) F))
                  (RingQuot.mkAlgHom R (Rel R L))) ∘ₗ
              ιₜ :
            (a : L) → A)
          x :
        A)
      (((F.comp (RingQuot.mkAlgHom R (Rel R L))).toLinearMap ∘ₗ ιₜ : (a : L) → A) x : A)
⊢ AlgHom.comp (B := RingQuot (R := TensorAlgebra R L) (Rel R L))
      ((fun (f : L →ₗ⁅R⁆ A) ↦
          ((RingQuot.liftAlgHom R (s := Rel R L) :
                (a :
                    { f : TensorAlgebra R L →ₐ[R] A //
                      ∀ ⦃x y : TensorAlgebra R L⦄,
                        Rel R L x y → (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                  RingQuot (Rel R L) →ₐ[R] A)
              (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                ∀ ⦃x y : TensorAlgebra R L⦄,
                  Rel R L x y →
                    Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                      ((f : (a : TensorAlgebra R L) → A) y : A))
                ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
            RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
        ((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R)) F))
      (RingQuot.mkAlgHom R (Rel R L)) =
    F.comp (RingQuot.mkAlgHom R (Rel R L))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
x : L
w :
  Eq.{u₃ + 1} (α := A)
    ((F : (a : UniversalEnvelopingAlgebra R L) → A)
        ((RingQuot.mkAlgHom R (Rel R L) : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          UniversalEnvelopingAlgebra R L) :
      A)
    ((F : (a : RingQuot (Rel R L)) → A)
        ((RingQuot.mkAlgHom R (Rel R L) : (a : TensorAlgebra R L) → RingQuot (Rel R L))
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          RingQuot (R := TensorAlgebra R L) (Rel R L)) :
      A)
⊢ Eq.{u₃ + 1} (α := A)
    ((AlgHom.toLinearMap
              (AlgHom.comp (B := RingQuot (R := TensorAlgebra R L) (Rel R L))
                ((fun (f : L →ₗ⁅R⁆ A) ↦
                    ((RingQuot.liftAlgHom R (s := Rel R L) :
                          (a :
                              { f : TensorAlgebra R L →ₐ[R] A //
                                ∀ ⦃x y : TensorAlgebra R L⦄,
                                  Rel R L x y →
                                    (f : (a : TensorAlgebra R L) → A) x = (f : (a : TensorAlgebra R L) → A) y }) →
                            RingQuot (Rel R L) →ₐ[R] A)
                        (Subtype.mk (p := fun (f : TensorAlgebra R L →ₐ[R] A) ↦
                          ∀ ⦃x y : TensorAlgebra R L⦄,
                            Rel R L x y →
                              Eq.{u₃ + 1} (α := A) ((f : (a : TensorAlgebra R L) → A) x : A)
                                ((f : (a : TensorAlgebra R L) → A) y : A))
                          ((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A)) ⋯) :
                      RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
                  ((fun (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) ↦ F.toLieHom.comp (ι R)) F))
                (RingQuot.mkAlgHom R (Rel R L))) ∘ₗ
            ιₜ :
          (a : L) → A)
        x :
      A)
    (((F.comp (RingQuot.mkAlgHom R (Rel R L))).toLinearMap ∘ₗ ιₜ : (a : L) → A) x : A)

Tactic:
simp [mkAlgHom]

Premises used: UniversalEnvelopingAlgebra.mkAlgHom
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
x : L
⊢ Eq.{u₃ + 1} (α := A)
    ((F : (a : UniversalEnvelopingAlgebra R L) → A)
        ((RingQuot.mkAlgHom R (Rel R L) : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          UniversalEnvelopingAlgebra R L) :
      A)
    ((F : (a : RingQuot (Rel R L)) → A)
        ((RingQuot.mkAlgHom R (Rel R L) : (a : TensorAlgebra R L) → RingQuot (Rel R L))
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          RingQuot (R := TensorAlgebra R L) (Rel R L)) :
      A)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) F = F.toLieHom.comp (ι R)

Tactic:
rfl

Premises used: LieHom.comp, rfl
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
⊢ Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L)
      (⇑((lift R : (a : L →ₗ⁅R⁆ A) → UniversalEnvelopingAlgebra R L →ₐ[R] A) f :
            UniversalEnvelopingAlgebra R L →ₐ[R] A) :
        (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)

Tactic:
funext <| LieHom.ext_iff.mp <| (lift R).symm_apply_apply f

Premises used: LieHom.ext_iff, UniversalEnvelopingAlgebra.lift, Equiv.symm_apply_apply, funext, Iff.mp
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
rw :
  Eq.{u₃ + 1} (α := A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L)
        (⇑((lift R : (a : L →ₗ⁅R⁆ A) → UniversalEnvelopingAlgebra R L →ₐ[R] A) f :
              UniversalEnvelopingAlgebra R L →ₐ[R] A) :
          (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L) x :
      A)
    ((f : (a : L) → A) x : A)
rw₁ rw₂ : Eq.{u₃ + 1} (α := A) ((f : (a : L) → A) x : A) ((f : (a : L) → A) x : A)
⊢ Eq.{u₃ + 1} (α := A)
    ((((lift R : (a : L →ₗ⁅R⁆ A) → UniversalEnvelopingAlgebra R L →ₐ[R] A) f : UniversalEnvelopingAlgebra R L →ₐ[R] A) :
          (a : UniversalEnvelopingAlgebra R L) → A)
        ((ι R : (a : L) → UniversalEnvelopingAlgebra R L) x : UniversalEnvelopingAlgebra R L) :
      A)
    ((f : (a : L) → A) x : A)

Tactic:
rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]

Premises used: UniversalEnvelopingAlgebra.ι_comp_lift, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ Eq.{u₃ + 1} (α := A)
    ((((lift R : (a : L →ₗ⁅R⁆ A) → UniversalEnvelopingAlgebra R L →ₐ[R] A) f : UniversalEnvelopingAlgebra R L →ₐ[R] A) :
          (a : UniversalEnvelopingAlgebra R L) → A)
        ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x) :
          UniversalEnvelopingAlgebra R L) :
      A)
    ((f : (a : L) → A) x : A)

Tactic:
simpa using lift_ι_apply R f x

Premises used: UniversalEnvelopingAlgebra.lift_ι_apply
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) ↔
    g = (lift R : (a : L →ₗ⁅R⁆ A) → UniversalEnvelopingAlgebra R L →ₐ[R] A) f

Tactic:
Iff.trans ?_ (lift R).symm_apply_eq

Premises used: UniversalEnvelopingAlgebra.lift, Equiv.symm_apply_eq, Iff.trans