awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
I : LieIdeal R L
⊢ Eq (α := LieSubmodule R L M) ⁅I, maxTrivSubmodule R L M⁆ ⊥
have rw : ∀ (x : M),
  Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥(maxTrivSubmodule R L M)), ⁅(↑x_1 : L), (↑n : M)⁆ = x} x →
    x = 0
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span,
    LieSubmodule.bot_toSubmodule, Submodule.span_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ N ≤ maxTrivSubmodule R L M ↔ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
have refine_1 : ∀ (h : N ≤ maxTrivSubmodule R L M), Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
Tactic: refine ⟨fun h => ?_, fun h m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
refine_1 : ∀ (h : N ≤ maxTrivSubmodule R L M), Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
⊢ N ≤ maxTrivSubmodule R L M ↔ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
have refine_2 : ∀ (h : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥) (m : M) (hm : m ∈ N),
  Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m
Tactic: refine ⟨fun h => ?_, fun h m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
have refine_1 : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N ≤ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M)
Tactic: rw [← le_bot_iff, ← ideal_oper_maxTrivSubmodule_eq_bot R L M ⊤]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
h : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ = 0
have refine_2 : ∀ (h : ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ = 0) (m : M) (hm : m ∈ N) (x : L), ⁅x, m⁆ = 0
Tactic: rw [LieSubmodule.lie_eq_bot_iff] at h
Cleared hypotheses: h, m, hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
⊢ IsTrivial L M ↔ Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
have mp : IsTrivial L M → Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
mp : IsTrivial L M → Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
⊢ IsTrivial L M ↔ Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
have mpr : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤ → IsTrivial L M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
⊢ Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
have mp : ∀ (m : M),
  Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m ↔ Membership.mem (γ := LieSubmodule R L M) ⊤ m
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
⊢ IsTrivial L M
have mpr : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
x : L
m : M
⊢ ⁅x, m⁆ = 0
have mpr : ∀ (x : L), ⁅x, m⁆ = 0
Tactic: revert x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
m : M
⊢ ∀ (x : L), ⁅x, m⁆ = 0
have mpr : Membership.mem (γ := LieSubmodule R L M) ⊤ m
Tactic: rw [← mem_maxTrivSubmodule R L M, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m n : ↥(maxTrivSubmodule R L M)
⊢ Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
      ((f : (a : M) → N) (↑(m + n) : M)) ⋯ =
    HAdd.hAdd (α := ↥(maxTrivSubmodule R L N)) (β := ↥(maxTrivSubmodule R L N))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑m : M)) ⋯ :
        ↥(maxTrivSubmodule R L N))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑n : M)) ⋯ :
        ↥(maxTrivSubmodule R L N))
have a : (↑(Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
        ((f : (a : M) → N) (↑(m + n) : M)) sorry) :
    N) =
  (↑(HAdd.hAdd (α := ↥(maxTrivSubmodule R L N)) (β := ↥(maxTrivSubmodule R L N))
        (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
            ((f : (a : M) → N) (↑m : M)) sorry :
          ↥(maxTrivSubmodule R L N))
        (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
            ((f : (a : M) → N) (↑n : M)) sorry :
          ↥(maxTrivSubmodule R L N))) :
    N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : M →ₗ⁅R,L⁆ N
t : R
m : ↥(maxTrivSubmodule R L M)
⊢ Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
      ((f : (a : M) → N) (↑(t • m) : M)) ⋯ =
    HSMul.hSMul (α := R) (β := ↥(maxTrivSubmodule R L N)) ((RingHom.id R : (a : R) → R) t : R)
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑m : M)) ⋯ :
        ↥(maxTrivSubmodule R L N))
have a : (↑(Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
        ((f : (a : M) → N) (↑(t • m) : M)) sorry) :
    N) =
  (↑(HSMul.hSMul (α := R) (β := ↥(maxTrivSubmodule R L N)) ((RingHom.id R : (a : R) → R) t : R)
        (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
            ((f : (a : M) → N) (↑m : M)) sorry :
          ↥(maxTrivSubmodule R L N))) :
    N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
e : M ≃ₗ⁅R,L⁆ N
m : ↥(maxTrivSubmodule R L M)
⊢ ((maxTrivHom e.symm.toLieModuleHom :
          LieModuleHom.{u, v, w₁, w} R L ↥(maxTrivSubmodule R L N) ↥(maxTrivSubmodule R L M)) :
        (a : ↥(maxTrivSubmodule R L N)) → ↥(maxTrivSubmodule R L M))
      (((maxTrivHom e.toLieModuleHom :
            LieModuleHom.{u, v, w, w₁} R L ↥(maxTrivSubmodule R L M) ↥(maxTrivSubmodule R L N)) :
          (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L N))
        m) =
    m
have a : (↑(((maxTrivHom e.symm.toLieModuleHom :
            LieModuleHom.{u, v, w₁, w} R L ↥(maxTrivSubmodule R L N) ↥(maxTrivSubmodule R L M)) :
          (a : ↥(maxTrivSubmodule R L N)) → ↥(maxTrivSubmodule R L M))
        (((maxTrivHom e.toLieModuleHom :
              LieModuleHom.{u, v, w, w₁} R L ↥(maxTrivSubmodule R L M) ↥(maxTrivSubmodule R L N)) :
            (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L N))
          m)) :
    M) =
  (↑m : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
e : M ≃ₗ⁅R,L⁆ N
n : ↥(maxTrivSubmodule R L N)
⊢ ((maxTrivHom e.toLieModuleHom : LieModuleHom.{u, v, w, w₁} R L ↥(maxTrivSubmodule R L M) ↥(maxTrivSubmodule R L N)) :
        (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L N))
      (((maxTrivHom e.symm.toLieModuleHom :
            LieModuleHom.{u, v, w₁, w} R L ↥(maxTrivSubmodule R L N) ↥(maxTrivSubmodule R L M)) :
          (a : ↥(maxTrivSubmodule R L N)) → ↥(maxTrivSubmodule R L M))
        n) =
    n
have a : (↑(((maxTrivHom e.toLieModuleHom : LieModuleHom.{u, v, w, w₁} R L ↥(maxTrivSubmodule R L M) ↥(maxTrivSubmodule R L N)) :
          (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L N))
        (((maxTrivHom e.symm.toLieModuleHom :
              LieModuleHom.{u, v, w₁, w} R L ↥(maxTrivSubmodule R L N) ↥(maxTrivSubmodule R L M)) :
            (a : ↥(maxTrivSubmodule R L N)) → ↥(maxTrivSubmodule R L M))
          n)) :
    N) =
  (↑n : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
⊢ Eq.{w + 1} (α := ↥(maxTrivSubmodule R L M) ≃ₗ⁅R,L⁆ ↥(maxTrivSubmodule R L M)) (maxTrivEquiv LieModuleEquiv.refl)
    LieModuleEquiv.refl
have h : ∀ (m : ↥(maxTrivSubmodule R L M)),
  Eq.{w + 1} (α := M)
    (↑((maxTrivEquiv LieModuleEquiv.refl : (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L M)) m) : M)
    (↑((LieModuleEquiv.refl : (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L M)) m) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ Eq.{w₁ + 1} (α := N) ((⁅x, (↑f : M →ₗ[R] N)⁆ : (a : M) → N) m : N) (0 : N)
have rw : Eq.{w₁ + 1} (α := N) ((0 : (a : M) → N) m : N) (0 : N)
Tactic: rw [f.property x, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
rw : Eq.{w₁ + 1} (α := N) ((0 : (a : M) → N) m : N) (0 : N)
⊢ Eq.{w₁ + 1} (α := N) ((⁅x, (↑f : M →ₗ[R] N)⁆ : (a : M) → N) m : N) (0 : N)
have rw₁ : Eq.{w₁ + 1} (α := N) 0 0
Tactic: rw [f.property x, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ (↑f : M →ₗ[R] N).toFun ⁅x, m⁆ = ⁅x, (↑f : M →ₗ[R] N).toFun m⁆
have hf : Eq.{w₁ + 1} (α := N) ((⁅x, (↑f : M →ₗ[R] N)⁆ : (a : M) → N) m : N) (0 : N)
Tactic: have hf : ⁅x, f.val⁆ m = 0 := by rw [f.property x, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
hf : Eq.{w₁ + 1} (α := N) ((⁅x, (↑f : M →ₗ[R] N)⁆ : (a : M) → N) m : N) (0 : N)
⊢ (↑f : M →ₗ[R] N).toFun ⁅x, m⁆ = ⁅x, (↑f : M →ₗ[R] N).toFun m⁆
have hf₁ : ⁅x, (↑f : M →ₗ[R] N).toFun m⁆ = (↑f : M →ₗ[R] N).toFun ⁅x, m⁆
Tactic: rw [LieHom.lie_apply, sub_eq_zero, ← LinearMap.toFun_eq_coe] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f g : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ (let __LinearMap := (↑(f + g) : M →ₗ[R] N);
    { toLinearMap := __LinearMap, map_lie' := ⋯ }) =
    HAdd.hAdd (α := M →ₗ⁅R,L⁆ N)
      (let __LinearMap := (↑f : M →ₗ[R] N);
      { toLinearMap := __LinearMap, map_lie' := ⋯ : M →ₗ⁅R,L⁆ N })
      (let __LinearMap := (↑g : M →ₗ[R] N);
      { toLinearMap := __LinearMap, map_lie' := ⋯ : M →ₗ⁅R,L⁆ N })
have h : ∀ (m : M),
  Eq.{w₁ + 1} (α := N)
    ((let __LinearMap := (↑(f + g) : M →ₗ[R] N);
          { toLinearMap := __LinearMap, map_lie' := sorry } :
          (a : M) → N)
        m :
      N)
    ((HAdd.hAdd (α := M →ₗ⁅R,L⁆ N)
            (let __LinearMap := (↑f : M →ₗ[R] N);
            { toLinearMap := __LinearMap, map_lie' := sorry : M →ₗ⁅R,L⁆ N })
            (let __LinearMap := (↑g : M →ₗ[R] N);
            { toLinearMap := __LinearMap, map_lie' := sorry : M →ₗ⁅R,L⁆ N }) :
          (a : M) → N)
        m :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
F : R
G : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ (let __LinearMap := (↑(F • G) : M →ₗ[R] N);
    { toLinearMap := __LinearMap, map_lie' := ⋯ }) =
    HSMul.hSMul (α := R) (β := M →ₗ⁅R,L⁆ N) ((RingHom.id R : (a : R) → R) F : R)
      (let __LinearMap := (↑G : M →ₗ[R] N);
      { toLinearMap := __LinearMap, map_lie' := ⋯ : M →ₗ⁅R,L⁆ N })
have h : ∀ (m : M),
  Eq.{w₁ + 1} (α := N)
    ((let __LinearMap := (↑(F • G) : M →ₗ[R] N);
          { toLinearMap := __LinearMap, map_lie' := sorry } :
          (a : M) → N)
        m :
      N)
    ((HSMul.hSMul (α := R) (β := M →ₗ⁅R,L⁆ N) ((RingHom.id R : (a : R) → R) F : R)
            (let __LinearMap := (↑G : M →ₗ[R] N);
            { toLinearMap := __LinearMap, map_lie' := sorry : M →ₗ⁅R,L⁆ N }) :
          (a : M) → N)
        m :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
F : M →ₗ⁅R,L⁆ N
x : L
⊢ ⁅x, (↑F : M →ₗ[R] N)⁆ = 0
have h : ∀ (x_1 : M), Eq.{w₁ + 1} (α := N) ((⁅x, (↑F : M →ₗ[R] N)⁆ : (a : M) → N) x_1 : N) ((0 : (a : M) → N) x_1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ Eq (α := (a : M) → N)
    (⇑((maxTrivLinearMapEquivLieModuleHom : (a : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) → M →ₗ⁅R,L⁆ N) f : M →ₗ⁅R,L⁆ N) :
      (a : M) → N)
    (⇑(↑f : M →ₗ[R] N) : (a : M) → N)
have h : ∀ (x : M),
  Eq.{w₁ + 1} (α := N)
    ((((maxTrivLinearMapEquivLieModuleHom : (a : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) → M →ₗ⁅R,L⁆ N) f : M →ₗ⁅R,L⁆ N) :
          (a : M) → N)
        x :
      N)
    (((↑f : M →ₗ[R] N) : (a : M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
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
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ (↑((maxTrivLinearMapEquivLieModuleHom : (a : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) → M →ₗ⁅R,L⁆ N) f) : M →ₗ[R] N) =
    (↑f : M →ₗ[R] N)
have h : ∀ (x : M),
  Eq.{w₁ + 1} (α := N)
    (((↑((maxTrivLinearMapEquivLieModuleHom : (a : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) → M →ₗ⁅R,L⁆ N) f) : M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)
    (((↑f : M →ₗ[R] N) : (a : M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := LieIdeal R L) (LieModule.ker R L L) (center R L)
have h : ∀ (y : L),
  Membership.mem (γ := LieSubmodule R L L) (LieModule.ker R L L) y ↔
    Membership.mem (γ := LieSubmodule R L L) (center R L) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LieModule.IsFaithful R L L ↔ Eq (α := LieIdeal R L) (center R L) ⊥
have rw : Eq (α := LieIdeal R L) (LieModule.ker R L L) ⊥ ↔ Eq (α := LieIdeal R L) (center R L) ⊥
Tactic: rw [LieModule.isFaithful_iff_ker_eq_bot, self_module_ker_eq_center]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
rw : Eq (α := LieIdeal R L) (LieModule.ker R L L) ⊥ ↔ Eq (α := LieIdeal R L) (center R L) ⊥
⊢ LieModule.IsFaithful R L L ↔ Eq (α := LieIdeal R L) (center R L) ⊥
have rw₁ : Eq (α := LieIdeal R L) (center R L) ⊥ ↔ Eq (α := LieIdeal R L) (center R L) ⊥
Tactic: rw [LieModule.isFaithful_iff_ker_eq_bot, self_module_ker_eq_center]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x
y : L
⊢ Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw : Commute.{w} (S := Module.End R M)
  (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
  (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
Tactic: rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x
y : L
rw :
  Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
⊢ Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw₁ : Eq.{w + 1} (α := Module.End R M)
  (Bracket.bracket (L := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
    Module.End R M)
  (0 : Module.End R M)
Tactic: rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x
y : L
rw :
  Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
rw₁ :
  Eq.{w + 1} (α := Module.End R M)
    (Bracket.bracket (L := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
      Module.End R M)
    (0 : Module.End R M)
⊢ Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw₂ : Eq.{w + 1} (α := Module.End R M)
  (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) ⁅y, x⁆ : Module.End R M)
  (0 : Module.End R M)
Tactic: rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, map_zero]