awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
⊢ (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
have 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)) sorry) :
                  RingQuot (R := TensorAlgebra R L) (Rel R L) →ₐ[R] A))
              f) :
          (a : L) → A)
        x :
      A)
    ((f : (a : L) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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)
    (((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)
have 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)) sorry) :
          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 [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom,
      UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
⊢ (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
have 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)) sorry) :
          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: apply RingQuot.ringQuot_ext'
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
⊢ 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))
have 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)) sorry) :
                      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: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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)
    ((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)
have 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)
Tactic: simp [mkAlgHom]
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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)
        ((ι R : (a : L) → UniversalEnvelopingAlgebra R L) x : UniversalEnvelopingAlgebra R L) :
      A)
    ((f : (a : L) → A) x : A)
have 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)
Tactic: rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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)
⊢ 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)
have rw₁ : Eq.{u₃ + 1} (α := A) ((f : (a : L) → A) x : A) ((f : (a : L) → A) x : A)
Tactic: rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
have refine : Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A) ↔
  (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
Tactic: refine Iff.trans ?_ (lift R).symm_apply_eq
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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) ↔
    (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
have mp : Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A) →
  (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
mp :
  Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) →
    (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
⊢ Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) ↔
    (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
have mpr : (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f →
  Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
h :
  Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)
⊢ (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
have mp : ∀ (x : L),
  Eq.{u₃ + 1} (α := A)
    ((((Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g : L →ₗ⁅R⁆ A) : (a : L) → A)
        x :
      A)
    ((f : (a : L) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
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
h : (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
⊢ Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)
have mpr : ∀ (x : L),
  Eq.{u₃ + 1} (α := A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L) x :
      A)
    ((f : (a : L) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (χ₁ + χ₂)) ⁅x, m⁆
have rw : ∀ (i : ↥H),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpaceOf M ((χ₁ + χ₂) i) i : LieSubmodule.{u_1, u_2, u_3} R (↥H) M) ⁅x, m⁆
Tactic: rw [genWeightSpace, LieSubmodule.mem_iInf]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
⊢ Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
have rw : ∀ (hx : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ i) i) x)
  (hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m) (y : ↥H),
  Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
Tactic: rw [rootSpace, genWeightSpace, LieSubmodule.mem_iInf] at hx
Cleared hypotheses: hx, hm, y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpaceOf M ((χ₁ + χ₂) y) y : LieSubmodule.{u_1, u_2, u_3} R (↥H) M) ⁅x, m⁆
have hx₁ : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
Tactic: replace hx : x ∈ genWeightSpaceOf L (χ₁ y) y := by
    rw [rootSpace, genWeightSpace, LieSubmodule.mem_iInf] at hx; exact hx y
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m
have rw : ∀ (hm : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ i) i) m)
  (y : ↥H) (hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m
Tactic: rw [genWeightSpace, LieSubmodule.mem_iInf] at hm
Cleared hypotheses: hm, y, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpaceOf M ((χ₁ + χ₂) y) y : LieSubmodule.{u_1, u_2, u_3} R (↥H) M) ⁅x, m⁆
have hm₁ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m
Tactic: replace hm : m ∈ genWeightSpaceOf M (χ₂ y) y := by
    rw [genWeightSpace, LieSubmodule.mem_iInf] at hm; exact hm y
Cleared hypotheses: hm