awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
⊢ HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)

Tactic:
have h : (toEnd R L M₂ x - χ x • ↑1) ∘ₗ f =
             f ∘ₗ (toEnd R L M x - χ x • ↑1) := by ext; simp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
refine_1 :
  ∀ (k : ℕ)
    (hk :
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)),
    ∃ (k : ℕ),
      Eq (α := M)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M)
        (0 : M)
⊢ ∃ (k : ℕ),
    Eq (α := M)
      ((HSub.hSub (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                  Module.End R M)
                (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)

Tactic:
obtain ⟨k, hk⟩ := hm x
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
hk :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    (0 : M₂)
h₁ :
  Eq (α := M)
    ((HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
            k :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ ∃ (k : ℕ),
    Eq (α := M)
      ((HSub.hSub (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                  Module.End R M)
                (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
hk :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    (0 : M₂)
this :
  Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M) :
      M₂)
    (0 : M₂)
⊢ Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M) :
      M₂)
    ((f : (a : M) → M₂) 0 : M₂)

Tactic:
rw [← map_zero f] at this

Premises used: map_zero
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
hk :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    (0 : M₂)
this :
  Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M) :
      M₂)
    ((f : (a : M) → M₂) 0 : M₂)
⊢ Eq (α := M)
    ((HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
            k :
          (a : M) → M)
        m :
      M)
    (0 : M)

Tactic:
hf this
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
hk :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    (0 : M₂)
this :
  Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M) :
      M₂)
    ((f : (a : M) → M₂) 0 : M₂)
⊢ Eq (α := M)
    ((HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
            k :
          (a : M) → M)
        m :
      M)
    (0 : M)

Tactic:
exact hf this
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
hk :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    (0 : M₂)
h₁ :
  Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M) :
      M₂)
    (0 : M₂)
⊢ Eq (α := M)
    ((HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
            k :
          (a : M) → M)
        m :
      M)
    (0 : M)

Tactic:
suffices f (((toEnd R L M x - χ x • ↑1) ^ k) m) = 0 by
      rw [← map_zero f] at this; exact hf this
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
h :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
hk :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) m : M₂) :
      M₂)
    (0 : M₂)
⊢ Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HSub.hSub (α := Module.End R M)
                  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M) :
      M₂)
    (0 : M₂)

Tactic:
simpa [hk] using (LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h k) m).symm

Premises used: LinearMap.congr_fun, Module.End.commute_pow_left_of_commute, Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
refine_2 : LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ
⊢ genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)

Tactic:
rw [← LieSubmodule.map_le_iff_le_comap]

Premises used: LieSubmodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ

Tactic:
map_genWeightSpace_le f

Premises used: LieModule.map_genWeightSpace_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ

Tactic:
exact map_genWeightSpace_le f

Premises used: LieModule.map_genWeightSpace_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ LieSubmodule.map f (genWeightSpace M χ) = genWeightSpace M₂ χ ⊓ f.range

Tactic:
le_antisymm (le_inf_iff.mpr ⟨map_genWeightSpace_le f, LieSubmodule.map_le_range f⟩) ?_

Premises used: Iff.mpr, LieModule.map_genWeightSpace_le, le_inf_iff, le_antisymm, And.intro, LieSubmodule.map_le_range
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
refine : genWeightSpace M₂ χ ⊓ f.range ≤ LieSubmodule.map f (genWeightSpace M χ)
⊢ LieSubmodule.map f (genWeightSpace M χ) = genWeightSpace M₂ χ ⊓ f.range

Tactic:
refine le_antisymm (le_inf_iff.mpr ⟨map_genWeightSpace_le f, LieSubmodule.map_le_range f⟩) ?_

Premises used: Iff.mpr, LieModule.map_genWeightSpace_le, le_inf_iff, le_antisymm, And.intro, LieSubmodule.map_le_range
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : 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
inst_7 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm : Membership.mem (α := M₂) (↑(↑(genWeightSpace M₂ χ) : Submodule R M₂) : Set M₂) ((f : (a : M) → M₂) m : M₂)
simp :
  ∃ (m_1 : M),
    Membership.mem (α := M₂) (γ := LieSubmodule R L M₂) (genWeightSpace M₂ χ) ((f : (a : M) → M₂) m_1 : M₂) ∧
      Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) m_1 : M₂) ((f : (a : M) → M₂) m : M₂)
⊢ Membership.mem (α := M₂) (LieSubmodule.map f (genWeightSpace M χ)) ((f : (a : M) → M₂) m : M₂)

Tactic:
simp only [← comap_genWeightSpace_eq_of_injective hf, LieSubmodule.mem_map,
    LieSubmodule.mem_comap]

Premises used: LieSubmodule.mem_comap, LieModule.comap_genWeightSpace_eq_of_injective, LieSubmodule.mem_map