mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝³ : R
x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ (↑⟨{
              toFun := fun x ↦
                { toFun := fun y ↦ ⁅x, (x✝³ • x✝²) y⁆ - ⁅y, (x✝³ • x✝²) x⁆ - (x✝³ • x✝²) ⁅x, y⁆, map_add' := ⋯,
                  map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ },
            ⋯⟩
        x✝¹)
      x✝ =
    (↑((RingHom.id R) x✝³ •
            ⟨{
                toFun := fun x ↦
                  { toFun := fun y ↦ ⁅x, x✝² y⁆ - ⁅y, x✝² x⁆ - x✝² ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩)
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝³ : R
x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ (↑⟨{
              toFun := fun x ↦
                { toFun := fun y ↦ ⁅x, (x✝³ • x✝²) y⁆ - ⁅y, (x✝³ • x✝²) x⁆ - (x✝³ • x✝²) ⁅x, y⁆, map_add' := ⋯,
                  map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ },
            ⋯⟩
        x✝¹)
      x✝ =
    (↑((RingHom.id R) x✝³ •
            ⟨{
                toFun := fun x ↦
                  { toFun := fun y ↦ ⁅x, x✝² y⁆ - ⁅y, x✝² x⁆ - x✝² ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩)
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y x✝¹ x✝ : L
⊢ ⁅x, (a y) x✝¹⁆ + ⁅x, (a y) x✝⁆ - (⁅y, (a x) x✝¹⁆ + ⁅y, (a x) x✝⁆) + (⁅x✝¹, (a x) y⁆ + ⁅x✝, (a x) y⁆) -
          ((a ⁅x, y⁆) x✝¹ + (a ⁅x, y⁆) x✝) +
        ((a ⁅x, x✝¹⁆) y + (a ⁅x, x✝⁆) y) -
      ((a ⁅y, x✝¹⁆) x + (a ⁅y, x✝⁆) x) =
    ⁅x, (a y) x✝¹⁆ - ⁅y, (a x) x✝¹⁆ + ⁅x✝¹, (a x) y⁆ - (a ⁅x, y⁆) x✝¹ + (a ⁅x, x✝¹⁆) y - (a ⁅y, x✝¹⁆) x +
      (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y x✝¹ x✝ : L
⊢ ⁅x, (a y) x✝¹⁆ + ⁅x, (a y) x✝⁆ - (⁅y, (a x) x✝¹⁆ + ⁅y, (a x) x✝⁆) + (⁅x✝¹, (a x) y⁆ + ⁅x✝, (a x) y⁆) -
          ((a ⁅x, y⁆) x✝¹ + (a ⁅x, y⁆) x✝) +
        ((a ⁅x, x✝¹⁆) y + (a ⁅x, x✝⁆) y) -
      ((a ⁅y, x✝¹⁆) x + (a ⁅y, x✝⁆) x) =
    ⁅x, (a y) x✝¹⁆ - ⁅y, (a x) x✝¹⁆ + ⁅x✝¹, (a x) y⁆ - (a ⁅x, y⁆) x✝¹ + (a ⁅x, x✝¹⁆) y - (a ⁅y, x✝¹⁆) x +
      (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y : L
x✝¹ : R
x✝ : L
⊢ x✝¹ • ⁅x, (a y) x✝⁆ - x✝¹ • ⁅y, (a x) x✝⁆ + x✝¹ • ⁅x✝, (a x) y⁆ - x✝¹ • (a ⁅x, y⁆) x✝ + x✝¹ • (a ⁅x, x✝⁆) y -
      x✝¹ • (a ⁅y, x✝⁆) x =
    x✝¹ • (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y : L
x✝¹ : R
x✝ : L
⊢ x✝¹ • ⁅x, (a y) x✝⁆ - x✝¹ • ⁅y, (a x) x✝⁆ + x✝¹ • ⁅x✝, (a x) y⁆ - x✝¹ • (a ⁅x, y⁆) x✝ + x✝¹ • (a ⁅x, x✝⁆) y -
      x✝¹ • (a ⁅y, x✝⁆) x =
    x✝¹ • (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y : L
x✝¹ : R
x✝ : L
⊢ x✝¹ • ⁅x, (a y) x✝⁆ +
      (-1 • x✝¹ • ⁅y, (a x) x✝⁆ +
        (x✝¹ • ⁅x✝, (a x) y⁆ + (-1 • x✝¹ • (a ⁅x, y⁆) x✝ + (x✝¹ • (a ⁅x, x✝⁆) y + -1 • x✝¹ • (a ⁅y, x✝⁆) x)))) =
    x✝¹ •
      (⁅x, (a y) x✝⁆ +
        (-1 • ⁅y, (a x) x✝⁆ + (⁅x✝, (a x) y⁆ + (-1 • (a ⁅x, y⁆) x✝ + ((a ⁅x, x✝⁆) y + -1 • (a ⁅y, x✝⁆) x)))))

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y : L
x✝¹ : R
x✝ : L
⊢ x✝¹ • ⁅x, (a y) x✝⁆ +
      (-1 • x✝¹ • ⁅y, (a x) x✝⁆ +
        (x✝¹ • ⁅x✝, (a x) y⁆ + (-1 • x✝¹ • (a ⁅x, y⁆) x✝ + (x✝¹ • (a ⁅x, x✝⁆) y + -1 • x✝¹ • (a ⁅y, x✝⁆) x)))) =
    x✝¹ •
      (⁅x, (a y) x✝⁆ +
        (-1 • ⁅y, (a x) x✝⁆ + (⁅x✝, (a x) y⁆ + (-1 • (a ⁅x, y⁆) x✝ + ((a ⁅x, x✝⁆) y + -1 • (a ⁅y, x✝⁆) x)))))
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x x✝² x✝¹ x✝ : L
⊢ {
        toFun := fun z ↦
          ⁅x, (a (x✝² + x✝¹)) z⁆ - ⁅x✝² + x✝¹, (a x) z⁆ + ⁅z, (a x) (x✝² + x✝¹)⁆ - (a ⁅x, x✝² + x✝¹⁆) z +
              (a ⁅x, z⁆) (x✝² + x✝¹) -
            (a ⁅x✝² + x✝¹, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }
      x✝ =
    ({
          toFun := fun z ↦
            ⁅x, (a x✝²) z⁆ - ⁅x✝², (a x) z⁆ + ⁅z, (a x) x✝²⁆ - (a ⁅x, x✝²⁆) z + (a ⁅x, z⁆) x✝² - (a ⁅x✝², z⁆) x,
          map_add' := ⋯, map_smul' := ⋯ } +
        {
          toFun := fun z ↦
            ⁅x, (a x✝¹) z⁆ - ⁅x✝¹, (a x) z⁆ + ⁅z, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) z + (a ⁅x, z⁆) x✝¹ - (a ⁅x✝¹, z⁆) x,
          map_add' := ⋯, map_smul' := ⋯ })
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x x✝² x✝¹ x✝ : L
⊢ {
        toFun := fun z ↦
          ⁅x, (a (x✝² + x✝¹)) z⁆ - ⁅x✝² + x✝¹, (a x) z⁆ + ⁅z, (a x) (x✝² + x✝¹)⁆ - (a ⁅x, x✝² + x✝¹⁆) z +
              (a ⁅x, z⁆) (x✝² + x✝¹) -
            (a ⁅x✝² + x✝¹, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }
      x✝ =
    ({
          toFun := fun z ↦
            ⁅x, (a x✝²) z⁆ - ⁅x✝², (a x) z⁆ + ⁅z, (a x) x✝²⁆ - (a ⁅x, x✝²⁆) z + (a ⁅x, z⁆) x✝² - (a ⁅x✝², z⁆) x,
          map_add' := ⋯, map_smul' := ⋯ } +
        {
          toFun := fun z ↦
            ⁅x, (a x✝¹) z⁆ - ⁅x✝¹, (a x) z⁆ + ⁅z, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) z + (a ⁅x, z⁆) x✝¹ - (a ⁅x✝¹, z⁆) x,
          map_add' := ⋯, map_smul' := ⋯ })
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x x✝² x✝¹ x✝ : L
⊢ ⁅x, (a x✝²) x✝⁆ + ⁅x, (a x✝¹) x✝⁆ - (⁅x✝², (a x) x✝⁆ + ⁅x✝¹, (a x) x✝⁆) + (⁅x✝, (a x) x✝²⁆ + ⁅x✝, (a x) x✝¹⁆) -
          ((a ⁅x, x✝²⁆) x✝ + (a ⁅x, x✝¹⁆) x✝) +
        ((a ⁅x, x✝⁆) x✝² + (a ⁅x, x✝⁆) x✝¹) -
      ((a ⁅x✝², x✝⁆) x + (a ⁅x✝¹, x✝⁆) x) =
    ⁅x, (a x✝²) x✝⁆ - ⁅x✝², (a x) x✝⁆ + ⁅x✝, (a x) x✝²⁆ - (a ⁅x, x✝²⁆) x✝ + (a ⁅x, x✝⁆) x✝² - (a ⁅x✝², x✝⁆) x +
      (⁅x, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x) x✝⁆ + ⁅x✝, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) x✝ + (a ⁅x, x✝⁆) x✝¹ - (a ⁅x✝¹, x✝⁆) x)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x x✝² x✝¹ x✝ : L
⊢ ⁅x, (a x✝²) x✝⁆ + ⁅x, (a x✝¹) x✝⁆ - (⁅x✝², (a x) x✝⁆ + ⁅x✝¹, (a x) x✝⁆) + (⁅x✝, (a x) x✝²⁆ + ⁅x✝, (a x) x✝¹⁆) -
          ((a ⁅x, x✝²⁆) x✝ + (a ⁅x, x✝¹⁆) x✝) +
        ((a ⁅x, x✝⁆) x✝² + (a ⁅x, x✝⁆) x✝¹) -
      ((a ⁅x✝², x✝⁆) x + (a ⁅x✝¹, x✝⁆) x) =
    ⁅x, (a x✝²) x✝⁆ - ⁅x✝², (a x) x✝⁆ + ⁅x✝, (a x) x✝²⁆ - (a ⁅x, x✝²⁆) x✝ + (a ⁅x, x✝⁆) x✝² - (a ⁅x✝², x✝⁆) x +
      (⁅x, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x) x✝⁆ + ⁅x✝, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) x✝ + (a ⁅x, x✝⁆) x✝¹ - (a ⁅x✝¹, x✝⁆) x)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x : L
x✝² : R
x✝¹ x✝ : L
⊢ {
        toFun := fun z ↦
          ⁅x, (a (x✝² • x✝¹)) z⁆ - ⁅x✝² • x✝¹, (a x) z⁆ + ⁅z, (a x) (x✝² • x✝¹)⁆ - (a ⁅x, x✝² • x✝¹⁆) z +
              (a ⁅x, z⁆) (x✝² • x✝¹) -
            (a ⁅x✝² • x✝¹, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }
      x✝ =
    ((RingHom.id R) x✝² •
        {
          toFun := fun z ↦
            ⁅x, (a x✝¹) z⁆ - ⁅x✝¹, (a x) z⁆ + ⁅z, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) z + (a ⁅x, z⁆) x✝¹ - (a ⁅x✝¹, z⁆) x,
          map_add' := ⋯, map_smul' := ⋯ })
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x : L
x✝² : R
x✝¹ x✝ : L
⊢ {
        toFun := fun z ↦
          ⁅x, (a (x✝² • x✝¹)) z⁆ - ⁅x✝² • x✝¹, (a x) z⁆ + ⁅z, (a x) (x✝² • x✝¹)⁆ - (a ⁅x, x✝² • x✝¹⁆) z +
              (a ⁅x, z⁆) (x✝² • x✝¹) -
            (a ⁅x✝² • x✝¹, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }
      x✝ =
    ((RingHom.id R) x✝² •
        {
          toFun := fun z ↦
            ⁅x, (a x✝¹) z⁆ - ⁅x✝¹, (a x) z⁆ + ⁅z, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) z + (a ⁅x, z⁆) x✝¹ - (a ⁅x✝¹, z⁆) x,
          map_add' := ⋯, map_smul' := ⋯ })
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x : L
x✝² : R
x✝¹ x✝ : L
⊢ x✝² • ⁅x, (a x✝¹) x✝⁆ - x✝² • ⁅x✝¹, (a x) x✝⁆ + x✝² • ⁅x✝, (a x) x✝¹⁆ - x✝² • (a ⁅x, x✝¹⁆) x✝ +
        x✝² • (a ⁅x, x✝⁆) x✝¹ -
      x✝² • (a ⁅x✝¹, x✝⁆) x =
    x✝² • (⁅x, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x) x✝⁆ + ⁅x✝, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) x✝ + (a ⁅x, x✝⁆) x✝¹ - (a ⁅x✝¹, x✝⁆) x)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x : L
x✝² : R
x✝¹ x✝ : L
⊢ x✝² • ⁅x, (a x✝¹) x✝⁆ - x✝² • ⁅x✝¹, (a x) x✝⁆ + x✝² • ⁅x✝, (a x) x✝¹⁆ - x✝² • (a ⁅x, x✝¹⁆) x✝ +
        x✝² • (a ⁅x, x✝⁆) x✝¹ -
      x✝² • (a ⁅x✝¹, x✝⁆) x =
    x✝² • (⁅x, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x) x✝⁆ + ⁅x✝, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) x✝ + (a ⁅x, x✝⁆) x✝¹ - (a ⁅x✝¹, x✝⁆) x)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x : L
x✝² : R
x✝¹ x✝ : L
⊢ x✝² • ⁅x, (a x✝¹) x✝⁆ +
      (-1 • x✝² • ⁅x✝¹, (a x) x✝⁆ +
        (x✝² • ⁅x✝, (a x) x✝¹⁆ + (-1 • x✝² • (a ⁅x, x✝¹⁆) x✝ + (x✝² • (a ⁅x, x✝⁆) x✝¹ + -1 • x✝² • (a ⁅x✝¹, x✝⁆) x)))) =
    x✝² •
      (⁅x, (a x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (a x) x✝⁆ + (⁅x✝, (a x) x✝¹⁆ + (-1 • (a ⁅x, x✝¹⁆) x✝ + ((a ⁅x, x✝⁆) x✝¹ + -1 • (a ⁅x✝¹, x✝⁆) x)))))

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x : L
x✝² : R
x✝¹ x✝ : L
⊢ x✝² • ⁅x, (a x✝¹) x✝⁆ +
      (-1 • x✝² • ⁅x✝¹, (a x) x✝⁆ +
        (x✝² • ⁅x✝, (a x) x✝¹⁆ + (-1 • x✝² • (a ⁅x, x✝¹⁆) x✝ + (x✝² • (a ⁅x, x✝⁆) x✝¹ + -1 • x✝² • (a ⁅x✝¹, x✝⁆) x)))) =
    x✝² •
      (⁅x, (a x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (a x) x✝⁆ + (⁅x✝, (a x) x✝¹⁆ + (-1 • (a ⁅x, x✝¹⁆) x✝ + ((a ⁅x, x✝⁆) x✝¹ + -1 • (a ⁅x✝¹, x✝⁆) x)))))
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ x✝² x✝¹ x✝ : L
⊢ ({
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x✝³ + x✝², (a y) z⁆ - ⁅y, (a (x✝³ + x✝²)) z⁆ + ⁅z, (a (x✝³ + x✝²)) y⁆ - (a ⁅x✝³ + x✝², y⁆) z +
                    (a ⁅x✝³ + x✝², z⁆) y -
                  (a ⁅y, z⁆) (x✝³ + x✝²),
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ }
        x✝¹)
      x✝ =
    (({
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝³, (a y) z⁆ - ⁅y, (a x✝³) z⁆ + ⁅z, (a x✝³) y⁆ - (a ⁅x✝³, y⁆) z + (a ⁅x✝³, z⁆) y - (a ⁅y, z⁆) x✝³,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } +
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝², (a y) z⁆ - ⁅y, (a x✝²) z⁆ + ⁅z, (a x✝²) y⁆ - (a ⁅x✝², y⁆) z + (a ⁅x✝², z⁆) y - (a ⁅y, z⁆) x✝²,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ x✝² x✝¹ x✝ : L
⊢ ({
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x✝³ + x✝², (a y) z⁆ - ⁅y, (a (x✝³ + x✝²)) z⁆ + ⁅z, (a (x✝³ + x✝²)) y⁆ - (a ⁅x✝³ + x✝², y⁆) z +
                    (a ⁅x✝³ + x✝², z⁆) y -
                  (a ⁅y, z⁆) (x✝³ + x✝²),
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ }
        x✝¹)
      x✝ =
    (({
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝³, (a y) z⁆ - ⁅y, (a x✝³) z⁆ + ⁅z, (a x✝³) y⁆ - (a ⁅x✝³, y⁆) z + (a ⁅x✝³, z⁆) y - (a ⁅y, z⁆) x✝³,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } +
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝², (a y) z⁆ - ⁅y, (a x✝²) z⁆ + ⁅z, (a x✝²) y⁆ - (a ⁅x✝², y⁆) z + (a ⁅x✝², z⁆) y - (a ⁅y, z⁆) x✝²,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fintype m
A : Matrix m n R
⊢ (A * Aᵀ).rank = A.rank

Tactic:
by
  simpa only [rank_transpose, transpose_transpose] using rank_transpose_mul_self Aᵀ

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ x✝² x✝¹ x✝ : L
⊢ ⁅x✝³, (a x✝¹) x✝⁆ + ⁅x✝², (a x✝¹) x✝⁆ - (⁅x✝¹, (a x✝³) x✝⁆ + ⁅x✝¹, (a x✝²) x✝⁆) +
            (⁅x✝, (a x✝³) x✝¹⁆ + ⁅x✝, (a x✝²) x✝¹⁆) -
          ((a ⁅x✝³, x✝¹⁆) x✝ + (a ⁅x✝², x✝¹⁆) x✝) +
        ((a ⁅x✝³, x✝⁆) x✝¹ + (a ⁅x✝², x✝⁆) x✝¹) -
      ((a ⁅x✝¹, x✝⁆) x✝³ + (a ⁅x✝¹, x✝⁆) x✝²) =
    ⁅x✝³, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝³) x✝⁆ + ⁅x✝, (a x✝³) x✝¹⁆ - (a ⁅x✝³, x✝¹⁆) x✝ + (a ⁅x✝³, x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝³ +
      (⁅x✝², (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝²) x✝⁆ + ⁅x✝, (a x✝²) x✝¹⁆ - (a ⁅x✝², x✝¹⁆) x✝ + (a ⁅x✝², x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝²)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ x✝² x✝¹ x✝ : L
⊢ ⁅x✝³, (a x✝¹) x✝⁆ + ⁅x✝², (a x✝¹) x✝⁆ - (⁅x✝¹, (a x✝³) x✝⁆ + ⁅x✝¹, (a x✝²) x✝⁆) +
            (⁅x✝, (a x✝³) x✝¹⁆ + ⁅x✝, (a x✝²) x✝¹⁆) -
          ((a ⁅x✝³, x✝¹⁆) x✝ + (a ⁅x✝², x✝¹⁆) x✝) +
        ((a ⁅x✝³, x✝⁆) x✝¹ + (a ⁅x✝², x✝⁆) x✝¹) -
      ((a ⁅x✝¹, x✝⁆) x✝³ + (a ⁅x✝¹, x✝⁆) x✝²) =
    ⁅x✝³, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝³) x✝⁆ + ⁅x✝, (a x✝³) x✝¹⁆ - (a ⁅x✝³, x✝¹⁆) x✝ + (a ⁅x✝³, x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝³ +
      (⁅x✝², (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝²) x✝⁆ + ⁅x✝, (a x✝²) x✝¹⁆ - (a ⁅x✝², x✝¹⁆) x✝ + (a ⁅x✝², x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝²)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ ({
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x✝³ • x✝², (a y) z⁆ - ⁅y, (a (x✝³ • x✝²)) z⁆ + ⁅z, (a (x✝³ • x✝²)) y⁆ - (a ⁅x✝³ • x✝², y⁆) z +
                    (a ⁅x✝³ • x✝², z⁆) y -
                  (a ⁅y, z⁆) (x✝³ • x✝²),
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ }
        x✝¹)
      x✝ =
    (((RingHom.id R) x✝³ •
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝², (a y) z⁆ - ⁅y, (a x✝²) z⁆ + ⁅z, (a x✝²) y⁆ - (a ⁅x✝², y⁆) z + (a ⁅x✝², z⁆) y - (a ⁅y, z⁆) x✝²,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ ({
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x✝³ • x✝², (a y) z⁆ - ⁅y, (a (x✝³ • x✝²)) z⁆ + ⁅z, (a (x✝³ • x✝²)) y⁆ - (a ⁅x✝³ • x✝², y⁆) z +
                    (a ⁅x✝³ • x✝², z⁆) y -
                  (a ⁅y, z⁆) (x✝³ • x✝²),
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ }
        x✝¹)
      x✝ =
    (((RingHom.id R) x✝³ •
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x✝², (a y) z⁆ - ⁅y, (a x✝²) z⁆ + ⁅z, (a x✝²) y⁆ - (a ⁅x✝², y⁆) z + (a ⁅x✝², z⁆) y - (a ⁅y, z⁆) x✝²,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ x✝³ • ⁅x✝², (a x✝¹) x✝⁆ - x✝³ • ⁅x✝¹, (a x✝²) x✝⁆ + x✝³ • ⁅x✝, (a x✝²) x✝¹⁆ - x✝³ • (a ⁅x✝², x✝¹⁆) x✝ +
        x✝³ • (a ⁅x✝², x✝⁆) x✝¹ -
      x✝³ • (a ⁅x✝¹, x✝⁆) x✝² =
    x✝³ •
      (⁅x✝², (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝²) x✝⁆ + ⁅x✝, (a x✝²) x✝¹⁆ - (a ⁅x✝², x✝¹⁆) x✝ + (a ⁅x✝², x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝²)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ x✝³ • ⁅x✝², (a x✝¹) x✝⁆ - x✝³ • ⁅x✝¹, (a x✝²) x✝⁆ + x✝³ • ⁅x✝, (a x✝²) x✝¹⁆ - x✝³ • (a ⁅x✝², x✝¹⁆) x✝ +
        x✝³ • (a ⁅x✝², x✝⁆) x✝¹ -
      x✝³ • (a ⁅x✝¹, x✝⁆) x✝² =
    x✝³ •
      (⁅x✝², (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝²) x✝⁆ + ⁅x✝, (a x✝²) x✝¹⁆ - (a ⁅x✝², x✝¹⁆) x✝ + (a ⁅x✝², x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝²)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ x✝³ • ⁅x✝², (a x✝¹) x✝⁆ +
      (-1 • x✝³ • ⁅x✝¹, (a x✝²) x✝⁆ +
        (x✝³ • ⁅x✝, (a x✝²) x✝¹⁆ +
          (-1 • x✝³ • (a ⁅x✝², x✝¹⁆) x✝ + (x✝³ • (a ⁅x✝², x✝⁆) x✝¹ + -1 • x✝³ • (a ⁅x✝¹, x✝⁆) x✝²)))) =
    x✝³ •
      (⁅x✝², (a x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (a x✝²) x✝⁆ +
          (⁅x✝, (a x✝²) x✝¹⁆ + (-1 • (a ⁅x✝², x✝¹⁆) x✝ + ((a ⁅x✝², x✝⁆) x✝¹ + -1 • (a ⁅x✝¹, x✝⁆) x✝²)))))

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x✝³ : R
x✝² x✝¹ x✝ : L
⊢ x✝³ • ⁅x✝², (a x✝¹) x✝⁆ +
      (-1 • x✝³ • ⁅x✝¹, (a x✝²) x✝⁆ +
        (x✝³ • ⁅x✝, (a x✝²) x✝¹⁆ +
          (-1 • x✝³ • (a ⁅x✝², x✝¹⁆) x✝ + (x✝³ • (a ⁅x✝², x✝⁆) x✝¹ + -1 • x✝³ • (a ⁅x✝¹, x✝⁆) x✝²)))) =
    x✝³ •
      (⁅x✝², (a x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (a x✝²) x✝⁆ +
          (⁅x✝, (a x✝²) x✝¹⁆ + (-1 • (a ⁅x✝², x✝¹⁆) x✝ + ((a ⁅x✝², x✝⁆) x✝¹ + -1 • (a ⁅x✝¹, x✝⁆) x✝²)))))
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝⁴ x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ ⁅x✝², (x✝⁴ x✝¹) x✝⁆ + ⁅x✝², (x✝³ x✝¹) x✝⁆ - (⁅x✝¹, (x✝⁴ x✝²) x✝⁆ + ⁅x✝¹, (x✝³ x✝²) x✝⁆) +
            (⁅x✝, (x✝⁴ x✝²) x✝¹⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆) -
          ((x✝⁴ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝¹⁆) x✝) +
        ((x✝⁴ ⁅x✝², x✝⁆) x✝¹ + (x✝³ ⁅x✝², x✝⁆) x✝¹) -
      ((x✝⁴ ⁅x✝¹, x✝⁆) x✝² + (x✝³ ⁅x✝¹, x✝⁆) x✝²) =
    ⁅x✝², (x✝⁴ x✝¹) x✝⁆ - ⁅x✝¹, (x✝⁴ x✝²) x✝⁆ + ⁅x✝, (x✝⁴ x✝²) x✝¹⁆ - (x✝⁴ ⁅x✝², x✝¹⁆) x✝ + (x✝⁴ ⁅x✝², x✝⁆) x✝¹ -
        (x✝⁴ ⁅x✝¹, x✝⁆) x✝² +
      (⁅x✝², (x✝³ x✝¹) x✝⁆ - ⁅x✝¹, (x✝³ x✝²) x✝⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆ - (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝⁆) x✝¹ -
        (x✝³ ⁅x✝¹, x✝⁆) x✝²)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝⁴ x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ ⁅x✝², (x✝⁴ x✝¹) x✝⁆ + ⁅x✝², (x✝³ x✝¹) x✝⁆ - (⁅x✝¹, (x✝⁴ x✝²) x✝⁆ + ⁅x✝¹, (x✝³ x✝²) x✝⁆) +
            (⁅x✝, (x✝⁴ x✝²) x✝¹⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆) -
          ((x✝⁴ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝¹⁆) x✝) +
        ((x✝⁴ ⁅x✝², x✝⁆) x✝¹ + (x✝³ ⁅x✝², x✝⁆) x✝¹) -
      ((x✝⁴ ⁅x✝¹, x✝⁆) x✝² + (x✝³ ⁅x✝¹, x✝⁆) x✝²) =
    ⁅x✝², (x✝⁴ x✝¹) x✝⁆ - ⁅x✝¹, (x✝⁴ x✝²) x✝⁆ + ⁅x✝, (x✝⁴ x✝²) x✝¹⁆ - (x✝⁴ ⁅x✝², x✝¹⁆) x✝ + (x✝⁴ ⁅x✝², x✝⁆) x✝¹ -
        (x✝⁴ ⁅x✝¹, x✝⁆) x✝² +
      (⁅x✝², (x✝³ x✝¹) x✝⁆ - ⁅x✝¹, (x✝³ x✝²) x✝⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆ - (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝⁆) x✝¹ -
        (x✝³ ⁅x✝¹, x✝⁆) x✝²)