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
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
⊢ 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
have h : ∀ (n : M)
  (h :
    ((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := sorry,
                map_smul' := sorry, map_lie' := sorry } :
            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' := sorry, map_smul' := sorry, map_lie' := sorry }))
    x
Tactic: obtain ⟨n, h⟩ := hx
Cleared hypotheses: hx
-- 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
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 (γ := 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
have 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' := sorry, map_smul' := sorry, map_lie' := sorry }))
  (((↑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := sorry,
              map_smul' := sorry, map_lie' := sorry } :
          M →ₗ[R] LieAlgebra.ofTwoCocycle c) :
        (a : M) → LieAlgebra.ofTwoCocycle c)
      n :
    LieAlgebra.ofTwoCocycle c)
Tactic: rw [← h]
-- 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
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
⊢ 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
have this : 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
-- 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
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
⊢ ∃ (y : M), (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, y) = x
have h : (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
    (0, (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) =
  x
Tactic: use ((ofProd c).symm x).2
-- 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
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
⊢ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c)
      (0, (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).2) =
    x
have 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)
Tactic: nth_rw 2 [← Equiv.apply_symm_apply (ofProd c) x]
-- 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
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
⊢ 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)
have 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)
Tactic: rw [← this]
-- 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
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : E.L
y : M
⊢ Membership.mem (α := E.L) E.proj.ker (⁅x, (E.incl : (a : M) → E.L) y⁆ : E.L)
have 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)
Tactic: rw [LieHom.mem_ker, LieHom.map_lie, proj_incl, lie_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
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)
⊢ Membership.mem (α := E.L) E.proj.ker (⁅x, (E.incl : (a : M) → E.L) y⁆ : E.L)
have 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)
Tactic: rw [LieHom.mem_ker, LieHom.map_lie, proj_incl, lie_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
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)
⊢ Membership.mem (α := E.L) E.proj.ker (⁅x, (E.incl : (a : M) → E.L) y⁆ : E.L)
have rw₂ : Eq.{u_3 + 1} (α := L) (Bracket.bracket (L := L) ((E.proj : (a : E.L) → L) x : L) 0) 0
Tactic: rw [LieHom.mem_ker, LieHom.map_lie, proj_incl, lie_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
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
⊢ Membership.mem (α := E.L) E.proj.ker (⁅x, (E.incl : (a : M) → E.L) y⁆ : E.L)
have rw₃ : Eq.{u_3 + 1} (α := L) 0 0
Tactic: rw [LieHom.mem_ker, LieHom.map_lie, proj_incl, lie_zero]
-- 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
x y : M
⊢ 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)
have 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⁆) sorry) : 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) sorry : ↥E.proj.ker)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker) ((E.incl : (a : M) → E.L) y) sorry)) :
      E.L) :
    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
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : M
⊢ 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
have 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 sorry : (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) sorry) :
    ↥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) sorry :
    { x : E.L // Membership.mem (γ := Set E.L) (Set.range.{u_5, u_4 + 1} (ι := M) (⇑E.incl : (a : M) → E.L)) x })
Tactic: simp [IsExtension.kerEquivRange, Equiv.symm_apply_eq]
-- 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
x y : L
m : M
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h (x + y),
          (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
        ↥E.proj.ker) =
    HAdd.hAdd (α := M) (β := 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)) h x,
              (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
            ↥E.proj.ker) :
        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)) h y,
              (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
            ↥E.proj.ker) :
        M)
have rw : Eq (α := ↥E.proj.ker)
  (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x +
          Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y -
        Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h (x + y),
      (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
    ↥E.proj.ker)
  (0 : ↥E.proj.ker)
Tactic: rw [← map_add, ← add_lie, eq_comm, 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
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
x y : L
m : M
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
z : ↥E.proj.ker
⊢ Eq (α := ↥E.proj.ker)
    (⁅⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
          Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y⁆,
        z⁆ :
      ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h ⁅x, y⁆, z⁆ :
      ↥E.proj.ker)
have rw : ⁅⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
        Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y⁆ -
      Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h ⁅x, y⁆,
    z⁆ =
  0
Tactic: rw [← sub_eq_zero, ← sub_lie]
-- 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
x y : L
m : M
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
          (E.toKer : (a : M) → ↥E.proj.ker)
            ((E.toKer.symm : (a : ↥E.proj.ker) → M)
              (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y,
                  (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                ↥E.proj.ker))⁆ :
        ↥E.proj.ker) =
    HAdd.hAdd (α := M) (β := 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)) h ⁅x, y⁆,
              (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
            ↥E.proj.ker) :
        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)) h y,
              (E.toKer : (a : M) → ↥E.proj.ker)
                ((E.toKer.symm : (a : ↥E.proj.ker) → M)
                  (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
                      (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                    ↥E.proj.ker))⁆ :
            ↥E.proj.ker) :
        M)
have aux : ∀ (z : ↥E.proj.ker),
  Eq (α := ↥E.proj.ker)
    (⁅⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
          Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y⁆,
        z⁆ :
      ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h ⁅x, y⁆, z⁆ :
      ↥E.proj.ker)
Tactic: have aux (z : E.proj.ker) : ⁅⁅h.choose x, h.choose y⁆, z⁆ = ⁅h.choose ⁅x, y⁆, z⁆ := by
      rw [← sub_eq_zero, ← sub_lie]
      exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ z
-- 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
⊢ 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.incl.range
have rw : 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 ∈
  LieIdeal.toLieSubalgebra R E.L E.proj.ker
Tactic: rw [E.IsExtension.exact]
-- 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
⊢ 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 obtain : ∀ (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)) sorry
          ((E.proj : (a : E.L) → L) z) -
        z),
  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)
Tactic: obtain ⟨x, hx⟩ : E.proj_surjective.hasRightInverse.choose (E.proj z) - z ∈ E.incl.range := by
    rw [E.IsExtension.exact]
    change _ ∈ E.proj.ker
    simp [E.proj_surjective.hasRightInverse.choose_spec (E.proj z)]
-- 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
⊢ 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_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)) sorry
            ((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)
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)
⊢ 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),
      (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
    ↥E.proj.ker)
  (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥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]