awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
h :
  ∀ (hmn : m ≤ n),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
h₁ :
  ∀ (hmn : n ≤ m),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)

Tactic:
obtain (hmn | hmn) : m ≤ n ∨ n ≤ m := le_total m n

Premises used: le_total
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : m ≤ n
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)

Tactic:
Module.End.pow_map_zero_of_le hmn hm

Premises used: Module.End.pow_map_zero_of_le
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : m ≤ n
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)

Tactic:
exact Module.End.pow_map_zero_of_le hmn hm

Premises used: Module.End.pow_map_zero_of_le
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : n ≤ m
⊢ ∀ (k : ℕ),
    Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
              (a : L) → L)
            (↑y : L) :
          L)
        (0 : L) ↔
      Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y

Tactic:
simp [K, Subtype.ext_iff, coe_ad_pow]

Premises used: LieSubalgebra.coe_ad_pow, Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : n ≤ m
⊢ ∀ (k : ℕ),
    Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
              (a : L) → L)
            (↑y : L) :
          L)
        (0 : L) ↔
      Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y

Tactic:
have : ∀ k : ℕ, ((ad R L) x ^ k) y = 0 ↔ y ∈ K k := by simp [K, Subtype.ext_iff, coe_ad_pow]
-- 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 N
inst_4 : LieAlgebra R N
inst_5 : LieRing M
inst_6 : LieAlgebra R M
i : N →ₗ⁅R⁆ L
p : L →ₗ⁅R⁆ M
h : i.range = LieIdeal.toLieSubalgebra R L p.ker
x : L
⊢ Eq.{u_4 + 1} (α := M) ((p : (a : L) → M) x : M) (0 : M) ↔
    Membership.mem (γ := Set L) (Set.range.{u_3, u_2 + 1} (ι := N) (⇑i : (a : N) → L)) x

Tactic:
simp [← LieHom.coe_range, h]

Premises used: LieHom.coe_range
-- 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 N
inst_4 : LieAlgebra R N
inst_5 : LieRing M
inst_6 : LieAlgebra R M
i : N →ₗ⁅R⁆ L
p : L →ₗ⁅R⁆ M
inst_7 : IsExtension i p
⊢ (LieIdeal.toLieSubalgebra R L p.ker).toSubmodule = i.range.toSubmodule

Tactic:
simp [exact (i := i) (p := p)]

Premises used: LieAlgebra.IsExtension.exact
-- 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
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : M
⊢ Membership.mem (α := E.L) E.proj.ker ((E.incl : (a : M) → E.L) x : E.L)

Tactic:
Exact.apply_apply_eq_zero ((E.incl.range_eq_ker_iff E.proj).mp E.IsExtension.exact) x

Premises used: Function.Exact.apply_apply_eq_zero, LieAlgebra.Extension.proj, Set.Mem, setOf, Set.preimage, Set.singleton, Iff.mp, LieAlgebra.IsExtension.exact, LieAlgebra.Extension.incl, LieHom.range_eq_ker_iff
-- 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
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : M
⊢ Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) ((E.incl : (a : M) → E.L) x : E.L) : L) (0 : L)

Tactic:
LieHom.mem_ker.mp (incl_apply_mem_ker E x)

Premises used: LieAlgebra.Extension.incl_apply_mem_ker, LieHom.mem_ker, Iff.mp
-- 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
E : Extension.{u_1, u_4, u_3, u_5} R M L
⊢ Injective.{u_4 + 1, u_5 + 1} (α := M) (β := E.L) (⇑E.incl : (a : M) → E.L)

Tactic:
(LieHom.ker_eq_bot E.incl).mp E.IsExtension.ker_eq_bot

Premises used: LieHom.ker_eq_bot, LieAlgebra.IsExtension.ker_eq_bot, Iff.mp, LieAlgebra.Extension.incl
-- 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
E : Extension.{u_1, u_4, u_3, u_5} R M L
⊢ Surjective.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L)

Tactic:
(LieHom.range_eq_top E.proj).mp E.IsExtension.range_eq_top

Premises used: LieAlgebra.Extension.proj, LieHom.range_eq_top, Iff.mp, LieAlgebra.IsExtension.range_eq_top
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
⊢ Eq (α := ofTwoCocycle c) ((ofProd c : (a : L × M) → ofTwoCocycle c) 0) 0

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y : L × M
⊢ (ofProd c : (a : L × M) → ofTwoCocycle c) (x + y) =
    HAdd.hAdd (α := ofTwoCocycle c) (β := ofTwoCocycle c) ((ofProd c : (a : L × M) → ofTwoCocycle c) x : ofTwoCocycle c)
      ((ofProd c : (a : L × M) → ofTwoCocycle c) y : ofTwoCocycle c)

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
r : R
x : L × M
⊢ (ofProd c : (a : L × M) → ofTwoCocycle c) (r • x) =
    HSMul.hSMul (β := ofTwoCocycle c) r ((ofProd c : (a : L × M) → ofTwoCocycle c) x : ofTwoCocycle c)

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
⊢ Eq (α := L × M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) 0) 0

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y : ofTwoCocycle c
⊢ ((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x + y) =
    HAdd.hAdd (α := L × M) (β := L × M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x : L × M)
      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y : L × M)

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
r : R
x : ofTwoCocycle c
⊢ ((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • x) =
    HSMul.hSMul (β := L × M) r (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x : L × M)

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
n : ℕ
x : L × M
⊢ (ofProd c : (a : L × M) → ofTwoCocycle c) (n • x) =
    HSMul.hSMul (β := ofTwoCocycle c) n ((ofProd c : (a : L × M) → ofTwoCocycle c) x : ofTwoCocycle c)

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
n : ℕ
x : ofTwoCocycle c
⊢ ((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (n • x) =
    HSMul.hSMul (β := L × M) n (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x : L × M)

Tactic:
rfl

Premises used: rfl
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M) +
        HAdd.hAdd (α := M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2) -
      HAdd.hAdd (α := M)
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2) =
    HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2 :
            M) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2 +
      (HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2 :
            M) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2)

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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
            M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M) +
        HAdd.hAdd (α := M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2) -
      HAdd.hAdd (α := M)
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) =
    HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
            M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2 :
            M) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2 +
      (HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2 :
            M) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)

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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x : ofTwoCocycle c
rw :
  Eq (α := ofTwoCocycle c)
    ((ofProd c : (a : L × M) → ofTwoCocycle c)
        (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1,
          HAdd.hAdd (α := M) 0
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) -
            Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) :
      ofTwoCocycle c)
    ((ofProd c : (a : L × M) → ofTwoCocycle c) 0 : ofTwoCocycle c)
⊢ Eq (α := ofTwoCocycle c)
    ((ofProd c : (a : L × M) → ofTwoCocycle c)
        (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1,
          HAdd.hAdd (α := M) (β := M)
              ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2 :
                M) -
            Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) :
      ofTwoCocycle c)
    (0 : ofTwoCocycle c)

Tactic:
rw [← of_zero, c.1.2]

Premises used: LieAlgebra.of_zero, Subtype.val, Subtype.property
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x : ofTwoCocycle c
⊢ Eq (α := L × M)
    (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1,
      HAdd.hAdd (α := M) 0
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)
    0

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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x : ofTwoCocycle c
⊢ Eq (α := ofTwoCocycle c)
    ((ofProd c : (a : L × M) → ofTwoCocycle c)
        (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1,
          HAdd.hAdd (α := M) 0
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) -
            Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) :
      ofTwoCocycle c)
    ((ofProd c : (a : L × M) → ofTwoCocycle c) 0 : ofTwoCocycle c)

Tactic:
exact Equiv.congr_arg (by simp)

Premises used: Equiv.congr_arg
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← of_add]

Premises used: LieAlgebra.of_add
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Equiv.congr_arg ?_

Premises used: Equiv.congr_arg
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Equiv.congr_arg ?_

Premises used: Equiv.congr_arg