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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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) x :
              Module.End R M)
            m).range =
      (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) x : Module.End R M)
          b).range
x_1 : HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)
m : M
h :
  let F : LieSubmodule R L M := posFittingComp R L M;
  ∀ (x_2 : M ⧸ F),
    Eq (α := M ⧸ F)
      ((HPow.hPow (α := Module.End R (M ⧸ F))
              ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k :
            (a : M ⧸ F) → M ⧸ F)
          (Quot.mk (⇑(↑F : Submodule R M).quotientRel : M → M → Prop) m) :
        M ⧸ F)
      ((0 : (a : M ⧸ F) → M ⧸ F) (Quot.mk (⇑(↑F : Submodule R M).quotientRel : M → M → Prop) m) : M ⧸ F)
⊢ Eq (α := HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
    ((HPow.hPow (α := Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
            ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
                  (a : L) → Module.End R (M ⧸ posFittingComp R L M))
                x :
              Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
            k :
          (a : M ⧸ posFittingComp R L M) → M ⧸ posFittingComp R L M)
        (Quot.mk (⇑(↑(posFittingComp R L M) : Submodule R M).quotientRel : M → M → Prop) m) :
      HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
    ((0 : (a : M ⧸ posFittingComp R L M) → M ⧸ posFittingComp R L M)
        (Quot.mk (⇑(↑(posFittingComp R L M) : Submodule R M).quotientRel : M → M → Prop) m) :
      HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))

Tactic:
set F := posFittingComp R L M

Premises used: LieModule.posFittingComp
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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) x :
              Module.End R M)
            m).range =
      (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) x : Module.End R M)
          b).range
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
a :
  Membership.mem (α := M) (γ := LieSubmodule R L M) (posFittingCompOf R M x)
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) F
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)

Tactic:
apply posFittingCompOf_le_posFittingComp R L M x

Premises used: LieModule.posFittingCompOf_le_posFittingComp
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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) x :
              Module.End R M)
            m).range =
      (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) x : Module.End R M)
          b).range
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
a :
  Membership.mem (α := 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) x : Module.End R M)
        k).range
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule R L M) (posFittingCompOf R M x)
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)

Tactic:
simp_rw [← LieSubmodule.mem_toSubmodule, posFittingCompOf, hk k (le_refl k)]

Premises used: le_refl, LieSubmodule.mem_toSubmodule, LieModule.posFittingCompOf
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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) x :
              Module.End R M)
            m).range =
      (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) x : Module.End R M)
          b).range
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
⊢ Membership.mem (α := 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) x : Module.End R M)
        k).range
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)

Tactic:
apply LinearMap.mem_range_self

Premises used: LinearMap.mem_range_self
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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) x :
              Module.End R M)
            m).range =
      (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) x : Module.End R M)
          b).range
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
⊢ Membership.mem (α := M) F
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)

Tactic:
replace hk : (toEnd R L M x ^ k) m ∈ F := by
    apply posFittingCompOf_le_posFittingComp R L M x
    simp_rw [← LieSubmodule.mem_toSubmodule, posFittingCompOf, hk k (le_refl k)]
    apply LinearMap.mem_range_self
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
hk :
  Membership.mem (α := M) F
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)
this :
  Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
            ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k :
          (a : M ⧸ F) → M ⧸ F)
        (LieSubmodule.Quotient.mk m) :
      M ⧸ F)
    (LieSubmodule.Quotient.mk
        ((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) x :
                Module.End R M)
              k :
            (a : M) → M)
          m) :
      M ⧸ F)
⊢ Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
            ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k :
          (a : M ⧸ F) → M ⧸ F)
        (Quot.mk (⇑(↑F : Submodule R M).quotientRel : M → M → Prop) m) :
      M ⧸ F)
    ((0 : (a : M ⧸ F) → M ⧸ F) (Quot.mk (⇑(↑F : Submodule R M).quotientRel : M → M → Prop) m) : M ⧸ F)

Tactic:
simpa [Submodule.Quotient.quot_mk_eq_mk, this]

Premises used: Submodule.Quotient.quot_mk_eq_mk
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
hk :
  Membership.mem (α := M) F
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)
h :
  Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
            ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k :
          (a : M ⧸ F) → M ⧸ F)
        (LieSubmodule.Quotient.mk m) :
      M ⧸ F)
    (LieSubmodule.Quotient.mk
        ((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) x :
                Module.End R M)
              k :
            (a : M) → M)
          m) :
      M ⧸ F)
⊢ Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
            ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k :
          (a : M ⧸ F) → M ⧸ F)
        (Quot.mk (⇑(↑F : Submodule R M).quotientRel : M → M → Prop) m) :
      M ⧸ F)
    ((0 : (a : M ⧸ F) → M ⧸ F) (Quot.mk (⇑(↑F : Submodule R M).quotientRel : M → M → Prop) m) : M ⧸ F)

Tactic:
suffices (toEnd R L (M ⧸ F) x ^ k) (LieSubmodule.Quotient.mk (N := F) m) =
    LieSubmodule.Quotient.mk (N := F) ((toEnd R L M x ^ k) m)
      by simpa [Submodule.Quotient.quot_mk_eq_mk, 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
hk :
  Membership.mem (α := M) F
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)
⊢ Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
              ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k ∘ₗ
            (↑(LieSubmodule.Quotient.mk' F) : M →ₗ[R] M ⧸ F) :
          (a : M) → M ⧸ F)
        m :
      M ⧸ F)
    (((↑(LieSubmodule.Quotient.mk' F) : M →ₗ[R] M ⧸ F) ∘ₗ
            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) x :
                Module.End R M)
              k :
          (a : M) → M ⧸ F)
        m :
      M ⧸ F)

Tactic:
have := LinearMap.congr_fun (Module.End.commute_pow_left_of_commute
    (LieSubmodule.Quotient.toEnd_comp_mk' F x) k) m
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x_1 : M ⧸ F
hk :
  Membership.mem (α := M) F
    ((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) x :
              Module.End R M)
            k :
          (a : M) → M)
        m :
      M)
this :
  Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
              ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k ∘ₗ
            (↑(LieSubmodule.Quotient.mk' F) : M →ₗ[R] M ⧸ F) :
          (a : M) → M ⧸ F)
        m :
      M ⧸ F)
    (((↑(LieSubmodule.Quotient.mk' F) : M →ₗ[R] M ⧸ F) ∘ₗ
            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) x :
                Module.End R M)
              k :
          (a : M) → M ⧸ F)
        m :
      M ⧸ F)
⊢ Eq (α := M ⧸ F)
    ((HPow.hPow (α := Module.End R (M ⧸ F))
            ((toEnd R L (M ⧸ F) : (a : L) → Module.End R (M ⧸ F)) x : Module.End R (M ⧸ F)) k :
          (a : M ⧸ F) → M ⧸ F)
        (LieSubmodule.Quotient.mk m) :
      M ⧸ F)
    (LieSubmodule.Quotient.mk
        ((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) x :
                Module.End R M)
              k :
            (a : M) → M)
          m) :
      M ⧸ F)

Tactic:
simpa using 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
inst_8 : IsNilpotent L M
⊢ Eq (α := LieSubmodule R L M) (posFittingComp R L M) ⊥

Tactic:
simp [posFittingComp]

Premises used: LieModule.posFittingComp
-- 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₂
rw :
  LE.le.{u_5} (α := LieSubmodule R L M₂) (⨆ (i : L), LieSubmodule.map f (posFittingCompOf R M i))
    (⨆ (x : L), posFittingCompOf R M₂ x)
⊢ LieSubmodule.map f (posFittingComp R L M) ≤ posFittingComp R L M₂

Tactic:
rw [posFittingComp, posFittingComp, LieSubmodule.map_iSup]

Premises used: LieSubmodule.map_iSup, LieModule.posFittingComp
-- 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₂
⊢ LE.le.{u_5} (α := LieSubmodule R L M₂) (⨆ (i : L), LieSubmodule.map f (posFittingCompOf R M i))
    (⨆ (x : L), posFittingCompOf R M₂ x)

Tactic:
iSup_mono fun y ↦ LieSubmodule.map_le_iff_le_comap.mpr fun m hm ↦ ?_

Premises used: Iff.mpr, Set.Mem, LieSubmodule.map_le_iff_le_comap, iSup_mono
-- 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₂
refine :
  ∀ (y : L) (m : M) (hm : Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M y) m),
    m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)
⊢ LE.le.{u_5} (α := LieSubmodule R L M₂) (⨆ (i : L), LieSubmodule.map f (posFittingCompOf R M i))
    (⨆ (x : L), posFittingCompOf R M₂ x)

Tactic:
refine iSup_mono fun y ↦ LieSubmodule.map_le_iff_le_comap.mpr fun m hm ↦ ?_

Premises used: Iff.mpr, LieSubmodule.map_le_iff_le_comap, iSup_mono
-- 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 : Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M y) m
⊢ ∀ (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

Tactic:
simp only [mem_posFittingCompOf] at hm

Premises used: LieModule.mem_posFittingCompOf
-- 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
simp :
  ∀ (k : ℕ),
    ∃ (n : 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₂)
            n :
          M₂)
        ((f : (a : M) → M₂) m : M₂)
⊢ m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)

Tactic:
simp only [LieSubmodule.mem_comap, mem_posFittingCompOf]

Premises used: LieSubmodule.mem_comap, LieModule.mem_posFittingCompOf
-- 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 : ℕ
obtain :
  ∀ (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),
    ∃ (n : 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₂)
            n :
          M₂)
        ((f : (a : M) → M₂) m : M₂)
⊢ ∃ (n : 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₂)
          n :
        M₂)
      ((f : (a : M) → M₂) m : M₂)

Tactic:
obtain ⟨n, hn⟩ := hm 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₂
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 (α := 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₂)
⊢ ∃ (n : 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₂)
          n :
        M₂)
      ((f : (a : M) → M₂) m : M₂)

Tactic:
use f n

Premises used: DFunLike.coe