awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
h :
  ∀ (hmn : m ≤ n),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
have h₁ : ∀ (hmn : n ≤ m),
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
Tactic: obtain (hmn | hmn) : m ≤ n ∨ n ≤ m := le_total m n
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : n ≤ m
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
have this : ∀ (k : ℕ),
  Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k : (a : L) → L)
          (↑y : L) :
        L)
      (0 : L) ↔
    Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y
Tactic: have : ∀ k : ℕ, ((ad R L) x ^ k) y = 0 ↔ y ∈ K k := by simp [K, Subtype.ext_iff, coe_ad_pow]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : n ≤ m
this :
  ∀ (k : ℕ),
    Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
              (a : L) → L)
            (↑y : L) :
          L)
        (0 : L) ↔
      Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
have h : ∀ (hm : Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H) y) (hmn : n ≤ m)
  (this :
    ∀ (k : ℕ),
      Eq (α := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
                (a : L) → L)
              (↑y : L) :
            L)
          (0 : L) ↔
        Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y),
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
Tactic: rwa [this, ← hn m hmn, ← this] at hm
Cleared hypotheses: hm, hmn, this
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : n ≤ m
this :
  ∀ (k : ℕ),
    Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
              (a : L) → L)
            (↑y : L) :
          L)
        (0 : L) ↔
      Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y
h :
  ∀ (hm : Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H) y) (hmn : n ≤ m)
    (this :
      ∀ (k : ℕ),
        Eq (α := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
                  (a : L) → L)
                (↑y : L) :
              L)
            (0 : L) ↔
          Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
have h₁ : ∀ (hm : Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H) y) (hmn : n ≤ m)
  (this :
    ∀ (k : ℕ),
      Eq (α := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
                (a : L) → L)
              (↑y : L) :
            L)
          (0 : L) ↔
        Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y),
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
Tactic: rwa [this, ← hn m hmn, ← this] at hm
Cleared hypotheses: hm, hmn, this
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x : ofTwoCocycle c
⊢ Eq (α := ofTwoCocycle c)
    ((ofProd c : (a : L × M) → ofTwoCocycle c)
        (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1,
          HAdd.hAdd (α := M) (β := M)
              ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2 :
                M) -
            Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) :
      ofTwoCocycle c)
    (0 : ofTwoCocycle c)
have rw : Eq (α := ofTwoCocycle c)
  ((ofProd c : (a : L × M) → ofTwoCocycle c)
      (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1,
        HAdd.hAdd (α := M) 0
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) -
          Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) :
    ofTwoCocycle c)
  ((ofProd c : (a : L × M) → ofTwoCocycle c) 0 : ofTwoCocycle c)
Tactic: rw [← of_zero, c.1.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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← of_add]
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine Equiv.congr_arg ?_
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
r : R
x y : ofTwoCocycle c
⊢ ⁅x, r • y⁆ = r • ⁅x, y⁆
have simp : (ofProd c : (a : L × M) → ofTwoCocycle c)
    (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).1,
      HAdd.hAdd (α := M) (β := M)
          ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).1 :
            M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).2 :
            M) -
        Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (r • y)).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) =
  HSMul.hSMul (β := ofTwoCocycle c) r
    ((ofProd c : (a : L × M) → ofTwoCocycle c)
        (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1,
          HAdd.hAdd (α := M) (β := M)
              ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2 :
                M) -
            Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2) :
      ofTwoCocycle c)
Tactic: simp only [bracket_ofTwoCocycle]
-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
x_1 x_2 : ofTwoCocycle c
⊢ (ofProd c' : (a : L × M) → ofTwoCocycle c')
      ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x_1 + x_2)).1,
        HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x_1 + x_2)).2 : M)
          ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x_1 + x_2)).1 : M)) =
    HAdd.hAdd (α := ofTwoCocycle c') (β := ofTwoCocycle c')
      ((ofProd c' : (a : L × M) → ofTwoCocycle c')
          ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1,
            HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
              ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)) :
        ofTwoCocycle c')
      ((ofProd c' : (a : L × M) → ofTwoCocycle c')
          ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1,
            HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 : M)
              ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M)) :
        ofTwoCocycle c')
have simp : HAdd.hAdd (α := M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2
      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 -
    HAdd.hAdd (α := M) (β := M) ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)
      ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M) =
  HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
      ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M) +
    HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).2 : M)
      ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_2).1 : M)
Tactic: simp [← of_add]
-- 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)
⊢ Eq.{u_4 + 1} (α := LieIdeal R M)
    (LieHom.ker (L' := LieAlgebra.ofTwoCocycle c)
      { toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := ⋯,
        map_smul' := ⋯, map_lie' := ⋯ })
    ⊥
have rw : Injective (α := M) (β := LieAlgebra.ofTwoCocycle c)
  (⇑{ toFun := fun (x : M) ↦ (ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (0, x), map_add' := sorry, map_smul' := sorry,
        map_lie' := sorry } :
    (a : M) → LieAlgebra.ofTwoCocycle c)
Tactic: rw [LieHom.ker_eq_bot]
-- 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)
⊢ Eq.{u_3 + 1} (α := LieSubalgebra R L)
    (LieHom.range (L := LieAlgebra.ofTwoCocycle c)
      {
        toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦
          (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
        map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ })
    ⊤
have rw : Surjective (α := LieAlgebra.ofTwoCocycle c) (β := 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 } :
    (a : LieAlgebra.ofTwoCocycle c) → L)
Tactic: rw [LieHom.range_eq_top]
-- 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 : L
⊢ ∃ (a : LieAlgebra.ofTwoCocycle c),
    ({ toFun := fun (x : LieAlgebra.ofTwoCocycle c) ↦ (((ofProd c).symm : (a : LieAlgebra.ofTwoCocycle c) → L × M) x).1,
            map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
          (a : LieAlgebra.ofTwoCocycle c) → L)
        a =
      x
have h : ({ 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 } :
      (a : LieAlgebra.ofTwoCocycle c) → L)
    ((ofProd c : (a : L × M) → LieAlgebra.ofTwoCocycle c) (x, 0) : LieAlgebra.ofTwoCocycle c) =
  x
Tactic: use (ofProd c (x, 0))
-- 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)
⊢ Eq (α := 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' := ⋯ })
    (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' := ⋯ }))
have h : ∀ (x : LieAlgebra.ofTwoCocycle c),
  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' := sorry,
          map_smul' := sorry, map_lie' := sorry })
      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: ext 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
⊢ 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 : 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' := sorry,
        map_smul' := sorry, map_lie' := sorry })
    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: constructor
-- 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
h :
  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
⊢ 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₁ : 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 →
  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' := sorry,
        map_smul' := sorry, map_lie' := sorry })
    x
Tactic: constructor