awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ 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)
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 : L
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x + x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x + x_1) : E.L))
          ⋯) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) ⋯ +
          Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
      M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x + x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x + x_1) : E.L))
          ⋯) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L) +
            HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L))
          ⋯) :
      M)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x + x_1) : E.L) ((s₂ : (a : L) → E.L) (x + x_1) : E.L))
        ⋯) =
    HAdd.hAdd (α := M) (β := M)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) ⋯) :
        M)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw₂ : Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
    (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x + x_1) : E.L) ((s₂ : (a : L) → E.L) (x + x_1) : E.L)) sorry =
  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
    (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L) +
      HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L))
    sorry
Tactic: rw [← map_add, AddMemClass.mk_add_mk, EquivLike.apply_eq_iff_eq, Subtype.mk_eq_mk, map_add,
      map_add, add_sub_add_comm]
-- 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₁ 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)
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
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw : (E.toKer.symm : (a : ↥E.proj.ker) → M)
    (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
      sorry) =
  HSMul.hSMul (β := M) x
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) sorry) :
      M)
Tactic: rw [RingHom.id_apply, ← map_smul, EquivLike.apply_eq_iff_eq, SetLike.mk_smul_of_tower_mk,
      Subtype.mk_eq_mk, LinearMap.map_smul_of_tower, smul_sub, LinearMap.map_smul_of_tower]
-- 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₁ 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)
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
rw :
  (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (β := M) x
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw₁ : Eq.{u_4 + 1} (α := M)
  ((E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        sorry) :
    M)
  ((E.toKer.symm : (a : ↥E.proj.ker) → M)
      (x •
        Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) sorry) :
    M)
Tactic: rw [RingHom.id_apply, ← map_smul, EquivLike.apply_eq_iff_eq, SetLike.mk_smul_of_tower_mk,
      Subtype.mk_eq_mk, LinearMap.map_smul_of_tower, smul_sub, LinearMap.map_smul_of_tower]
-- 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₁ 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)
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
rw :
  (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (β := M) x
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
          ⋯) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (x •
          Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
      M)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw₂ : Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
    (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L)) sorry =
  x •
    Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) sorry
Tactic: rw [RingHom.id_apply, ← map_smul, EquivLike.apply_eq_iff_eq, SetLike.mk_smul_of_tower_mk,
      Subtype.mk_eq_mk, LinearMap.map_smul_of_tower, smul_sub, LinearMap.map_smul_of_tower]
-- 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₁ 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)
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
rw :
  (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (β := M) x
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
          ⋯) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (x •
          Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
      M)
rw₂ :
  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
      ⋯ =
    x •
      Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw₃ : Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
    (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L)) sorry =
  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
    (x • HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) sorry
Tactic: rw [RingHom.id_apply, ← map_smul, EquivLike.apply_eq_iff_eq, SetLike.mk_smul_of_tower_mk,
      Subtype.mk_eq_mk, LinearMap.map_smul_of_tower, smul_sub, LinearMap.map_smul_of_tower]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
⊢ (d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂) =
    (↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))
have a : ∀ (x y : L),
  Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
Tactic: ext x y
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
⊢ Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
have a : ∀ (s : (b : L) → E.L) (hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b),
  Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
Tactic: choose s hs using E.proj_surjective
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
⊢ s x - s' x ∈ E.proj.ker
have rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x - s' x) : L) (0 : L)
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x - s' x) : L) (0 : L)
⊢ s x - s' x ∈ E.proj.ker
have rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L) = 0
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x - s' x) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L) = 0
⊢ s x - s' x ∈ E.proj.ker
have rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L)
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x - s' x) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L) = 0
rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L)
⊢ s x - s' x ∈ E.proj.ker
have rw₃ : (E.proj : (a : E.L) → L) (s x) = x
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x - s' x) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L) = 0
rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s x) : L) ((E.proj : (a : E.L) → L) (s' x) : L)
rw₃ : (E.proj : (a : E.L) → L) (s x) = x
⊢ s x - s' x ∈ E.proj.ker
have rw₄ : x = x
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
⊢ s' y - s y ∈ E.proj.ker
have rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y - s y) : L) (0 : L)
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y - s y) : L) (0 : L)
⊢ s' y - s y ∈ E.proj.ker
have rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L) = 0
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]
-- 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₁ 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)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj : (a : E.L) → L) s'
rw : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y - s y) : L) (0 : L)
rw₁ : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L) = 0
⊢ s' y - s y ∈ E.proj.ker
have rw₂ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) (s' y) : L) ((E.proj : (a : E.L) → L) (s y) : L)
Tactic: rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]