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
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 y z : L
this :
  HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
u : L
v : ↥E.proj.ker
⊢ ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u, v⁆ =
    Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
have rw : Bracket.bracket (L := E.L)
    ((s : (a : L) → E.L)
        ((E.proj : (a : E.L) → L)
          (Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u)) :
      E.L)
    v =
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
Tactic: rw [← E.lie_apply_proj_of_leftInverse_eq hs, h.choose_spec _]
-- 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)
x y z : L
this :
  HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
u : L
v : ↥E.proj.ker
rw :
  Bracket.bracket (L := E.L)
      ((s : (a : L) → E.L)
          ((E.proj : (a : E.L) → L)
            (Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u)) :
        E.L)
      v =
    Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
⊢ ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h u, v⁆ =
    Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
have rw₁ : Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v = Bracket.bracket (L := E.L) ((s : (a : L) → E.L) u : E.L) v
Tactic: rw [← E.lie_apply_proj_of_leftInverse_eq hs, h.choose_spec _]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
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)
x y z : L
⊢ HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
have hjac : Bracket.bracket (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) z) =
  HSub.hSub (α := E.L) (β := E.L)
    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
      E.L)
    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
      E.L)
Tactic: have hjac := lie_lie (s x) (s y) (s z)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
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)
x y z : L
hjac :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) =
    -HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
⊢ HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
have hja : Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅⁅x, y⁆, z⁆ : E.L) ((s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)
Tactic: have hja := congr_arg s (lie_lie x y z)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
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)
x y z : L
hjac :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) =
    -HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
hja :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)
⊢ HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : E.L) -
              HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
have hj : Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅⁅y, x⁆, z⁆ : E.L) ((s : (a : L) → E.L) (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆) : E.L)
Tactic: have hj := congr_arg s (lie_lie y x z)
-- 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 : L
⊢ Eq.{u_3 + 1} (α := L)
    ((E.proj : (a : E.L) → L)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) :
      L)
    (0 : L)
have rw : HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
    ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L) =
  0
Tactic: rw [map_sub, sub_eq_zero, hs₁, hs₂]
-- 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 : L
rw :
  HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
      ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L) =
    0
⊢ Eq.{u_3 + 1} (α := L)
    ((E.proj : (a : E.L) → L)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) :
      L)
    (0 : L)
have rw₁ : Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
  ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L)
Tactic: rw [map_sub, sub_eq_zero, hs₁, hs₂]
-- 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 : L
rw :
  HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
      ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L) =
    0
rw₁ :
  Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
    ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L)
⊢ Eq.{u_3 + 1} (α := L)
    ((E.proj : (a : E.L) → L)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) :
      L)
    (0 : L)
have rw₂ : x = (E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L)
Tactic: rw [map_sub, sub_eq_zero, hs₁, hs₂]
-- 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 : L
rw :
  HSub.hSub (α := L) (β := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
      ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L) =
    0
rw₁ :
  Eq.{u_3 + 1} (α := L) ((E.proj : (a : E.L) → L) ((s₁ : (a : L) → E.L) x : E.L) : L)
    ((E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L) : L)
rw₂ : x = (E.proj : (a : E.L) → L) ((s₂ : (a : L) → E.L) x : E.L)
⊢ Eq.{u_3 + 1} (α := L)
    ((E.proj : (a : E.L) → L)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) :
      L)
    (0 : L)
have rw₃ : x = x
Tactic: rw [map_sub, sub_eq_zero, hs₁, hs₂]
-- 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
⊢ (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 : 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)
      (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)) sorry +
        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 [← 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 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)
⊢ (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₁ : 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)
      (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) :
    M)
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]