awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
⊢ IsLieAbelian.{u_5} ↥E.proj.ker

Tactic:
(lie_abelian_iff_equiv_lie_abelian E.toKer.symm).mpr inferInstance

Premises used: Iff.mpr, lie_abelian_iff_equiv_lie_abelian, inferInstance, LieAlgebra.Extension.toKer, LieEquiv.symm
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x y : L
m : M
set :
  let h := ⋯;
  (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)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ (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)) ⋯ 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)) ⋯ y,
              (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
            ↥E.proj.ker) :
        M)

Tactic:
set h := E.proj_surjective.hasRightInverse

Premises used: Function.Surjective.hasRightInverse, LieAlgebra.Extension.proj_surjective
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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) := ⋯
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)
⊢ (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)

Tactic:
rw [← map_add, ← add_lie, eq_comm, EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]

Premises used: sub_eq_zero, EquivLike.apply_eq_iff_eq, map_add, eq_comm, sub_lie, add_lie
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
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) := ⋯
⊢ 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.proj.ker

Tactic:
simp [h.choose_spec _]

Premises used: Exists.choose_spec
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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) := ⋯
⊢ 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:
exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)

Premises used: LieAlgebra.Extension.proj, Membership.mem, Subtype, Subtype.mk, LieHom.ker, LieAlgebra.Extension.toKer, trivial_lie_zero, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : L
m n : 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)) ⋯ x,
          (E.toKer : (a : M) → ↥E.proj.ker) (m + n)⁆ :
        ↥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)) ⋯ 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)) ⋯ x,
              (E.toKer : (a : M) → ↥E.proj.ker) n⁆ :
            ↥E.proj.ker) :
        M)

Tactic:
simp [← map_add, ← lie_add]

Premises used: map_add, lie_add
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x y : L
m : M
set :
  let h := ⋯;
  (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)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ 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)) ⋯ 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)) ⋯ ⁅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)) ⋯ 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)) ⋯ x,
                      (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                    ↥E.proj.ker))⁆ :
            ↥E.proj.ker) :
        M)

Tactic:
set h := E.proj_surjective.hasRightInverse

Premises used: Function.Surjective.hasRightInverse, LieAlgebra.Extension.proj_surjective
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
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
⊢ 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:
rw [← sub_eq_zero, ← sub_lie]

Premises used: sub_eq_zero, sub_lie
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
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
⊢ ⁅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.proj.ker

Tactic:
simp [h.choose_spec _]

Premises used: Exists.choose_spec
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
⊢ ⁅⁅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:
exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ z

Premises used: LieAlgebra.Extension.proj, Membership.mem, Subtype, Subtype.mk, LieHom.ker, trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
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)

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
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
rw :
  Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z ∈
    LieIdeal.toLieSubalgebra R E.L 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.incl.range

Tactic:
rw [E.IsExtension.exact]

Premises used: LieAlgebra.IsExtension.exact
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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.proj.ker

Tactic:
simp [E.proj_surjective.hasRightInverse.choose_spec (E.proj z)]

Premises used: Exists.choose_spec, Function.Surjective.hasRightInverse, LieAlgebra.Extension.proj, LieAlgebra.Extension.proj_surjective, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
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)) ⋯
            ((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)
⊢ 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)]

Premises used: Function.Surjective.hasRightInverse, LieAlgebra.Extension.proj, LieHom.range, Exists.choose, LieAlgebra.Extension.incl, LieAlgebra.Extension.proj_surjective, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
rw :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ (r • x) -
          r • Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ x,
        (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
      ↥E.proj.ker)
    (0 : ↥E.proj.ker)
⊢ ⁅r • x, m⁆ = r • ⁅x, m⁆

Tactic:
rw [ringModuleOf_bracket, ringModuleOf_bracket, ← map_smul, ← smul_lie,
          EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]

Premises used: sub_eq_zero, EquivLike.apply_eq_iff_eq, LieAlgebra.Extension.ringModuleOf_bracket, smul_lie, sub_lie, map_smul
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
⊢ Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ (r • x) -
      r • Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ x ∈
    E.proj.ker

Tactic:
simp [h.choose_spec _]

Premises used: Exists.choose_spec
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
⊢ Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ (r • x) -
          r • Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ x,
        (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
      ↥E.proj.ker)
    (0 : ↥E.proj.ker)

Tactic:
exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)

Premises used: LieAlgebra.Extension.proj, Membership.mem, Subtype, Subtype.mk, LieHom.ker, LieAlgebra.Extension.toKer, trivial_lie_zero, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
⊢ ⁅x, r • m⁆ = r • ⁅x, m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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) := ⋯
⊢ LieModule R L M

Tactic:
exact
    { smul_lie r x m := by
        rw [ringModuleOf_bracket, ringModuleOf_bracket, ← map_smul, ← smul_lie,
          EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]
        exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)
      lie_smul r x m := by simp }
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x : ↥E.proj.ker
y : L
⊢ Eq (α := ↥E.proj.ker) ((E.toKer : (a : M) → ↥E.proj.ker) ⁅y, (E.toKer.symm : (a : ↥E.proj.ker) → M) x⁆ : ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯ y, x⁆ : ↥E.proj.ker)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
rw : ⁅HSub.hSub (α := E.L) ((s : (a : L) → E.L) ((E.proj : (a : E.L) → L) x) : E.L) x, y⁆ = 0
⊢ Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ((E.proj : (a : E.L) → L) x) : E.L) y = ⁅x, y⁆

Tactic:
rw [← sub_eq_zero, ← sub_lie]

Premises used: sub_eq_zero, sub_lie
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
⊢ HSub.hSub (α := E.L) ((s : (a : L) → E.L) ((E.proj : (a : E.L) → L) x) : E.L) x ∈ E.proj.ker

Tactic:
simp [hs.eq]

Premises used: Function.LeftInverse.eq
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
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
⊢ ⁅HSub.hSub (α := E.L) ((s : (a : L) → E.L) ((E.proj : (a : E.L) → L) x) : E.L) x, y⁆ = 0

Tactic:
exact trivial_lie_zero E.proj.ker E.proj.ker ⟨_, (by simp [hs.eq])⟩ y

Premises used: LieAlgebra.Extension.proj, Membership.mem, Subtype, Subtype.mk, LieHom.ker, trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
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 : 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) y) : E.L)
      ((s : (a : L) → E.L) ⁅x, y⁆ : E.L) ∈
    E.proj.ker

Tactic:
simp [hs.eq]

Premises used: Function.LeftInverse.eq