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₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm :
  ∀ (k : ℕ),
    ∃ (n : M),
      (HPow.hPow (α := 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) y :
                Module.End R M)
              k :
            (a : M) → M)
          n =
        m
k : ℕ
n : M
hn :
  (HPow.hPow (α := 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) y : Module.End R M)
          k :
        (a : M) → M)
      n =
    m
h :
  Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HPow.hPow (α := 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) y :
                  Module.End R M)
                k :
              (a : M) → M)
            n :
          M) :
      M₂)
    ((f : (a : M) → M₂) m : M₂)
h₁ h₂ : Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) ((f : (a : M) → M₂) m : M₂)
⊢ Eq (α := M₂)
    ((HPow.hPow (α := 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₂) y :
              Module.End R M₂)
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) n : M₂) :
      M₂)
    ((f : (a : M) → M₂) m : M₂)

Tactic:
rw [LieModule.toEnd_pow_apply_map, hn]

Premises used: LieModule.toEnd_pow_apply_map
-- 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₂
rw : genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)
⊢ LieSubmodule.map f (genWeightSpace M χ) ≤ 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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
simp :
  ∀ (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₂)
⊢ m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)

Tactic:
simp only [LieSubmodule.mem_comap, mem_genWeightSpace]

Premises used: LieSubmodule.mem_comap, LieModule.mem_genWeightSpace
-- 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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
h :
  ∀ (x_1 : M),
    Eq.{u_5 + 1} (α := 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) ∘ₗ
              (↑f : M →ₗ[R] M₂) :
            (a : M) → M₂)
          x_1 :
        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) :
            (a : M) → M₂)
          x_1 :
        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) ∘ₗ
      (↑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:
ext
-- 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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
x_1 : M
⊢ Eq.{u_5 + 1} (α := 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) ∘ₗ
            (↑f : M →ₗ[R] M₂) :
          (a : M) → M₂)
        x_1 :
      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) :
          (a : M) → M₂)
        x_1 :
      M₂)

Tactic:
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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) 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 : (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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
this :
  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)
obtain :
  ∀ (k : ℕ)
    (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_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_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₂)

Tactic:
obtain ⟨k, h⟩ := (mem_genWeightSpace _ _ _).mp hm x

Premises used: LieModule.mem_genWeightSpace, Iff.mp
-- 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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
this :
  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 : ℕ
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_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₂)

Tactic:
⟨k, ?_⟩

Premises used: Exists.intro
-- 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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
this :
  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 : ℕ
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)
refine :
  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_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₂)

Tactic:
refine ⟨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₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
this :
  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 : ℕ
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)
⊢ 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₂)

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

Premises used: LinearMap.congr_fun, Module.End.commute_pow_left_of_commute
-- 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.comap f (genWeightSpace M₂ χ) = genWeightSpace M χ

Tactic:
le_antisymm (fun m hm ↦ ?_) ?_

Premises used: le_antisymm
-- 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_1 :
  ∀ (m : M) (hm : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)),
    Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
refine_2 : genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)
⊢ LieSubmodule.comap f (genWeightSpace M₂ χ) = genWeightSpace M χ

Tactic:
refine le_antisymm (fun m hm ↦ ?_) ?_

Premises used: le_antisymm
-- 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 : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)
⊢ ∀ (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₂)

Tactic:
simp only [LieSubmodule.mem_comap, mem_genWeightSpace] at hm

Premises used: LieSubmodule.mem_comap, LieModule.mem_genWeightSpace
-- 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₂)
refine_1 :
  ∀ (x : L),
    ∃ (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)
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m

Tactic:
simp only [mem_genWeightSpace]

Premises used: LieModule.mem_genWeightSpace
-- 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 :
  ∀ (x_1 : M),
    Eq.{u_5 + 1} (α := 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) ∘ₗ
              (↑f : M →ₗ[R] M₂) :
            (a : M) → M₂)
          x_1 :
        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) :
            (a : M) → M₂)
          x_1 :
        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) ∘ₗ
      (↑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:
ext
-- 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
x_1 : M
⊢ Eq.{u_5 + 1} (α := 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) ∘ₗ
            (↑f : M →ₗ[R] M₂) :
          (a : M) → M₂)
        x_1 :
      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) :
          (a : M) → M₂)
        x_1 :
      M₂)

Tactic:
simp