awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Abelian
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)
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)) ⋯) :
      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)) ⋯ :
            ↥(maxTrivSubmodule R L N))) :
      N)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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)) ⋯) :
      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)) ⋯ :
            ↥(maxTrivSubmodule R L N))) :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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
m : ↥(maxTrivSubmodule R L M)
⊢ Eq.{w₁ + 1} (α := ↥(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) (↑⁅x, m⁆ : M)) ⋯ :
      ↥(maxTrivSubmodule R L N))
    (⁅x,
        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))

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Abelian
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 : ↥(maxTrivSubmodule R L M)
⊢ Eq.{w₁ + 1} (α := N)
    ((↑(((maxTrivHom f : 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) :
        N) :
      N)
    ((f : (a : M) → N) (↑m : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Abelian
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)
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)
⊢ ((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

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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) =
    (↑m : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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)
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)
⊢ ((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

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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) =
    (↑n : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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)
⊢ Eq.{w₁ + 1} (α := N)
    ((↑(((maxTrivEquiv e : LieModuleEquiv.{u, v, w, w₁} R L ↥(maxTrivSubmodule R L M) ↥(maxTrivSubmodule R L N)) :
              (a : ↥(maxTrivSubmodule R L M)) → ↥(maxTrivSubmodule R L N))
            m) :
        N) :
      N)
    ((e : (a : M) → N) (↑m : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Abelian
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 :
  ∀ (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)
⊢ Eq.{w + 1} (α := ↥(maxTrivSubmodule R L M) ≃ₗ⁅R,L⁆ ↥(maxTrivSubmodule R L M)) (maxTrivEquiv LieModuleEquiv.refl)
    LieModuleEquiv.refl

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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
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:
simp only [coe_maxTrivEquiv_apply, LieModuleEquiv.refl_apply]

Premises used: LieModuleEquiv.refl_apply, LieModule.coe_maxTrivEquiv_apply
-- Module: Mathlib.Algebra.Lie.Abelian
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
⊢ Eq (α := LieModuleEquiv.{u, v, w₁, w} R L ↥(maxTrivSubmodule R L N) ↥(maxTrivSubmodule R L M))
    (LieModuleEquiv.symm (maxTrivEquiv e)) (maxTrivEquiv e.symm)

Tactic:
rfl

Premises used: LieModuleHom.inverse, LieModuleEquiv.symm, LieModule.maxTrivEquiv, LinearMap.inverse, rfl
-- Module: Mathlib.Algebra.Lie.Abelian
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)
rw₁ rw₂ : Eq.{w₁ + 1} (α := N) 0 0
⊢ Eq.{w₁ + 1} (α := N) ((⁅x, (↑f : M →ₗ[R] N)⁆ : (a : M) → N) m : N) (0 : N)

Tactic:
rw [f.property x, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, Subtype.property
-- Module: Mathlib.Algebra.Lie.Abelian
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)

Tactic:
have hf : ⁅x, f.val⁆ m = 0 := by rw [f.property x, LinearMap.zero_apply]
-- Module: Mathlib.Algebra.Lie.Abelian
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)
⊢ ⁅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

Premises used: sub_eq_zero, LinearMap.toFun_eq_coe, LieHom.lie_apply
-- Module: Mathlib.Algebra.Lie.Abelian
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 : ⁅x, (↑f : M →ₗ[R] N).toFun m⁆ = (↑f : M →ₗ[R] N).toFun ⁅x, m⁆
⊢ (↑f : M →ₗ[R] N).toFun ⁅x, m⁆ = ⁅x, (↑f : M →ₗ[R] N).toFun m⁆

Tactic:
hf.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Lie.Abelian
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 : ⁅x, (↑f : M →ₗ[R] N).toFun m⁆ = (↑f : M →ₗ[R] N).toFun ⁅x, m⁆
⊢ (↑f : M →ₗ[R] N).toFun ⁅x, m⁆ = ⁅x, (↑f : M →ₗ[R] N).toFun m⁆

Tactic:
exact hf.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Lie.Abelian
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))
h :
  ∀ (m : M),
    Eq.{w₁ + 1} (α := N)
      ((let __LinearMap := (↑(f + g) : M →ₗ[R] N);
            { toLinearMap := __LinearMap, map_lie' := ⋯ } :
            (a : M) → N)
          m :
        N)
      ((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 }) :
            (a : M) → N)
          m :
        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 })

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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))
m : M
⊢ Eq.{w₁ + 1} (α := N)
    ((let __LinearMap := (↑(f + g) : M →ₗ[R] N);
          { toLinearMap := __LinearMap, map_lie' := ⋯ } :
          (a : M) → N)
        m :
      N)
    ((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 }) :
          (a : M) → N)
        m :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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))
h :
  ∀ (m : M),
    Eq.{w₁ + 1} (α := N)
      ((let __LinearMap := (↑(F • G) : M →ₗ[R] N);
            { toLinearMap := __LinearMap, map_lie' := ⋯ } :
            (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' := ⋯ : M →ₗ⁅R,L⁆ N }) :
            (a : M) → N)
          m :
        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 })

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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))
m : M
⊢ Eq.{w₁ + 1} (α := N)
    ((let __LinearMap := (↑(F • G) : M →ₗ[R] N);
          { toLinearMap := __LinearMap, map_lie' := ⋯ } :
          (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' := ⋯ : M →ₗ⁅R,L⁆ N }) :
          (a : M) → N)
        m :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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
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)
⊢ ⁅x, (↑F : M →ₗ[R] N)⁆ = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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_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:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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))
⊢ (fun (F : M →ₗ⁅R,L⁆ N) ↦
        (Subtype.mk (p := fun (x : M →ₗ[R] N) ↦
            Membership.mem (γ := LieSubmodule R L (M →ₗ[R] N)) (maxTrivSubmodule R L (M →ₗ[R] N)) x) (↑F : M →ₗ[R] N)
            ⋯ :
          ↥(maxTrivSubmodule R L (M →ₗ[R] N))))
      ((fun (f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) ↦
          let __LinearMap := (↑f : M →ₗ[R] N);
          ({ toLinearMap := __LinearMap, map_lie' := ⋯ } : M →ₗ⁅R,L⁆ N))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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
⊢ (fun (f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) ↦
        let __LinearMap := (↑f : M →ₗ[R] N);
        ({ toLinearMap := __LinearMap, map_lie' := ⋯ } : M →ₗ⁅R,L⁆ N))
      ((fun (F : M →ₗ⁅R,L⁆ N) ↦
          (Subtype.mk (p := fun (x : M →ₗ[R] N) ↦
              Membership.mem (γ := LieSubmodule R L (M →ₗ[R] N)) (maxTrivSubmodule R L (M →ₗ[R] N)) x) (↑F : M →ₗ[R] N)
              ⋯ :
            ↥(maxTrivSubmodule R L (M →ₗ[R] N))))
        F) =
    F

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
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))
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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 : 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:
rfl
-- Module: Mathlib.Algebra.Lie.Abelian
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
⊢ Eq (α := (a : M) → N)
    (⇑(↑((LinearEquiv.symm maxTrivLinearMapEquivLieModuleHom : (a : M →ₗ⁅R,L⁆ N) → ↥(maxTrivSubmodule R L (M →ₗ[R] N)))
              f) :
          M →ₗ[R] N) :
      (a : M) → N)
    (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Abelian
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))
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)
⊢ (↑((maxTrivLinearMapEquivLieModuleHom : (a : ↥(maxTrivSubmodule R L (M →ₗ[R] N))) → M →ₗ⁅R,L⁆ N) f) : M →ₗ[R] N) =
    (↑f : M →ₗ[R] N)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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 : 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:
rfl