awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
f : X → L
⊢ (fun (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) ↦
        (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R) : X → L))
      ((fun (f : X → L) ↦
          ({
              toFun := fun (c : FreeLieAlgebra R X) ↦
                Quot.liftOn (r := Rel R X) c (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯,
              map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
            FreeLieAlgebra R X →ₗ⁅R⁆ L))
        f) =
    f
have h : ∀ (x : X),
  (fun (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) ↦
        (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R) : X → L))
      ((fun (f : X → L) ↦
          ({
              toFun := fun (c : FreeLieAlgebra R X) ↦
                Quot.liftOn (r := Rel R X) c (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) sorry,
              map_add' := sorry, map_smul' := sorry, map_lie' := sorry } :
            FreeLieAlgebra R X →ₗ⁅R⁆ L))
        f)
      x =
    f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (fun (f : X → L) ↦
        ({
            toFun := fun (c : FreeLieAlgebra R X) ↦
              Quot.liftOn (r := Rel R X) c (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯,
            map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
          FreeLieAlgebra R X →ₗ⁅R⁆ L))
      ((fun (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) ↦
          (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R) : X → L))
        F) =
    F
have h : ∀ (x : FreeLieAlgebra R X) (a : lib R X),
  Eq.{w + 1} (α := L)
    (((fun (f : X → L) ↦
              ({
                  toFun := fun (c : FreeLieAlgebra R X) ↦
                    Quot.liftOn (r := Rel R X) c (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) sorry,
                  map_add' := sorry, map_smul' := sorry, map_lie' := sorry } :
                FreeLieAlgebra R X →ₗ⁅R⁆ L))
            ((fun (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) ↦
                (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R) : X → L))
              F) :
          (a : FreeLieAlgebra R X) → L)
        (Quot.mk (Rel R X) a) :
      L)
    ((F : (a : FreeLieAlgebra R X) → L) (Quot.mk (Rel R X) a) : L)
Tactic: ext ⟨a⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
f : X → L
x : X
⊢ (((lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L) f : FreeLieAlgebra R X →ₗ⁅R⁆ L) : (a : FreeLieAlgebra R X) → L)
      (of R x) =
    f x
have rw : Function.comp (β := FreeLieAlgebra R X)
    (⇑((lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L) f : FreeLieAlgebra R X →ₗ⁅R⁆ L) :
      (a : FreeLieAlgebra R X) → L)
    (of R) x =
  f x
Tactic: rw [← @Function.comp_apply _ _ _ (lift R f) (of R) x, of_comp_lift]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
f : X → L
x : X
rw :
  Function.comp (β := FreeLieAlgebra R X)
      (⇑((lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L) f : FreeLieAlgebra R X →ₗ⁅R⁆ L) :
        (a : FreeLieAlgebra R X) → L)
      (of R) x =
    f x
⊢ (((lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L) f : FreeLieAlgebra R X →ₗ⁅R⁆ L) : (a : FreeLieAlgebra R X) → L)
      (of R x) =
    f x
have rw₁ : f x = f x
Tactic: rw [← @Function.comp_apply _ _ _ (lift R f) (of R) x, of_comp_lift]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L)
      (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R)) =
    F
have rw : (lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L)
    ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F) =
  F
Tactic: rw [← lift_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h :
  ∀ (x : X),
    Eq.{w + 1} (α := L) ((F₁ : (a : FreeLieAlgebra R X) → L) (of R x) : L)
      ((F₂ : (a : FreeLieAlgebra R X) → L) (of R x) : L)
⊢ Eq (α := X → L) ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F₁ : X → L)
    ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F₂ : X → L)
have h₁ : ∀ (x : X),
  Eq.{w + 1} (α := L) ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F₁ x : L)
    ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F₂ x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := FreeAlgebra R X →ₐ[R] FreeAlgebra R X)
    (AlgHom.comp (B := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
      ((UniversalEnvelopingAlgebra.lift R :
          (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
            UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
        ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R)))
      ((FreeAlgebra.lift R :
          (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
            FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (Function.comp (β := FreeLieAlgebra R X)
          (⇑(UniversalEnvelopingAlgebra.ι R) :
            (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
          (of R))))
    (AlgHom.id R (FreeAlgebra R X))
have w : ∀ (x : X),
  Eq (α := FreeAlgebra R X)
    (Function.comp (β := FreeAlgebra R X)
      (⇑(AlgHom.comp (B := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
            ((UniversalEnvelopingAlgebra.lift R :
                (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
                  UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
              ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R)))
            ((FreeAlgebra.lift R :
                (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
                  FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
              (Function.comp (β := FreeLieAlgebra R X)
                (⇑(UniversalEnvelopingAlgebra.ι R) :
                  (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                (of R)))) :
        (a : FreeAlgebra R X) → FreeAlgebra R X)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R X) (⇑(AlgHom.id R (FreeAlgebra R X)) : (a : FreeAlgebra R X) → FreeAlgebra R X)
      (FreeAlgebra.ι R) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
    (AlgHom.comp (B := FreeAlgebra R X)
      ((FreeAlgebra.lift R :
          (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
            FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (Function.comp (β := FreeLieAlgebra R X)
          (⇑(UniversalEnvelopingAlgebra.ι R) :
            (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
          (of R)))
      ((UniversalEnvelopingAlgebra.lift R :
          (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
            UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
        ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R))))
    (AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)))
have h : ∀ (x : X),
  Eq (α := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
    ((LieHom.comp
            (AlgHom.toLieHom
              (AlgHom.comp (B := FreeAlgebra R X)
                ((FreeAlgebra.lift R :
                    (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
                      FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                  (Function.comp (β := FreeLieAlgebra R X)
                    (⇑(UniversalEnvelopingAlgebra.ι R) :
                      (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                    (of R)))
                ((UniversalEnvelopingAlgebra.lift R :
                    (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
                      UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
                  ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R)))))
            (UniversalEnvelopingAlgebra.ι R) :
          (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (of R x) :
      UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
    ((LieHom.comp (AlgHom.toLieHom (AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))))
            (UniversalEnvelopingAlgebra.ι R) :
          (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (of R x) :
      UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (goal)
Goal:
ι : Type u_1
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
x y : L
⊢ Eq (α := ⨁ (i : ι), ↥(ℒ i)) ((decompose ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) ⁅x, y⁆ : ⨁ (i : ι), ↥(ℒ i))
    (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i)) ((decompose ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x : ⨁ (i : ι), ↥(ℒ i))
        ((decompose ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) y) :
      ⨁ (i : ι), ↥(ℒ i))
have simp : Eq (α := ⨁ (i : ι), ↥(ℒ i)) ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) ⁅x, y⁆ : ⨁ (i : ι), ↥(ℒ i))
  (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x : ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) y) :
    ⨁ (i : ι), ↥(ℒ i))
Tactic: simp only [← decomposeLinearEquiv_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (goal)
Goal:
ι : Type u_1
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ Eq.{u_4 + 1} (α := L) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) ⁅x, y⁆ : L)
    (Bracket.bracket (L := L) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) y) :
      L)
have simp : Eq.{u_4 + 1} (α := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) ⁅x, y⁆ : L)
  (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) y) :
    L)
Tactic: simp only [← decomposeLinearEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)
⊢ Membership.mem (γ := Submodule R (⨁ (i : ι), ↥(ℒ i)))
    (LinearMap.range (lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k)) b
have h : ((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b) hb) =
  b
Tactic: use ⟨(decompose ℒ).symm b, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)
⊢ (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := ↥(ℒ i) →ₗ[R] ↥(ℒ i)) ((φ : (a : ι) → R) i : R) LinearMap.id :
        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      b =
    HSMul.hSMul (α := R) ((φ : (a : ι) → R) k : R) b
have obtain : ∀ (w : ↥(ℒ k))
  (hb :
    Membership.mem (α := L) (ℒ k)
      ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
                (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
              w :
            ⨁ (i : ι), ↥(ℒ i)) :
        L)),
  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := ↥(ℒ i) →ₗ[R] ↥(ℒ i)) ((φ : (a : ι) → R) i : R) LinearMap.id :
        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
          (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
        w) =
    HSMul.hSMul (α := R) (β := ⨁ (i : ι), ↥(ℒ i)) ((φ : (a : ι) → R) k : R)
      (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
            (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
          w :
        ⨁ (i : ι), ↥(ℒ i))
Tactic: obtain ⟨_, rfl⟩ : b ∈ LinearMap.range (lof R ι (ℒ ·) k) := by
          use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (hypothesis)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      ⁅x, y⁆ =
    HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
      (⁅x,
          (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
              (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
            y⁆ :
        ⨁ (i : ι), ↥(ℒ i))
      (⁅y,
          (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
              (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
            x⁆ :
        ⨁ (i : ι), ↥(ℒ i))
have hM : ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i))
  (hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)),
  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := ↥(ℒ i) →ₗ[R] ↥(ℒ i)) ((φ : (a : ι) → R) i : R) LinearMap.id :
        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      b =
    HSMul.hSMul (α := R) ((φ : (a : ι) → R) k : R) b
Tactic: have hM (k : ι) (b : ⨁ i, ℒ i) (hb : (decompose ℒ).symm b ∈ ℒ k) :
          (toModule R ι (⨁ (i : ι), ℒ i) fun i ↦ lof R ι (ℒ ·) i ∘ₗ (φ i • .id)) b = (φ k) • b := by
        obtain ⟨_, rfl⟩ : b ∈ LinearMap.range (lof R ι (ℒ ·) k) := by
          use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]
        simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i))
    (hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)),
    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
            lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
              HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := ↥(ℒ i) →ₗ[R] ↥(ℒ i)) ((φ : (a : ι) → R) i : R) LinearMap.id :
          (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
        b =
      HSMul.hSMul (α := R) ((φ : (a : ι) → R) k : R) b
⊢ (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      ⁅x, y⁆ =
    HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
      (⁅x,
          (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
              (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
            y⁆ :
        ⨁ (i : ι), ↥(ℒ i))
      (⁅y,
          (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
              (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
            x⁆ :
        ⨁ (i : ι), ↥(ℒ i))
have w : ∀ (j : ι),
  (↑((((toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                    lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) sorry :
                  (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                ⁅x, y⁆ :
              ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L) =
    (↑((HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
              (⁅x,
                  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                        lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                          Module.End.smulLeft ((φ : (a : ι) → R) i) sorry :
                      (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                    y⁆ :
                ⨁ (i : ι), ↥(ℒ i))
              (⁅y,
                  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                        lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                          Module.End.smulLeft ((φ : (a : ι) → R) i) sorry :
                      (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                    x⁆ :
                ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Lie.Graded (goal)
Goal:
ι : Type u_1
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
φ : ι →+ R
i : ι
a : L
ha : a ∈ ℒ i
⊢ (ofGrading ℒ φ : (a : L) → L) a = HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((φ : (a : ι) → R) i : R) a
have simp : HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := L) ((φ : (a : ι) → R) i : R)
    (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
        (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
            (Subtype.mk (p := fun (x : L) ↦ x ∈ ℒ i) a ha) :
          ⨁ (i : ι), ↥(ℒ i)) :
      L) =
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((φ : (a : ι) → R) i : R) a
Tactic: simp [ofGrading, decomposeLinearEquiv_apply, decompose_of_mem ℒ ha]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅x, y⁆ ∈ I
have rw : ⁅-y, x⁆ ∈ I
Tactic: rw [← lie_skew, ← neg_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I : LieIdeal R L
x y : L
h : x ∈ (↑I : Submodule R L).carrier
hy : y ∈ (↑I : Submodule R L).carrier
⊢ ⁅x, y⁆ ∈ (↑I : Submodule R L).carrier
have h : y ∈ I
Tactic: apply lie_mem_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∃ (I : LieIdeal R ↥K'), LieIdeal.toLieSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
have simp : (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
Tactic: simp only [exists_lieIdeal_coe_eq_iff, coe_bracket, mem_ofLe]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
have mp : (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
mp : (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
⊢ (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
have mpr : (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
this : Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
have simp : Membership.mem (α := L') (toLieSubalgebra R L' J)
  (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
Tactic: simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          Submodule.mem_toAddSubmonoid, Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie,
          LieSubalgebra.mem_toSubmodule]