awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
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 : 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)
x y z : L
hjac :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) =
    -HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
hja :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅⁅x, y⁆, z⁆ : E.L)
    ((s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)
⊢ Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)

Tactic:
rw [← lie_skew, map_neg, neg_eq_iff_eq_neg] at hja

Premises used: neg_eq_iff_eq_neg, map_neg, lie_skew
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
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 : 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)
x y z : L
hjac :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) =
    -HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
hja :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)
⊢ Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅⁅y, x⁆, z⁆ : E.L)
    ((s : (a : L) → E.L) (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆) : E.L)

Tactic:
have hj := congr_arg s (lie_lie y x z)
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
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 : 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)
x y z : L
hjac :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) =
    -HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
hja :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)
hj :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅⁅y, x⁆, z⁆ : E.L)
    ((s : (a : L) → E.L) (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆) : E.L)
⊢ Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆) : E.L)

Tactic:
rw [← lie_skew, map_neg, neg_eq_iff_eq_neg] at hj

Premises used: neg_eq_iff_eq_neg, map_neg, lie_skew
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
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
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 : L
rw :
  HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
      ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L) =
    0
rw₁ :
  Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
    ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L)
rw₂ : x = (E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L)
rw₃ rw₄ : x = x
⊢ Eq.{u_3 + 1} (α := L)
    ((E.proj : (a : E.L) → L)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) :
      L)
    (0 : L)

Tactic:
rw [map_sub, sub_eq_zero, hs₁, hs₂]

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.Algebra.Lie.Extension
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)
a :
  ∀ (x y : L),
    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)
⊢ (d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂) =
    (↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))

Tactic:
ext x y
-- Module: Mathlib.Algebra.Lie.Extension
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
a :
  ∀ (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)
⊢ 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)

Tactic:
choose s hs using E.proj_surjective

Premises used: LieAlgebra.Extension.proj_surjective
-- Module: Mathlib.Algebra.Lie.Extension
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 x - s' x) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L) = 0
rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L)
rw₃ : (E.proj : (a : E.L) → L) (s x) = x
rw₄ rw₅ : x = x
⊢ s x - s' x ∈ E.proj.ker

Tactic:
rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]

Premises used: map_sub, sub_eq_zero, LieHom.mem_ker
-- Module: Mathlib.Algebra.Lie.Extension
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)
rw₄ rw₅ : y = y
⊢ s' y - s y ∈ E.proj.ker

Tactic:
rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]

Premises used: map_sub, sub_eq_zero, LieHom.mem_ker
-- Module: Mathlib.Algebra.Lie.Extension
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'
⊢ 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) ⋯)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) (s' y - s y) ⋯))
    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]⟩
-- Module: Mathlib.Algebra.Lie.Extension
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'
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) ⋯)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) (s' y - s y) ⋯))
    0
⊢ ⁅s x - s' x, s' y - s y⁆ = 0

Tactic:
simpa only [Subtype.ext_iff, LieSubmodule.coe_zero, LieIdeal.coe_bracket_of_module,
      LieSubmodule.coe_bracket] using aux

Premises used: LieIdeal.coe_bracket_of_module, LieSubmodule.coe_zero, Subtype.ext_iff, LieSubmodule.coe_bracket
-- Module: Mathlib.Algebra.Lie.Extension
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

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
-- Module: Mathlib.Algebra.Lie.Extension
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
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:
simpa [sub_sub, sub_eq_zero] using this h

Premises used: sub_eq_zero, sub_sub
-- Module: Mathlib.Algebra.Lie.Extension
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
⊢ ∀ {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
-- Module: Mathlib.Algebra.Lie.Extension
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⁆)
⊢ HAdd.hAdd (α := E.L) (Bracket.bracket (L := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₁ : (a : L) → E.L) y) : E.L)
            (HSub.hSub (β := E.L) ⁅s x, s y⁆ (-⁅s y, (s₁ : (a : L) → E.L) x⁆ : E.L)) -
          HAdd.hAdd (α := E.L)
            (Bracket.bracket (L := E.L) ((s₂ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) y) : E.L)
            (HSub.hSub (β := E.L) ⁅s x, s y⁆ (-⁅s y, (s₂ : (a : L) → E.L) x⁆ : E.L)) -
        HSub.hSub (α := E.L) (β := E.L) (⁅s y, (s₁ : (a : L) → E.L) x⁆ : E.L) (⁅s y, (s₂ : (a : L) → E.L) x⁆ : E.L) -
      HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L) =
    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) -
      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)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
a b c : lib R X
h : Rel R X b c
rw : Rel R X (b + a) (c + a)
⊢ Rel R X (a + b) (a + c)

Tactic:
rw [add_comm _ b, add_comm _ c]

Premises used: add_comm
-- Module: Mathlib.Algebra.Lie.Free
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 (b + a) (c + a)

Tactic:
h.add_right _

Premises used: FreeLieAlgebra.Rel.add_right
-- Module: Mathlib.Algebra.Lie.Free
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 (b + a) (c + a)

Tactic:
exact h.add_right _

Premises used: FreeLieAlgebra.Rel.add_right
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
a b : lib R X
h : Rel R X a b
⊢ Rel R X (-a) (-b)

Tactic:
simpa only [neg_one_smul] using h.smul (-1)

Premises used: neg_one_smul, OfNat.ofNat, FreeLieAlgebra.Rel.smul, Neg.neg
-- Module: Mathlib.Algebra.Lie.Free
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)

Tactic:
simpa only [sub_eq_add_neg] using h.neg.addLeft a

Premises used: FreeLieAlgebra.Rel.addLeft, sub_eq_add_neg, FreeLieAlgebra.Rel.neg
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
a b c : lib R X
h : Rel R X a b
⊢ Rel R X (a - c) (b - c)

Tactic:
simpa only [sub_eq_add_neg] using h.add_right (-c)

Premises used: FreeLieAlgebra.Rel.add_right, sub_eq_add_neg, Neg.neg
-- Module: Mathlib.Algebra.Lie.Free
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
rw : Rel R X (HSMul.hSMul (β := R) t 1 • a) (HSMul.hSMul (β := R) t 1 • b)
⊢ Rel R X (t • a) (t • b)

Tactic:
rw [← smul_one_smul R t a, ← smul_one_smul R t b]

Premises used: smul_one_smul
-- Module: Mathlib.Algebra.Lie.Free
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 (HSMul.hSMul (β := R) t 1 • a) (HSMul.hSMul (β := R) t 1 • b)

Tactic:
h.smul _

Premises used: FreeLieAlgebra.Rel.smul
-- Module: Mathlib.Algebra.Lie.Free
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 (HSMul.hSMul (β := R) t 1 • a) (HSMul.hSMul (β := R) t 1 • b)

Tactic:
exact h.smul _

Premises used: FreeLieAlgebra.Rel.smul
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
⊢ Inhabited (Quot (α := lib R X) (FreeLieAlgebra.Rel R X))

Tactic:
infer_instance
-- 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
mk mk₁ : Eq (α := Quot (α := lib R X) (Rel R X)) (Quot.mk (Rel R X) ((a + b) * c)) (Quot.mk (Rel R X) (a * c + b * c))
⊢ Eq (α := Quot (α := lib R X) (Rel R X))
    (Quot.mk (Rel R X) ((fun (x1 x2 : lib R X) ↦ x1 * x2) ((fun (x1 x2 : lib R X) ↦ x1 + x2) a b) c))
    (Quot.mk (Rel R X)
      ((fun (x1 x2 : lib R X) ↦ x1 + x2) ((fun (x1 x2 : lib R X) ↦ x1 * x2) a c)
        ((fun (x1 x2 : lib R X) ↦ x1 * x2) b c)))

Tactic:
simp_rw [add_mul]

Premises used: add_mul
-- 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
mk mk₁ : Eq (α := Quot (α := lib R X) (Rel R X)) (Quot.mk (Rel R X) (a * (b + c))) (Quot.mk (Rel R X) (a * b + a * c))
⊢ Eq (α := Quot (α := lib R X) (Rel R X))
    (Quot.mk (Rel R X) ((fun (x1 x2 : lib R X) ↦ x1 * x2) a ((fun (x1 x2 : lib R X) ↦ x1 + x2) b c)))
    (Quot.mk (Rel R X)
      ((fun (x1 x2 : lib R X) ↦ x1 + x2) ((fun (x1 x2 : lib R X) ↦ x1 * x2) a b)
        ((fun (x1 x2 : lib R X) ↦ x1 * x2) a c)))

Tactic:
simp_rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
x : FreeLieAlgebra R X
a : lib R X
⊢ Eq (α := 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.mk (Rel R X) a)
      (Quot.mk (Rel R X) a))
    0

Tactic:
Quot.sound (Rel.lie_self a)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeLieAlgebra, FreeLieAlgebra.Rel.lie_self
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
x : FreeLieAlgebra R X
a : lib R X
⊢ Eq (α := 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.mk (Rel R X) a)
      (Quot.mk (Rel R X) a))
    0

Tactic:
exact Quot.sound (Rel.lie_self a)

Premises used: Quot.sound, FreeLieAlgebra.Rel.lie_self
-- 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:
Quot.sound (Rel.leibniz_lie a b c)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeLieAlgebra.Rel.leibniz_lie, FreeLieAlgebra