awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
x : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
b : lib R X
z : FreeLieAlgebra R X
c : lib R X
⊢ Quot.map₂ (r := Rel R X) (s := Rel R X) (t := Rel R X) (fun (x1 x2 : lib R X) ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a)
      (Quot.map₂ (r := Rel R X) (s := Rel R X) (t := Rel R X) (fun (x1 x2 : lib R X) ↦ x1 * x2) ⋯ ⋯
        (Quot.mk (Rel R X) b) (Quot.mk (Rel R X) c)) =
    HAdd.hAdd (α := FreeLieAlgebra R X)
      (Quot.map₂ (r := Rel R X) (s := Rel R X) (t := Rel R X) (fun (x1 x2 : lib R X) ↦ x1 * x2) ⋯ ⋯
        (Quot.map₂ (r := Rel R X) (s := Rel R X) (t := Rel R X) (fun (x1 x2 : lib R X) ↦ x1 * x2) ⋯ ⋯
          (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
        (Quot.mk (Rel R X) c))
      (Quot.map₂ (r := Rel R X) (s := Rel R X) (t := Rel R X) (fun (x1 x2 : lib R X) ↦ x1 * x2) ⋯ ⋯
        (Quot.mk (Rel R X) b)
        (Quot.map₂ (r := Rel R X) (s := Rel R X) (t := Rel R X) (fun (x1 x2 : lib R X) ↦ x1 * x2) ⋯ ⋯
          (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c)))

Tactic:
exact Quot.sound (Rel.leibniz_lie a b c)

Premises used: Quot.sound, FreeLieAlgebra.Rel.leibniz_lie
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
t : R
x : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
c : lib R X
mk : Eq (α := Quot (α := lib R X) (Rel R X)) (Quot.mk (Rel R X) (a • t • c)) (Quot.mk (Rel R X) (t • a • c))
⊢ Bracket.bracket (L := FreeLieAlgebra R X) (Quot.mk (Rel R X) a)
      (HSMul.hSMul (β := FreeLieAlgebra R X) t (Quot.mk (Rel R X) c)) =
    HSMul.hSMul (β := FreeLieAlgebra R X) t
      (Bracket.bracket (L := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c))

Tactic:
change Quot.mk _ (a • t • c) = Quot.mk _ (t • a • c)

Premises used: HSMul.hSMul, Quot.mk
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
t : R
x : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
c : lib R X
mk mk₁ : Eq (α := Quot (α := lib R X) (Rel R X)) (Quot.mk (Rel R X) (t • a • c)) (Quot.mk (Rel R X) (t • a • c))
⊢ Eq (α := Quot (α := lib R X) (Rel R X)) (Quot.mk (Rel R X) (a • t • c)) (Quot.mk (Rel R X) (t • a • c))

Tactic:
rw [← smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Lie.Free
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
t : R
a : lib R X
⊢ (liftAux R f : (a : lib R X) → CommutatorRing L) (t • a) =
    HSMul.hSMul (β := CommutatorRing L) t ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)

Tactic:
map_smul _ t a

Premises used: map_smul
-- Module: Mathlib.Algebra.Lie.Free
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
a b : lib R X
⊢ (liftAux R f : (a : lib R X) → CommutatorRing L) (a + b) =
    HAdd.hAdd (α := CommutatorRing L) (β := CommutatorRing L)
      ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)
      ((liftAux R f : (a : lib R X) → CommutatorRing L) b : CommutatorRing L)

Tactic:
map_add _ a b

Premises used: map_add
-- Module: Mathlib.Algebra.Lie.Free
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
a b : lib R X
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a * b) : CommutatorRing L)
    (Bracket.bracket (L := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)
        ((liftAux R f : (a : lib R X) → CommutatorRing L) b) :
      CommutatorRing L)

Tactic:
map_mul _ a b

Premises used: map_mul
-- Module: Mathlib.Algebra.Lie.Free
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
a b a' : lib R X
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a' * a') : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) 0 : CommutatorRing L)

Tactic:
simp only [liftAux_map_mul, map_zero, lie_self]

Premises used: map_zero, lie_self, FreeLieAlgebra.liftAux_map_mul
-- Module: Mathlib.Algebra.Lie.Free
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
a b a' b' c' : lib R X
⊢ Eq.{w + 1} (α := CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) (a' * (b' * c')) : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) (a' * b' * c' + b' * (a' * c')) : CommutatorRing L)

Tactic:
simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]

Premises used: FreeLieAlgebra.liftAux_map_add, FreeLieAlgebra.liftAux_map_mul, sub_add_cancel, lie_lie
-- Module: Mathlib.Algebra.Lie.Free
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
a b : lib R X
b' : R
a_1 b_1 : lib R X
h : Rel R X a_1 b_1
h₂ :
  Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a_1 : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) b_1 : CommutatorRing L)
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • a_1) : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • b_1) : CommutatorRing L)

Tactic:
simp only [liftAux_map_smul, h₂]

Premises used: FreeLieAlgebra.liftAux_map_smul
-- Module: Mathlib.Algebra.Lie.Free
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
a b a_1 b_1 c' : lib R X
h : Rel R X a_1 b_1
h₂ :
  Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a_1 : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) b_1 : CommutatorRing L)
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a_1 + c') : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) (b_1 + c') : CommutatorRing L)

Tactic:
simp only [liftAux_map_add, h₂]

Premises used: FreeLieAlgebra.liftAux_map_add
-- Module: Mathlib.Algebra.Lie.Free
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
a b c' b_1 c : lib R X
h : Rel R X b_1 c
h₂ :
  Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) b_1 : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) c : CommutatorRing L)
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (c' * b_1) : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) (c' * c) : CommutatorRing L)

Tactic:
simp only [liftAux_map_mul, h₂]

Premises used: FreeLieAlgebra.liftAux_map_mul
-- Module: Mathlib.Algebra.Lie.Free
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
a b a_1 b_1 c' : lib R X
h : Rel R X a_1 b_1
h₂ :
  Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a_1 : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) b_1 : CommutatorRing L)
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a_1 * c') : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) (b_1 * c') : CommutatorRing L)

Tactic:
simp only [liftAux_map_mul, h₂]

Premises used: FreeLieAlgebra.liftAux_map_mul
-- Module: Mathlib.Algebra.Lie.Free
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 : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
b : lib R X
mk :
  Quot.liftOn (r := Rel R X) (HAdd.hAdd (α := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    (liftAux R f : (a : lib R X) → CommutatorRing L) (a + b)
⊢ Quot.liftOn (r := Rel R X) (HAdd.hAdd (α := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) a) (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ +
      Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) b) (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯

Tactic:
rw [← liftAux_map_add]

Premises used: FreeLieAlgebra.liftAux_map_add
-- Module: Mathlib.Algebra.Lie.Free
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 : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
b : lib R X
⊢ Quot.liftOn (r := Rel R X) (HAdd.hAdd (α := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    (liftAux R f : (a : lib R X) → CommutatorRing L) (a + b)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Free
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
t : R
x : FreeLieAlgebra R X
a : lib R X
mk :
  Quot.liftOn (r := Rel R X) (HSMul.hSMul (β := FreeLieAlgebra R X) t (Quot.mk (Rel R X) a))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    (liftAux R f : (a : lib R X) → CommutatorRing L) (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R) a)
⊢ Quot.liftOn (r := Rel R X) (HSMul.hSMul (β := FreeLieAlgebra R X) t (Quot.mk (Rel R X) a))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R)
      (Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) a) (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯)

Tactic:
rw [← liftAux_map_smul]

Premises used: FreeLieAlgebra.liftAux_map_smul
-- Module: Mathlib.Algebra.Lie.Free
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
t : R
x : FreeLieAlgebra R X
a : lib R X
⊢ Quot.liftOn (r := Rel R X) (HSMul.hSMul (β := FreeLieAlgebra R X) t (Quot.mk (Rel R X) a))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    (liftAux R f : (a : lib R X) → CommutatorRing L) (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R) a)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Free
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 : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
b : lib R X
mk :
  Quot.liftOn (r := Rel R X) (Bracket.bracket (L := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    (liftAux R f : (a : lib R X) → CommutatorRing L) (a * b)
⊢ Quot.liftOn (r := Rel R X) (Bracket.bracket (L := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    ⁅Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) a) (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯,
      Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) b) (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯⁆

Tactic:
rw [← liftAux_map_mul]

Premises used: FreeLieAlgebra.liftAux_map_mul
-- Module: Mathlib.Algebra.Lie.Free
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 : FreeLieAlgebra R X
a : lib R X
y : FreeLieAlgebra R X
b : lib R X
⊢ Quot.liftOn (r := Rel R X) (Bracket.bracket (L := FreeLieAlgebra R X) (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b))
      (⇑(liftAux R f) : (a : lib R X) → CommutatorRing L) ⋯ =
    (liftAux R f : (a : lib R X) → CommutatorRing L) (a * b)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Free
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
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) ⋯,
                map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
              FreeLieAlgebra R X →ₗ⁅R⁆ L))
          f)
        x =
      f 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) ⋯,
              map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
            FreeLieAlgebra R X →ₗ⁅R⁆ L))
        f) =
    f

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Free
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
⊢ (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)
      x =
    f x

Tactic:
simp only [liftAux, of, LieHom.coe_mk, Function.comp_apply, lib.lift_of_apply]

Premises used: FreeLieAlgebra.of, FreeLieAlgebra.liftAux, LieHom.coe_mk, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.Free
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
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) ⋯,
                    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) :
            (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)
⊢ (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

Tactic:
ext ⟨a⟩
-- Module: Mathlib.Algebra.Lie.Free
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
x : FreeLieAlgebra R X
a : lib R X
F' : lib R X →ₙₐ[R] CommutatorRing L := F.toNonUnitalAlgHom.comp (mk R)
⊢ 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) ⋯,
                  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) :
          (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:
NonUnitalAlgHom.congr_fun (lib.lift_comp_of R F') a

Premises used: Multiset.sum, NonUnitalAlgHom.congr_fun, Multiset.foldr, Finsupp.sum, FreeLieAlgebra.of, CommutatorRing, Finset.sum, FreeNonUnitalNonAssocAlgebra.lift_comp_of
-- Module: Mathlib.Algebra.Lie.Free
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
x : FreeLieAlgebra R X
a : lib R X
F' : lib R X →ₙₐ[R] CommutatorRing L := F.toNonUnitalAlgHom.comp (mk R)
⊢ 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) ⋯,
                  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) :
          (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:
exact NonUnitalAlgHom.congr_fun (lib.lift_comp_of R F') a

Premises used: NonUnitalAlgHom.congr_fun, FreeNonUnitalNonAssocAlgebra.lift_comp_of
-- Module: Mathlib.Algebra.Lie.Free
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
⊢ Eq (α := X → L) ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F : X → L)
    (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R) : X → L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Free
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
⊢ 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) =
    f

Tactic:
(lift R).left_inv f

Premises used: FreeLieAlgebra.lift, Equiv.left_inv
-- Module: Mathlib.Algebra.Lie.Free
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
g : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ Function.comp (β := FreeLieAlgebra R X) (⇑g : (a : FreeLieAlgebra R X) → L) (of R) = f ↔
    g = (lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L) f

Tactic:
(lift R).symm_apply_eq

Premises used: FreeLieAlgebra.lift, Equiv.symm_apply_eq
-- Module: Mathlib.Algebra.Lie.Free
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
rw₁ rw₂ : f 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

Tactic:
rw [← @Function.comp_apply _ _ _ (lift R f) (of R) x, of_comp_lift]

Premises used: FreeLieAlgebra.of_comp_lift, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.Free
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
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
⊢ (lift R : (a : X → L) → FreeLieAlgebra R X →ₗ⁅R⁆ L)
      (Function.comp (β := FreeLieAlgebra R X) (⇑F : (a : FreeLieAlgebra R X) → L) (of R)) =
    F

Tactic:
rw [← lift_symm_apply]

Premises used: FreeLieAlgebra.lift_symm_apply
-- Module: Mathlib.Algebra.Lie.Free
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)
      ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F) =
    F

Tactic:
(lift R).apply_symm_apply F

Premises used: Equiv.apply_symm_apply, FreeLieAlgebra.lift
-- Module: Mathlib.Algebra.Lie.Free
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)
      ((Equiv.symm (lift R) : (a : FreeLieAlgebra R X →ₗ⁅R⁆ L) → X → L) F) =
    F

Tactic:
exact (lift R).apply_symm_apply F

Premises used: Equiv.apply_symm_apply, FreeLieAlgebra.lift
-- Module: Mathlib.Algebra.Lie.Free
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)
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Free
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)
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:
simp [h]
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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)
⊢ 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))

Tactic:
ext