awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y - s y) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L) = 0
rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L)
⊢ s' y - s y ∈ E.proj.ker
have rw₃ : y = (E.proj : (a : E.L) → L) (s y)
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y - s y) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L) = 0
rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L)
rw₃ : y = (E.proj : (a : E.L) → L) (s y)
⊢ s' y - s y ∈ E.proj.ker
have rw₄ : y = y
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
⊢ ⁅s x - s' x, s' y - s y⁆ = 0
have aux : Eq (α := ↥E.proj.ker)
  (Bracket.bracket (L := ↥E.proj.ker) (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) (s x - s' x) sorry)
    (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) (s' y - s y) sorry))
  0
Tactic: have aux := trivial_lie_zero E.proj.ker E.proj.ker
      ⟨s x - s' x, by rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]⟩
      ⟨s' y - s y, by rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
⊢ Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
have this : ∀ {s' : L → E.L} (h : LeftInverse (⇑E.proj : (a : E.L) → L) s'), ⁅s x - s' x, s' y - s y⁆ = 0
Tactic: have {s' : L → E.L} (h : LeftInverse E.proj s') : ⁅s x - s' x, s' y - s y⁆ = (0 : E.L) := by
    have aux := trivial_lie_zero E.proj.ker E.proj.ker
      ⟨s x - s' x, by rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]⟩
      ⟨s' y - s y, by rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]⟩
    simpa only [Subtype.ext_iff, LieSubmodule.coe_zero, LieIdeal.coe_bracket_of_module,
      LieSubmodule.coe_bracket] using aux
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
this : ∀ {s' : L → E.L} (h : LeftInverse (⇑E.proj : (a : E.L) → L) s'), ⁅s x - s' x, s' y - s y⁆ = 0
⊢ Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
have this₁ : ∀ {s' : L → E.L} (h : LeftInverse (⇑E.proj : (a : E.L) → L) s'), ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
Tactic: replace this {s' : L → E.L} (h : LeftInverse E.proj s') :
      ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆) := by
    simpa [sub_sub, sub_eq_zero] using this h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
this :
  ∀ {s' : L → E.L} (h : LeftInverse (⇑E.proj : (a : E.L) → L) s'),
    ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
⊢ Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
have a : HSub.hSub (β := M)
    (HSub.hSub (α := M) (β := M)
      (⁅x,
          (E.toKer.symm : (a : ↥E.proj.ker) → M)
            (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
              (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) y : E.L) ((s₂ : (a : L) → E.L) y : E.L)) sorry)⁆ :
        M)
      (⁅y,
          (E.toKer.symm : (a : ↥E.proj.ker) → M)
            (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
              (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) sorry)⁆ :
        M))
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L)) sorry) :
      M) =
  HSub.hSub (α := M) (β := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L)
            (Bracket.bracket (L := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₁ : (a : L) → E.L) y) : E.L)
            ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L))
          sorry) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L)
            (Bracket.bracket (L := E.L) ((s₂ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) y) : E.L)
            ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L))
          sorry) :
      M)
Tactic: simp only [d₁₂_apply_coe_apply_apply, oneCochainOfTwoSplitting_apply, AddSubgroupClass.coe_sub,
    twoCocycleOf_coe_coe, LinearMap.sub_apply, LinearMap.compr₂_apply, LinearMap.coe_mk,
    AddHom.coe_mk, LinearEquiv.coe_coe, LieEquiv.coe_toLinearEquiv]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a + b) (a + c)
have rw : Rel R X (b + a) (c + a)
Tactic: rw [add_comm _ b, add_comm _ c]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
S : Type u_1
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X (t • a) (t • b)
have rw : Rel R X (HSMul.hSMul (β := R) t 1 • a) (HSMul.hSMul (β := R) t 1 • b)
Tactic: rw [← smul_one_smul R t a, ← smul_one_smul R t b]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
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
⊢ 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))
have 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))
Tactic: change Quot.mk _ (a • t • c) = Quot.mk _ (t • a • c)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
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
⊢ Eq (α := Quot (α := lib R X) (Rel R X)) (Quot.mk (Rel R X) (a • t • c)) (Quot.mk (Rel R X) (t • a • c))
have 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))
Tactic: rw [← smul_comm]
-- 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
a b : lib R X
h : Rel R X a b
⊢ Eq.{w + 1} (α := 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)
have lie_self : ∀ (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: induction h with
  | lie_self a' => simp only [liftAux_map_mul, map_zero, lie_self]
  | leibniz_lie a' b' c' =>
    simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
Cleared hypotheses: h
-- 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
a b : lib R X
h : Rel R X a b
lie_self :
  ∀ (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)
⊢ Eq.{w + 1} (α := 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)
have leibniz_lie : ∀ (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: induction h with
  | lie_self a' => simp only [liftAux_map_mul, map_zero, lie_self]
  | leibniz_lie a' b' c' =>
    simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
Cleared hypotheses: h
-- 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
a b : lib R X
h : Rel R X a b
lie_self :
  ∀ (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)
leibniz_lie :
  ∀ (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)
⊢ Eq.{w + 1} (α := 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)
have smul : ∀ (b' : R) {a b : lib R X},
  Rel R X a b →
    ∀
      (h₂ :
        Eq.{w + 1} (α := 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)),
      Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • a) : CommutatorRing L)
        ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • b) : CommutatorRing L)
Tactic: induction h with
  | lie_self a' => simp only [liftAux_map_mul, map_zero, lie_self]
  | leibniz_lie a' b' c' =>
    simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
Cleared hypotheses: h
-- 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
a b : lib R X
h : Rel R X a b
lie_self :
  ∀ (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)
leibniz_lie :
  ∀ (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)
smul :
  ∀ (b' : R) {a b : lib R X},
    Rel R X a b →
      ∀
        (h₂ :
          Eq.{w + 1} (α := 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)),
        Eq.{w + 1} (α := CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • a) : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • b) : CommutatorRing L)
⊢ Eq.{w + 1} (α := 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)
have add_right : ∀ {a b : lib R X} (c' : lib R X),
  Rel R X a b →
    ∀
      (h₂ :
        Eq.{w + 1} (α := 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)),
      Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a + c') : CommutatorRing L)
        ((liftAux R f : (a : lib R X) → CommutatorRing L) (b + c') : CommutatorRing L)
Tactic: induction h with
  | lie_self a' => simp only [liftAux_map_mul, map_zero, lie_self]
  | leibniz_lie a' b' c' =>
    simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
Cleared hypotheses: h
-- 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
a b : lib R X
h : Rel R X a b
lie_self :
  ∀ (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)
leibniz_lie :
  ∀ (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)
smul :
  ∀ (b' : R) {a b : lib R X},
    Rel R X a b →
      ∀
        (h₂ :
          Eq.{w + 1} (α := 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)),
        Eq.{w + 1} (α := CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • a) : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • b) : CommutatorRing L)
add_right :
  ∀ {a b : lib R X} (c' : lib R X),
    Rel R X a b →
      ∀
        (h₂ :
          Eq.{w + 1} (α := 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)),
        Eq.{w + 1} (α := CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (a + c') : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b + c') : CommutatorRing L)
⊢ Eq.{w + 1} (α := 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)
have mul_left : ∀ (c' : lib R X) {b c : lib R X},
  Rel R X b c →
    ∀
      (h₂ :
        Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) b : 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) : CommutatorRing L)
        ((liftAux R f : (a : lib R X) → CommutatorRing L) (c' * c) : CommutatorRing L)
Tactic: induction h with
  | lie_self a' => simp only [liftAux_map_mul, map_zero, lie_self]
  | leibniz_lie a' b' c' =>
    simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
Cleared hypotheses: h
-- 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 : 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) ⋯ =
    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) ⋯
have 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) sorry =
  (liftAux R f : (a : lib R X) → CommutatorRing L) (a + b)
Tactic: rw [← liftAux_map_add]
-- 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
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) ⋯ =
    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) ⋯)
have 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) sorry =
  (liftAux R f : (a : lib R X) → CommutatorRing L) (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R) a)
Tactic: rw [← liftAux_map_smul]
-- 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 : 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) ⋯ =
    ⁅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) ⋯⁆
have 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) sorry =
  (liftAux R f : (a : lib R X) → CommutatorRing L) (a * b)
Tactic: rw [← liftAux_map_mul]