awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.OfAssociative
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) → x = 0
x y : L
hxy :
  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) 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)
refine_2 : ∀ (m : M), ⁅x - y, m⁆ = 0
⊢ x - y = 0

Tactic:
refine h _ fun m ↦ ?_
-- Module: Mathlib.Algebra.Lie.OfAssociative
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) → x = 0
x y : L
hxy :
  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) 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)
m : M
refine_2 : ⁅x, m⁆ - ⁅y, m⁆ = 0
refine_2₁ : ⁅x, m⁆ = ⁅y, m⁆
refine_2₂ :
  ((((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) :
        (a : M) → M)
      m =
    ⁅y, m⁆
refine_2₃ :
  Eq (α := 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) :
          (a : M) → M)
        m :
      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) :
          (a : M) → M)
        m :
      M)
refine_2₄ refine_2₅ :
  Eq (α := 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) :
          (a : M) → M)
        m :
      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) :
          (a : M) → M)
        m :
      M)
⊢ ⁅x - y, m⁆ = 0

Tactic:
rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]

Premises used: sub_eq_zero, LieModule.toEnd_apply_apply, sub_lie
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
inst_7 : IsFaithful R L M
L' : LieSubalgebra R L
⊢ IsFaithful.{u, v, w} R (↥L') M

Tactic:
⟨(?_ : Injective (toEnd R L M ∘ ((↑) : L' → L)))⟩

Premises used: LieModule.IsFaithful.mk
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
inst_7 : IsFaithful R L M
L' : LieSubalgebra R L
refine :
  Injective.{v + 1, w + 1} (α := ↥L') (β := Module.End R M)
    ((⇑(toEnd R L M) : (a : L) → Module.End R M) ∘ Subtype.val (p := fun (x : L) ↦ x ∈ L'))
⊢ IsFaithful.{u, v, w} R (↥L') M

Tactic:
refine ⟨(?_ : Injective (toEnd R L M ∘ ((↑) : L' → L)))⟩
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
inst_7 : IsFaithful R L M
L' : LieSubalgebra R L
⊢ Injective.{v + 1, w + 1} (α := ↥L') (β := Module.End R M)
    ((⇑(toEnd R L M) : (a : L) → Module.End R M) ∘ Subtype.val (p := fun (x : L) ↦ x ∈ L'))

Tactic:
IsFaithful.injective_toEnd.comp Subtype.val_injective

Premises used: Subtype.val_injective, LieModule.IsFaithful.injective_toEnd, Function.Injective.comp
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
inst_7 : IsFaithful R L M
L' : LieSubalgebra R L
⊢ Injective.{v + 1, w + 1} (α := ↥L') (β := Module.End R M)
    ((⇑(toEnd R L M) : (a : L) → Module.End R M) ∘ Subtype.val (p := fun (x : L) ↦ x ∈ L'))

Tactic:
exact IsFaithful.injective_toEnd.comp Subtype.val_injective

Premises used: Subtype.val_injective, LieModule.IsFaithful.injective_toEnd, Function.Injective.comp
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
⊢ Injective (α := Module.End R M) (β := Module.End R M)
    (⇑(toEnd R (Module.End R M) M) : (a : Module.End R M) → Module.End R M)

Tactic:
simpa using injective_id

Premises used: Function.injective_id
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
y : ↥N
⊢ Eq (α := M)
    ((↑(((((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                Module.End R ↥N) :
              (a : ↥N) → ↥N)
            y) :
        M) :
      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) :
          (a : M) → M)
        (↑y : M) :
      M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
y : ↥N
⊢ Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N) (β := ℕ)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                0 :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := 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 :
          (a : M) → M)
        (↑y : M) :
      M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
n : ℕ
ih :
  ∀ (y : ↥N),
    Eq (α := M)
      ((↑((HPow.hPow (α := Module.End R ↥N)
                  (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                    Module.End R ↥N)
                  n :
                (a : ↥N) → ↥N)
              y) :
          M) :
        M)
      ((HPow.hPow (α := 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)
              n :
            (a : M) → M)
          (↑y : M) :
        M)
y : ↥N
⊢ Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                (n + 1) :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := 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)
            (n + 1) :
          (a : M) → M)
        (↑y : M) :
      M)

Tactic:
simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]

Premises used: LieSubmodule.coe_toEnd, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
y : ↥N
n : ℕ
zero :
  ∀ (y : ↥N),
    Eq (α := M)
      ((↑((HPow.hPow (α := Module.End R ↥N) (β := ℕ)
                  (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                    Module.End R ↥N)
                  0 :
                (a : ↥N) → ↥N)
              y) :
          M) :
        M)
      ((HPow.hPow (α := 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 :
            (a : M) → M)
          (↑y : M) :
        M)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (y : ↥N),
        Eq (α := M)
          ((↑((HPow.hPow (α := Module.End R ↥N)
                      (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N)
                          x :
                        Module.End R ↥N)
                      n :
                    (a : ↥N) → ↥N)
                  y) :
              M) :
            M)
          ((HPow.hPow (α := 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)
                  n :
                (a : M) → M)
              (↑y : M) :
            M))
    (y : ↥N),
    Eq (α := M)
      ((↑((HPow.hPow (α := Module.End R ↥N)
                  (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                    Module.End R ↥N)
                  (n + 1) :
                (a : ↥N) → ↥N)
              y) :
          M) :
        M)
      ((HPow.hPow (α := 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)
              (n + 1) :
            (a : M) → M)
          (↑y : M) :
        M)
⊢ Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                n :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := 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) n :
          (a : M) → M)
        (↑y : M) :
      M)

Tactic:
induction n generalizing y with
  | zero => rfl
  | succ n ih => simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]

Premises used: LieSubmodule.coe_toEnd, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y : ↥H
⊢ Eq (α := L) ((↑((((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) : (a : ↥H) → ↥H) y) : L) : L)
    ((((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) : (a : L) → L) (↑y : L) : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y : ↥H
n : ℕ
⊢ Eq (α := L)
    ((↑((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n :
              (a : ↥H) → ↥H)
            y) :
        L) :
      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)

Tactic:
LieSubmodule.coe_toEnd_pow R H L H.toLieSubmodule x y n

Premises used: Set.Mem, Membership.mem, Subtype, LieSubalgebra.toLieSubmodule, LieSubmodule.coe_toEnd_pow
-- Module: Mathlib.Algebra.Lie.OfAssociative
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 y : L
z : M
⊢ ((((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) : (a : M) → M) ⁅y, z⁆ =
    HAdd.hAdd (β := M)
      (Bracket.bracket (L := L) ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) y : L) z)
      (⁅y,
          ((((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) : (a : M) → M)
            z⁆ :
        M)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y z : L
⊢ (((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) ⁅y, z⁆ =
    HAdd.hAdd (β := L)
      (Bracket.bracket (L := L) ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) y : L) z)
      (⁅y, (((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) z⁆ : L)

Tactic:
toEnd_lie _ x y z

Premises used: LieModule.toEnd_lie
-- Module: Mathlib.Algebra.Lie.OfAssociative
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 y : L
z : M
⊢ Eq (α := M)
    ((HPow.hPow (α := Module.End R M) (β := ℕ)
            (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) 0 :
          (a : M) → M)
        ⁅y, z⁆ :
      M)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
        HSMul.hSMul (β := M) (Nat.choose 0 ij.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                    (a : L) → L)
                  y :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) ij.2 :
                  (a : M) → M)
                z) :
            M) :
      M)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.OfAssociative
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 y : L
z : M
n : ℕ
ih :
  Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n :
          (a : M) → M)
        ⁅y, z⁆ :
      M)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose ij.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                    (a : L) → L)
                  y :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) ij.2 :
                  (a : M) → M)
                z) :
            M) :
      M)
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ (i, j).1 + (i, j).2 = n

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y z : L
n : ℕ
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) ⁅y, z⁆ :
      L)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := L) (n.choose ij.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                    (a : L) → L)
                  y :
                L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 :
                  (a : L) → L)
                z) :
            L) :
      L)

Tactic:
toEnd_pow_lie _ x y z n

Premises used: LieModule.toEnd_pow_lie
-- Module: Mathlib.Algebra.Lie.OfAssociative
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₂ : Type w₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
h :
  ((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x
⊢ HPow.hPow (α := 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₂)
        k ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HPow.hPow (α := 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) k

Tactic:
apply Module.End.commute_pow_left_of_commute

Premises used: Module.End.commute_pow_left_of_commute
-- Module: Mathlib.Algebra.Lie.OfAssociative
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₂ : Type w₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
h :
  ∀ (x_1 : M),
    Eq.{w₁ + 1} (α := M₂)
      ((((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) :
            (a : M) → M₂)
          x_1 :
        M₂)
      (((↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x :
            (a : M) → M₂)
          x_1 :
        M₂)
⊢ ((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.OfAssociative
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₂ : Type w₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
x_1 : M
⊢ Eq.{w₁ + 1} (α := M₂)
    ((((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) :
          (a : M) → M₂)
        x_1 :
      M₂)
    (((↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x :
          (a : M) → M₂)
        x_1 :
      M₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.OfAssociative
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₂ : Type w₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
m : M
⊢ Eq (α := M₂)
    ((HPow.hPow (α := 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₂)
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    ((f : (a : M) → M₂)
        ((HPow.hPow (α := 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)
                k :
              (a : M) → M)
            m :
          M) :
      M₂)

Tactic:
LinearMap.congr_fun (toEnd_pow_comp_lieHom f k x) m

Premises used: LinearMap.congr_fun, LieModule.toEnd_pow_comp_lieHom
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
⊢ Membership.mem (α := M) (↑N : Submodule 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) :
          (a : M) → M)
        m :
      M)

Tactic:
N.lie_mem hm

Premises used: Set.Mem, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
⊢ Membership.mem (α := M) (↑N : Submodule 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) :
          (a : M) → M)
        m :
      M)

Tactic:
exact N.lie_mem hm

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
m : M
hm : m ∈ (↑N : Submodule R M)
⊢ Membership.mem (α := M) (↑N : Submodule R M)
    ((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
            (↑N : Submodule R M).subtype :
          (a : ↥(↑N : Submodule R M)) → M)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑N : Submodule R M)) m hm) :
      M)

Tactic:
simpa using N.lie_mem hm

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
x : L
h :
  ∀ (m : M) (hm : m ∈ (↑N : Submodule R M)),
    Membership.mem (α := M) (↑N : Submodule R M)
      ((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              (↑N : Submodule R M).subtype :
            (a : ↥(↑N : Submodule R M)) → M)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑N : Submodule R M)) m hm) :
        M)
⊢ Eq.{w + 1} (α := ↥(↑N : Submodule R M) →ₗ[R] ↥(↑N : Submodule R M))
    (LinearMap.restrict (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) h)
    (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
φ : R
k : ℕ
x : L
rw :
  MapsTo
    (⇑(HSub.hSub (α := Module.End R M) (β := 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)
            ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) φ : Module.End R M)) :
        (a : M) → M)^[k]
    (↑N : Set M) (↑N : Set M)
⊢ MapsTo
    (⇑(HSub.hSub (α := Module.End R M) (β := 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)
            ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) φ : Module.End R M) ^
          k) :
      (a : M) → M)
    (↑N : Set M) (↑N : Set M)

Tactic:
rw [Module.End.coe_pow]

Premises used: Module.End.coe_pow