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
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 x_1 x_2 : L
simp :
  HAdd.hAdd (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_2) : E.L) -
      HAdd.hAdd (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) ((s : (a : L) → E.L) ⁅x, x_2⁆ : 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) x_1) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1⁆ : 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) x_2) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L)
⊢ 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) (x_1 + x_2)) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1 + x_2⁆ : E.L))
      ⋯ =
    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) x_1) : E.L)
          ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L))
        ⋯ +
      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) x_2) : E.L)
          ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L))
        ⋯

Tactic:
simp
-- 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 : 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 x_1 x_2 : L
⊢ HAdd.hAdd (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_2) : E.L) -
      HAdd.hAdd (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) ((s : (a : L) → E.L) ⁅x, x_2⁆ : 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) x_1) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1⁆ : 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) x_2) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L)

Tactic:
abel
-- 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 : 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 : L
x_1 : R
x_2 : L
⊢ 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) (x_1 • x_2)) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1 • x_2⁆ : E.L))
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x_1 : R)
      (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) x_2) : E.L)
          ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L))
        ⋯)

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- 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 : 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 x_1 : L
h :
  HAdd.hAdd (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) x_1) : E.L) -
      HAdd.hAdd (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) ((s : (a : L) → E.L) ⁅y, x_1⁆ : 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) x_1) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) +
      HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) x_1) : E.L)
        ((s : (a : L) → E.L) ⁅y, x_1⁆ : E.L)
⊢ Eq.{u_5 + 1} (α := E.L)
    (↑(({
              toFun := fun (y_1 : L) ↦
                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 + y) : E.L) ((s : (a : L) → E.L) y_1) : E.L)
                    ((s : (a : L) → E.L) ⁅x + y, y_1⁆ : E.L))
                  ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : L) → ↥E.proj.ker)
          x_1) :
      E.L)
    (↑((HAdd.hAdd (α := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
              {
                toFun := fun (y : L) ↦
                  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))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }
              {
                toFun := fun (y_1 : L) ↦
                  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) y : E.L) ((s : (a : L) → E.L) y_1) : E.L)
                      ((s : (a : L) → E.L) ⁅y, y_1⁆ : E.L))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker } :
            (a : L) → ↥E.proj.ker)
          x_1) :
      E.L)

Tactic:
simp
-- 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 : 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 x_1 : L
⊢ HAdd.hAdd (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) x_1) : E.L) -
      HAdd.hAdd (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) ((s : (a : L) → E.L) ⁅y, x_1⁆ : 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) x_1) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) +
      HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) x_1) : E.L)
        ((s : (a : L) → E.L) ⁅y, x_1⁆ : E.L)

Tactic:
abel
-- 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 : 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 : R
x_1 : L
h :
  ∀ (x_2 : L),
    Eq.{u_5 + 1} (α := E.L)
      (↑(({
                toFun := fun (y : L) ↦
                  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 • x_1) : E.L) ((s : (a : L) → E.L) y) : E.L)
                      ((s : (a : L) → E.L) ⁅x • x_1, y⁆ : E.L))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : L) → ↥E.proj.ker)
            x_2) :
        E.L)
      (↑((HSMul.hSMul (α := R) (β := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
                ((RingHom.id R : (a : R) → R) x : R)
                {
                  toFun := fun (y : L) ↦
                    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_1 : E.L) ((s : (a : L) → E.L) y) : E.L)
                        ((s : (a : L) → E.L) ⁅x_1, y⁆ : E.L))
                      ⋯,
                  map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker } :
              (a : L) → ↥E.proj.ker)
            x_2) :
        E.L)
⊢ {
      toFun := fun (y : L) ↦
        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 • x_1) : E.L) ((s : (a : L) → E.L) y) : E.L)
            ((s : (a : L) → E.L) ⁅x • x_1, y⁆ : E.L))
          ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
      ((RingHom.id R : (a : R) → R) x : R)
      {
        toFun := fun (y : L) ↦
          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_1 : E.L) ((s : (a : L) → E.L) y) : E.L)
              ((s : (a : L) → E.L) ⁅x_1, y⁆ : E.L))
            ⋯,
        map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }

Tactic:
ext
-- 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 : 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 : R
x_1 x_2 : L
⊢ Eq.{u_5 + 1} (α := E.L)
    (↑(({
              toFun := fun (y : L) ↦
                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 • x_1) : E.L) ((s : (a : L) → E.L) y) : E.L)
                    ((s : (a : L) → E.L) ⁅x • x_1, y⁆ : E.L))
                  ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : L) → ↥E.proj.ker)
          x_2) :
      E.L)
    (↑((HSMul.hSMul (α := R) (β := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
              ((RingHom.id R : (a : R) → R) x : R)
              {
                toFun := fun (y : L) ↦
                  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_1 : E.L) ((s : (a : L) → E.L) y) : E.L)
                      ((s : (a : L) → E.L) ⁅x_1, y⁆ : E.L))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker } :
            (a : L) → ↥E.proj.ker)
          x_2) :
      E.L)

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- 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)
⊢ Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M)
    ((E.twoCocycleAux hs).compr₂ (↑E.toKer.symm.toLinearEquiv : ↥E.proj.ker →ₗ[R] M))

Tactic:
simp
-- 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)
h :
  ∀ (x y z : L),
    Eq.{u_4 + 1} (α := M)
      ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
                            (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
                              Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
                              ((E.twoCocycleAux hs).compr₂ (↑E.toKer.symm.toLinearEquiv : ↥E.proj.ker →ₗ[R] M)) ⋯) :
                          L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                        (a : L) → L →ₗ[R] L →ₗ[R] M)
                      x :
                    L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                y :
              L →ₗ[R] M) :
            (a : L) → M)
          z :
        M)
      ((((((0 : (a : L) → L →ₗ[R] L →ₗ[R] M) x : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M)
          z :
        M)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M)
    (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
      Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
      ((E.twoCocycleAux hs).compr₂ (↑E.toKer.symm.toLinearEquiv : ↥E.proj.ker →ₗ[R] M)) ⋯)

Tactic:
ext x y 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
this :
  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) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := 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)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (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)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
u : L
v : ↥E.proj.ker
rw :
  Bracket.bracket (L := E.L)
      ((s : (a : L) → E.L)
          ((E.proj : (a : E.L) → L)
            (Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u)) :
        E.L)
      v =
    Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
rw₁ rw₂ :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v =
    Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
⊢ ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u, v⁆ =
    Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v

Tactic:
rw [← E.lie_apply_proj_of_leftInverse_eq hs, h.choose_spec _]

Premises used: Exists.choose_spec, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq
-- 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
this :
  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) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := 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)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (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)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
⊢ ∀ (u : L) (v : ↥E.proj.ker),
    ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u, v⁆ =
      Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v

Tactic:
have aux (u : L) (v : E.proj.ker) : ⁅h.choose u, v⁆ = ⁅s u, v⁆ := by
        rw [← E.lie_apply_proj_of_leftInverse_eq hs, h.choose_spec _]
-- 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
⊢ Bracket.bracket (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) z) =
    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)

Tactic:
have hjac := lie_lie (s x) (s y) (s 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) (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) z) =
    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)
⊢ 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)

Tactic:
rw [← lie_skew, neg_eq_iff_eq_neg] at hjac

Premises used: neg_eq_iff_eq_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)
⊢ 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)

Tactic:
have hja := congr_arg s (lie_lie x y z)