awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x : L
h :
  ({ 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)
      ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (x, 0) : LieAlgebra.ofTwoCocycle c) =
    x
⊢ ∃ (a : 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' := ⋯ } :
          (a : LieAlgebra.ofTwoCocycle c) → L)
        a =
      x

Tactic:
use (ofProd c (x, 0))

Premises used: Prod.mk, LieAlgebra.ofProd, OfNat.ofNat, DFunLike.coe
-- 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 : 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)
      ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (x, 0) : LieAlgebra.ofTwoCocycle c) =
    x

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)
h :
  ∀ (x : LieAlgebra.ofTwoCocycle c),
    Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
        (LieHom.range (L := M)
          { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
            map_smul' := ⋯, map_lie' := ⋯ })
        x ↔
      Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
        (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
          (LieHom.ker (L' := L)
            {
              toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
                (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
              map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
        x
⊢ Eq (α := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieHom.range (L := M)
      { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
        map_smul' := ⋯, map_lie' := ⋯ })
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))

Tactic:
ext x
-- 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 : LieAlgebra.ofTwoCocycle c
h :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieHom.range (L := M)
        { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
          map_smul' := ⋯, map_lie' := ⋯ })
      x →
    Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
        (LieHom.ker (L' := L)
          {
            toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
              (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
            map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
      x
h₁ :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
        (LieHom.ker (L' := L)
          {
            toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
              (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
            map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
      x →
    Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieHom.range (L := M)
        { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
          map_smul' := ⋯, map_lie' := ⋯ })
      x
⊢ Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieHom.range (L := M)
        { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
          map_smul' := ⋯, map_lie' := ⋯ })
      x ↔
    Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
        (LieHom.ker (L' := L)
          {
            toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
              (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
            map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
      x

Tactic:
constructor
-- 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 : LieAlgebra.ofTwoCocycle c
hx :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieHom.range (L := M)
      { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
        map_smul' := ⋯, map_lie' := ⋯ })
    x
h :
  ∀ (n : M)
    (h :
      ((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
                  map_smul' := ⋯, map_lie' := ⋯ } :
              M →ₗ[R] LieAlgebra.ofTwoCocycle c) :
            (a : M) → LieAlgebra.ofTwoCocycle c)
          n =
        x),
    Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
      (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
        (LieHom.ker (L' := L)
          {
            toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
              (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
            map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
      x
⊢ Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    x

Tactic:
obtain ⟨n, h⟩ := hx
-- 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 : LieAlgebra.ofTwoCocycle c
n : M
h :
  ((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
              map_smul' := ⋯, map_lie' := ⋯ } :
          M →ₗ[R] LieAlgebra.ofTwoCocycle c) :
        (a : M) → LieAlgebra.ofTwoCocycle c)
      n =
    x
h₁ :
  Membership.mem (α := LieAlgebra.ofTwoCocycle c) (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    (((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
                map_smul' := ⋯, map_lie' := ⋯ } :
            M →ₗ[R] LieAlgebra.ofTwoCocycle c) :
          (a : M) → LieAlgebra.ofTwoCocycle c)
        n :
      LieAlgebra.ofTwoCocycle c)
⊢ Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    x

Tactic:
rw [← h]
-- 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 : LieAlgebra.ofTwoCocycle c
n : M
h :
  ((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
              map_smul' := ⋯, map_lie' := ⋯ } :
          M →ₗ[R] LieAlgebra.ofTwoCocycle c) :
        (a : M) → LieAlgebra.ofTwoCocycle c)
      n =
    x
⊢ Membership.mem (α := LieAlgebra.ofTwoCocycle c) (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    (((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
                map_smul' := ⋯, map_lie' := ⋯ } :
            M →ₗ[R] LieAlgebra.ofTwoCocycle c) :
          (a : M) → LieAlgebra.ofTwoCocycle c)
        n :
      LieAlgebra.ofTwoCocycle c)

Tactic:
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 : 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 : LieAlgebra.ofTwoCocycle c
hx :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    x
⊢ Eq.{u_3 + 1} (α := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1 0

Tactic:
have : ((ofProd c).symm x).1 = 0 := hx
-- 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 : LieAlgebra.ofTwoCocycle c
hx :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    x
this : Eq.{u_3 + 1} (α := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1 0
h :
  (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
      (0, (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) =
    x
⊢ ∃ (y : M), (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, y) = x

Tactic:
use ((ofProd c).symm x).2

Premises used: LieAlgebra.ofProd, Equiv.symm, Prod.snd, DFunLike.coe
-- 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 : LieAlgebra.ofTwoCocycle c
hx :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    x
this : Eq.{u_3 + 1} (α := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1 0
h :
  Eq (α := LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
        (0, (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) :
      LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
        (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x) :
      LieAlgebra.ofTwoCocycle c)
⊢ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
      (0, (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) =
    x

Tactic:
nth_rw 2 [← Equiv.apply_symm_apply (ofProd c) x]

Premises used: Equiv.apply_symm_apply, LieAlgebra.ofProd
-- 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 : LieAlgebra.ofTwoCocycle c
hx :
  Membership.mem (γ := LieSubalgebra R (LieAlgebra.ofTwoCocycle c))
    (LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      (LieHom.ker (L' := L)
        {
          toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
            (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }))
    x
this : Eq.{u_3 + 1} (α := L) (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1 0
h h₁ :
  Eq (α := LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
        ((((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
          (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) :
      LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
        (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x) :
      LieAlgebra.ofTwoCocycle c)
⊢ Eq (α := LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
        (0, (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) :
      LieAlgebra.ofTwoCocycle c)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
        (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x) :
      LieAlgebra.ofTwoCocycle c)

Tactic:
rw [← this]
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
c : ↥(twoCocycle R L M)
x y : (ofTwoCocycle c).L
⊢ ⁅x, y⁆ =
    (ofAlg c : (a : LieAlgebra.ofTwoCocycle c) → (ofTwoCocycle c).L)
      (Bracket.bracket (L := LieAlgebra.ofTwoCocycle c)
        ((LieEquiv.symm (ofAlg c) : (a : (ofTwoCocycle c).L) → LieAlgebra.ofTwoCocycle c) x : LieAlgebra.ofTwoCocycle c)
        ((LieEquiv.symm (ofAlg c) : (a : (ofTwoCocycle c).L) → LieAlgebra.ofTwoCocycle c) y))

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 : 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 : M
⊢ Eq (α := (ofTwoCocycle c).L) (((ofTwoCocycle c).incl : (a : M) → (ofTwoCocycle c).L) x : (ofTwoCocycle c).L)
    ({ carrier := (0, x) } : LieAlgebra.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 : 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 : (ofTwoCocycle c).L
⊢ ((ofTwoCocycle c).proj : (a : (ofTwoCocycle c).L) → L) x = x.carrier.1

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 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : E.L
y : M
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (⁅x, (E.incl : (a : M) → E.L) y⁆ : E.L) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L)
    (Bracket.bracket (L := L) ((E.proj : (a : E.L) → L) x : L)
        ((E.proj : (a : E.L) → L) ((E.incl : (a : M) → E.L) y : E.L)) :
      L)
    (0 : L)
rw₂ : Eq.{u_3 + 1} (α := L) (Bracket.bracket (L := L) ((E.proj : (a : E.L) → L) x : L) 0) 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := L) 0 0
⊢ Membership.mem (α := E.L) E.proj.ker (⁅x, (E.incl : (a : M) → E.L) y⁆ : E.L)

Tactic:
rw [LieHom.mem_ker, LieHom.map_lie, proj_incl, lie_zero]

Premises used: LieHom.map_lie, LieAlgebra.Extension.proj_incl, LieHom.mem_ker, 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
E : Extension.{u_1, u_4, u_3, u_5} R M L
x x_1 : M
⊢ Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) (x + x_1)) ⋯ =
    HAdd.hAdd (α := ↥E.proj.ker) (β := ↥E.proj.ker)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x) ⋯ : ↥E.proj.ker)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x_1) ⋯ : ↥E.proj.ker)

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
x : R
x_1 : M
⊢ Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) (x • x_1)) ⋯ =
    HSMul.hSMul (α := R) (β := ↥E.proj.ker) ((RingHom.id R : (a : R) → R) x : R)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x_1) ⋯ : ↥E.proj.ker)

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
x y : M
a :
  Eq.{u_5 + 1} (α := E.L)
    ((↑(Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) ⁅x, y⁆) ⋯) : E.L) : E.L)
    ((↑(Bracket.bracket (L := ↥E.proj.ker)
            (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x) ⋯ : ↥E.proj.ker)
            (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) y) ⋯)) :
        E.L) :
      E.L)
⊢ Eq.{u_5 + 1} (α := ↥E.proj.ker)
    (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) ⁅x, y⁆) ⋯ : ↥E.proj.ker)
    (Bracket.bracket (L := ↥E.proj.ker)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x) ⋯ : ↥E.proj.ker)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) y) ⋯) :
      ↥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
x y : M
⊢ Eq.{u_5 + 1} (α := E.L)
    ((↑(Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) ⁅x, y⁆) ⋯) : E.L) : E.L)
    ((↑(Bracket.bracket (L := ↥E.proj.ker)
            (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x) ⋯ : ↥E.proj.ker)
            (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) y) ⋯)) :
        E.L) :
      E.L)

Tactic:
simp [← LieHom.map_lie]

Premises used: LieHom.map_lie
-- 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
x : M
simp :
  Eq (α := (↑(Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) : Type u_5))
    ((LinearEquiv.ofEq (↑E.proj : E.L →ₗ[R] L).ker (↑E.incl : M →ₗ[R] E.L).range ⋯ : (a : ↥E.proj.ker) → ↥E.incl.range)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x) ⋯) :
      ↥E.incl.range)
    (Subtype.mk (p := fun (x : E.L) ↦
        Membership.mem (γ := Set E.L) (Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) x)
        ((E.incl : (a : M) → E.L) x) ⋯ :
      { x : E.L // Membership.mem (γ := Set E.L) (Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) x })
⊢ comp (α := ↥E.proj.ker) (β := (↑(Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) : Type u_5))
      (⇑(Equiv.ofInjective (⇑E.incl : (a : M) → E.L) ⋯).symm :
        (a : (↑(Set.range (⇑E.incl : (a : M) → E.L)) : Type u_5)) → M)
      (⇑(IsExtension.kerEquivRange E.incl E.proj) : (a : ↥E.proj.ker) → ↥E.incl.range)
      ((fun (m : M) ↦ (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) m) ⋯ : ↥E.proj.ker))
        x) =
    x

Tactic:
simp [IsExtension.kerEquivRange, Equiv.symm_apply_eq]

Premises used: LieAlgebra.IsExtension.kerEquivRange, Equiv.symm_apply_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
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : M
⊢ Eq (α := (↑(Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) : Type u_5))
    ((LinearEquiv.ofEq (↑E.proj : E.L →ₗ[R] L).ker (↑E.incl : M →ₗ[R] E.L).range ⋯ : (a : ↥E.proj.ker) → ↥E.incl.range)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) x) ⋯) :
      ↥E.incl.range)
    (Subtype.mk (p := fun (x : E.L) ↦
        Membership.mem (γ := Set E.L) (Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) x)
        ((E.incl : (a : M) → E.L) x) ⋯ :
      { x : E.L // Membership.mem (γ := Set E.L) (Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) x })

Tactic:
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 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : ↥E.proj.ker
⊢ (fun (m : M) ↦ (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) m) ⋯ : ↥E.proj.ker))
      (comp (β := (↑(Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) : Type u_5))
        (⇑(Equiv.ofInjective (⇑E.incl : (a : M) → E.L) ⋯).symm :
          (a : (↑(Set.range (⇑E.incl : (a : M) → E.L)) : Type u_5)) → M)
        (⇑(IsExtension.kerEquivRange E.incl E.proj) : (a : ↥E.proj.ker) → ↥E.incl.range) x) =
    x

Tactic:
simpa [Subtype.ext_iff] using Equiv.apply_ofInjective_symm E.incl_injective _

Premises used: LieAlgebra.Extension.incl_injective, Subtype.ext_iff, Equiv.apply_ofInjective_symm
-- 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
y : E.L
⊢ Eq (α := E.L) (⁅y, (↑((E.toKer : (a : M) → ↥E.proj.ker) x) : E.L)⁆ : E.L) (⁅y, (E.incl : (a : M) → E.L) x⁆ : E.L)

Tactic:
rfl