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 : 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
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) (↑c : ↥(twoCochain R L M))

Tactic:
have hc := c.2
-- 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
hc : Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) (↑c : ↥(twoCochain R L M))
⊢ Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) (↑c : ↥(twoCochain R L M)) :
      L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)

Tactic:
rw [mem_twoCocycle_iff] at hc

Premises used: LieModule.Cohomology.mem_twoCocycle_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 : 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
⊢ ⁅x, y⁆ =
    (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) y).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) 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)

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)
r : R
x y : ofTwoCocycle c
simp :
  (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) (r • y)).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) (r • 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) (r • y)).2 :
              M) -
          Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) =
    HSMul.hSMul (β := ofTwoCocycle c) r
      ((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) y).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) 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) :
        ofTwoCocycle c)
⊢ ⁅x, r • y⁆ = r • ⁅x, y⁆

Tactic:
simp only [bracket_ofTwoCocycle]

Premises used: LieAlgebra.bracket_ofTwoCocycle
-- 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)
r : R
x y : ofTwoCocycle c
⊢ (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).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) (r • 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) (r • y)).2 :
            M) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) =
    HSMul.hSMul (β := L × M) r
      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M)
          ((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) y).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) 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)) :
        L × M)

Tactic:
simp [← smul_add, smul_sub]

Premises used: smul_sub, smul_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)
r : R
x y : 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) (r • y)).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) (r • 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) (r • y)).2 :
              M) -
          Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) =
    HSMul.hSMul (β := ofTwoCocycle c) r
      ((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) y).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) 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) :
        ofTwoCocycle c)

Tactic:
exact Equiv.congr_arg (by simp [← smul_add, smul_sub])

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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
x_1 x_2 : ofTwoCocycle c
simp :
  HAdd.hAdd (α := M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 -
      HAdd.hAdd (α := M) (β := M) ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M) =
    HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M) +
      HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M)
⊢ (ofProd c' : (a : L × M) → ofTwoCocycle c')
      ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x_1 + x_2)).1,
        HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x_1 + x_2)).2 : M)
          ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x_1 + x_2)).1 : M)) =
    HAdd.hAdd (α := ofTwoCocycle c') (β := ofTwoCocycle c')
      ((ofProd c' : (a : L × M) → ofTwoCocycle c')
          ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1,
            HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
              ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)) :
        ofTwoCocycle c')
      ((ofProd c' : (a : L × M) → ofTwoCocycle c')
          ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1,
            HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 : M)
              ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M)) :
        ofTwoCocycle c')

Tactic:
simp [← 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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
x_1 x_2 : ofTwoCocycle c
⊢ HAdd.hAdd (α := M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 -
      HAdd.hAdd (α := M) (β := M) ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M) =
    HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M) +
      HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M)

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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
⊢ ∀ (m : R) (x_1 : ofTwoCocycle c),
    (ofProd c' : (a : L × M) → ofTwoCocycle c')
        ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (m • x_1)).1,
          HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (m • x_1)).2 : M)
            ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (m • x_1)).1 : M)) =
      HSMul.hSMul (α := R) (β := ofTwoCocycle c') ((RingHom.id R : (a : R) → R) m : R)
        ((ofProd c' : (a : L × M) → ofTwoCocycle c')
            ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1,
              HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
                ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)) :
          ofTwoCocycle c')

Tactic:
simp [← of_smul, smul_sub]

Premises used: LieAlgebra.of_smul, 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
y : ofTwoCocycle c
⊢ (fun (z : ofTwoCocycle c') ↦
        ((ofProd c : (a : L × M) → ofTwoCocycle c)
            ((((ofProd c').symm : (a : ofTwoCocycle c') → L × M) z).1,
              HAdd.hAdd (α := M) (β := M) ((((ofProd c').symm : (a : ofTwoCocycle c') → L × M) z).2 : M)
                ((x : (a : L) → M) (((ofProd c').symm : (a : ofTwoCocycle c') → L × M) z).1 : M)) :
          ofTwoCocycle c))
      ((fun (y : ofTwoCocycle c) ↦
          ((ofProd c' : (a : L × M) → ofTwoCocycle c')
              ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1,
                HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2 : M)
                  ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 : M)) :
            ofTwoCocycle c'))
        y) =
    y

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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
z : ofTwoCocycle c'
⊢ (fun (y : ofTwoCocycle c) ↦
        ((ofProd c' : (a : L × M) → ofTwoCocycle c')
            ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1,
              HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2 : M)
                ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 : M)) :
          ofTwoCocycle c'))
      ((fun (z : ofTwoCocycle c') ↦
          ((ofProd c : (a : L × M) → ofTwoCocycle c)
              ((((ofProd c').symm : (a : ofTwoCocycle c') → L × M) z).1,
                HAdd.hAdd (α := M) (β := M) ((((ofProd c').symm : (a : ofTwoCocycle c') → L × M) z).2 : M)
                  ((x : (a : L) → M) (((ofProd c').symm : (a : ofTwoCocycle c') → L × M) z).1 : M)) :
            ofTwoCocycle c))
        z) =
    z

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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x x_1 : M
⊢ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x + x_1) =
    HAdd.hAdd (α := LieAlgebra.ofTwoCocycle c) (β := LieAlgebra.ofTwoCocycle c)
      ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x) : LieAlgebra.ofTwoCocycle c)
      ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x_1) : LieAlgebra.ofTwoCocycle c)

Tactic:
simp [← 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 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x : R
x_1 : M
⊢ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x • x_1) =
    HSMul.hSMul (α := R) (β := LieAlgebra.ofTwoCocycle c) ((RingHom.id R : (a : R) → R) x : R)
      ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x_1) : LieAlgebra.ofTwoCocycle c)

Tactic:
simp [← of_smul]

Premises used: LieAlgebra.of_smul
-- 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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x x_1 : M
⊢ Eq (α := LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, ⁅x, x_1⁆) : LieAlgebra.ofTwoCocycle c)
    (Bracket.bracket (L := LieAlgebra.ofTwoCocycle c)
        ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x) : LieAlgebra.ofTwoCocycle c)
        ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x_1)) :
      LieAlgebra.ofTwoCocycle c)

Tactic:
simp [trivial_lie_zero, bracket_ofTwoCocycle]

Premises used: LieAlgebra.bracket_ofTwoCocycle, trivial_lie_zero
-- 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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x x_1 : LieAlgebra.ofTwoCocycle c
⊢ (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) (x + x_1)).1 =
    HAdd.hAdd (α := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1
      (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x_1).1

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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x : R
x_1 : LieAlgebra.ofTwoCocycle c
⊢ (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) (x • x_1)).1 =
    HSMul.hSMul (α := R) (β := L) ((RingHom.id R : (a : R) → R) x : R)
      (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x_1).1

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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x x_1 : LieAlgebra.ofTwoCocycle c
⊢ Eq.{u_3 + 1} (α := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) ⁅x, x_1⁆).1
    (Bracket.bracket (L := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1
      (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x_1).1)

Tactic:
simp [bracket_ofTwoCocycle]

Premises used: LieAlgebra.bracket_ofTwoCocycle
-- 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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
rw :
  Injective (α := M) (β := LieAlgebra.ofTwoCocycle c)
    (⇑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
          map_smul' := ⋯, map_lie' := ⋯ } :
      (a : M) → LieAlgebra.ofTwoCocycle c)
⊢ Eq.{u_4 + 1} (α := LieIdeal R M)
    (LieHom.ker (L' := LieAlgebra.ofTwoCocycle c)
      { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
        map_smul' := ⋯, map_lie' := ⋯ })
    ⊥

Tactic:
rw [LieHom.ker_eq_bot]

Premises used: LieHom.ker_eq_bot
-- 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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x y : M
⊢ Eq (α := LieAlgebra.ofTwoCocycle c)
      (({ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
              map_smul' := ⋯, map_lie' := ⋯ } :
            (a : M) → LieAlgebra.ofTwoCocycle c)
          x :
        LieAlgebra.ofTwoCocycle c)
      (({ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
              map_smul' := ⋯, map_lie' := ⋯ } :
            (a : M) → LieAlgebra.ofTwoCocycle c)
          y :
        LieAlgebra.ofTwoCocycle c) →
    x = y

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
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
rw :
  Surjective (α := LieAlgebra.ofTwoCocycle c) (β := L)
    (⇑{
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
      (a : LieAlgebra.ofTwoCocycle c) → L)
⊢ Eq.{u_3 + 1} (α := LieSubalgebra R L)
    (LieHom.range (L := LieAlgebra.ofTwoCocycle c)
      {
        toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
          (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
        map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ })
    ⊤

Tactic:
rw [LieHom.range_eq_top]

Premises used: LieHom.range_eq_top