awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
x : M
hx :
  ((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x =
    Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z),
            (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
          ↥E.proj.ker) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) : M)
rw₁ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
⊢ Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) z : L) y =
    (E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
have rw₂ : HSub.hSub (α := ↥E.proj.ker) (β := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) =
  0
Tactic: rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
x : M
hx :
  ((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x =
    Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z),
            (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
          ↥E.proj.ker) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) : M)
rw₁ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
rw₂ :
  HSub.hSub (α := ↥E.proj.ker) (β := ↥E.proj.ker)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z),
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
        ↥E.proj.ker)
      (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) =
    0
⊢ Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) z : L) y =
    (E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
have rw₃ : Eq (α := ↥E.proj.ker)
  (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry
          ((E.proj : (a : E.L) → L) z) -
        z,
      (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
    ↥E.proj.ker)
  (0 : ↥E.proj.ker)
Tactic: rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
x : M
hx :
  ((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x =
    Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z),
            (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
          ↥E.proj.ker) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) : M)
rw₁ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
rw₂ :
  HSub.hSub (α := ↥E.proj.ker) (β := ↥E.proj.ker)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z),
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
        ↥E.proj.ker)
      (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) =
    0
rw₃ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (0 : ↥E.proj.ker)
⊢ Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) z : L) y =
    (E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
have rw₄ : Eq.{u_5 + 1} (α := E.L)
  (↑⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
    E.L)
  (↑0 : E.L)
Tactic: rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
x : M
hx :
  ((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x =
    Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z),
            (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
          ↥E.proj.ker) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) : M)
rw₁ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
rw₂ :
  HSub.hSub (α := ↥E.proj.ker) (β := ↥E.proj.ker)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z),
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
        ↥E.proj.ker)
      (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) =
    0
rw₃ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (0 : ↥E.proj.ker)
rw₄ :
  Eq.{u_5 + 1} (α := E.L)
    (↑⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z) -
            z,
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      E.L)
    (↑0 : E.L)
⊢ Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) z : L) y =
    (E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
have rw₅ : Eq (α := E.L)
  ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry
        ((E.proj : (a : E.L) → L) z) -
      z,
    (↑((E.toKer : (a : M) → ↥E.proj.ker) y) : E.L)⁆
  (↑0 : E.L)
Tactic: rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
x : M
hx :
  ((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x =
    Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z),
            (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
          ↥E.proj.ker) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) : M)
rw₁ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
rw₂ :
  HSub.hSub (α := ↥E.proj.ker) (β := ↥E.proj.ker)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z),
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
        ↥E.proj.ker)
      (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) =
    0
rw₃ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (0 : ↥E.proj.ker)
rw₄ :
  Eq.{u_5 + 1} (α := E.L)
    (↑⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z) -
            z,
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      E.L)
    (↑0 : E.L)
rw₅ :
  Eq (α := E.L)
    ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z) -
        z,
      (↑((E.toKer : (a : M) → ↥E.proj.ker) y) : E.L)⁆
    (↑0 : E.L)
⊢ Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) z : L) y =
    (E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
have rw₆ : Eq (α := E.L)
  (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry
          ((E.proj : (a : E.L) → L) z) -
        z,
      (E.incl : (a : M) → E.L) y⁆ :
    E.L)
  ((↑0 : E.L) : E.L)
Tactic: rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
this : LieRingModule L M := E.ringModuleOf
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
r : R
x : L
m : M
⊢ ⁅r • x, m⁆ = r • ⁅x, m⁆
have rw : Eq (α := ↥E.proj.ker)
  (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry (r • x) -
        r • Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) sorry x,
      (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
    ↥E.proj.ker)
  (0 : ↥E.proj.ker)
Tactic: rw [ringModuleOf_bracket, ringModuleOf_bracket, ← map_smul, ← smul_lie,
          EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
s : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s : (a : L) → E.L)
x : E.L
y : ↥E.proj.ker
⊢ Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ((E.proj : (a : E.L) → L) x) : E.L) y = ⁅x, y⁆
have rw : ⁅HSub.hSub (α := E.L) ((s : (a : L) → E.L) ((E.proj : (a : E.L) → L) x) : E.L) x, y⁆ = 0
Tactic: rw [← sub_eq_zero, ← sub_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s : (a : L) → E.L)
x x_1 x_2 : L
⊢ Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) (x_1 + x_2)) : E.L)
        ((s : (a : L) → E.L) ⁅x, x_1 + x_2⁆ : E.L))
      ⋯ =
    Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
          ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L))
        ⋯ +
      Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_2) : E.L)
          ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L))
        ⋯
have simp : HAdd.hAdd (α := E.L) (β := E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_2) : E.L) -
    HAdd.hAdd (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L) =
  HSub.hSub (α := E.L) (β := E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
      ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) +
    HSub.hSub (α := E.L) (β := E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_2) : E.L)
      ((s : (a : L) → E.L) ⁅x, x_2⁆ : E.L)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s : (a : L) → E.L)
x y x_1 : L
⊢ Eq.{u_5 + 1} (α := E.L)
    (↑(({
              toFun := fun (y_1 : L) ↦
                Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                  (HSub.hSub (α := E.L) (β := E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) (x + y) : E.L) ((s : (a : L) → E.L) y_1) : E.L)
                    ((s : (a : L) → E.L) ⁅x + y, y_1⁆ : E.L))
                  ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : L) → ↥E.proj.ker)
          x_1) :
      E.L)
    (↑((HAdd.hAdd (α := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
              {
                toFun := fun (y : L) ↦
                  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                    (HSub.hSub (α := E.L) (β := E.L)
                      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y) : E.L)
                      ((s : (a : L) → E.L) ⁅x, y⁆ : E.L))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }
              {
                toFun := fun (y_1 : L) ↦
                  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                    (HSub.hSub (α := E.L) (β := E.L)
                      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) y_1) : E.L)
                      ((s : (a : L) → E.L) ⁅y, y_1⁆ : E.L))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker } :
            (a : L) → ↥E.proj.ker)
          x_1) :
      E.L)
have h : HAdd.hAdd (α := E.L) (β := E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) x_1) : E.L) -
    HAdd.hAdd (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) ((s : (a : L) → E.L) ⁅y, x_1⁆ : E.L) =
  HSub.hSub (α := E.L) (β := E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) x_1) : E.L)
      ((s : (a : L) → E.L) ⁅x, x_1⁆ : E.L) +
    HSub.hSub (α := E.L) (β := E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) x_1) : E.L)
      ((s : (a : L) → E.L) ⁅y, x_1⁆ : E.L)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s : (a : L) → E.L)
x : R
x_1 : L
⊢ {
      toFun := fun (y : L) ↦
        Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) (x • x_1) : E.L) ((s : (a : L) → E.L) y) : E.L)
            ((s : (a : L) → E.L) ⁅x • x_1, y⁆ : E.L))
          ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
      ((RingHom.id R : (a : R) → R) x : R)
      {
        toFun := fun (y : L) ↦
          Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x_1 : E.L) ((s : (a : L) → E.L) y) : E.L)
              ((s : (a : L) → E.L) ⁅x_1, y⁆ : E.L))
            ⋯,
        map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }
have h : ∀ (x_2 : L),
  Eq.{u_5 + 1} (α := E.L)
    (↑(({
              toFun := fun (y : L) ↦
                Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                  (HSub.hSub (α := E.L) (β := E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) (x • x_1) : E.L) ((s : (a : L) → E.L) y) : E.L)
                    ((s : (a : L) → E.L) ⁅x • x_1, y⁆ : E.L))
                  sorry,
              map_add' := sorry, map_smul' := sorry } :
            (a : L) → ↥E.proj.ker)
          x_2) :
      E.L)
    (↑((HSMul.hSMul (α := R) (β := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
              ((RingHom.id R : (a : R) → R) x : R)
              {
                toFun := fun (y : L) ↦
                  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                    (HSub.hSub (α := E.L) (β := E.L)
                      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x_1 : E.L) ((s : (a : L) → E.L) y) : E.L)
                      ((s : (a : L) → E.L) ⁅x_1, y⁆ : E.L))
                    sorry,
                map_add' := sorry, map_smul' := sorry : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker } :
            (a : L) → ↥E.proj.ker)
          x_2) :
      E.L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s : (a : L) → E.L)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M)
    (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
      Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
      ((E.twoCocycleAux hs).compr₂ (↑E.toKer.symm.toLinearEquiv : ↥E.proj.ker →ₗ[R] M)) ⋯)
have h : ∀ (x y z : L),
  Eq.{u_4 + 1} (α := M)
    ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
                          (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
                            Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
                            ((E.twoCocycleAux hs).compr₂ (↑E.toKer.symm.toLinearEquiv : ↥E.proj.ker →ₗ[R] M)) sorry) :
                        L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)
    ((((((0 : (a : L) → L →ₗ[R] L →ₗ[R] M) x : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M)
        z :
      M)
Tactic: ext x y z