awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
x : L
⊢ Eq (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
have simp_rw : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
Tactic: simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
    posFittingCompOf_le_lowerCentralSeries, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
x : L
simp_rw : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
⊢ Eq (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
have simp_rw₁ : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (⨅ (k : ℕ), lowerCentralSeries R L M k)
Tactic: simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
    posFittingCompOf_le_lowerCentralSeries, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
x : L
simp_rw : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
simp_rw₁ : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (⨅ (k : ℕ), lowerCentralSeries R L M k)
⊢ Eq (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
have simp_rw₂ : ∀ (i : ℕ), LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (lowerCentralSeries R L M i)
Tactic: simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
    posFittingCompOf_le_lowerCentralSeries, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
x : L
simp_rw : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
simp_rw₁ : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (⨅ (k : ℕ), lowerCentralSeries R L M k)
simp_rw₂ : ∀ (i : ℕ), LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (lowerCentralSeries R L M i)
⊢ Eq (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
have simp_rw₃ : ∀ (i : ℕ), True
Tactic: simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
    posFittingCompOf_le_lowerCentralSeries, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)
have refine : LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)
Tactic: refine le_antisymm ?_ (posFittingComp_le_iInf_lowerCentralSeries R L M)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)
have h : IsNilpotent.{u_3, u_4} L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
Tactic: apply iInf_lcs_le_of_isNilpotent_quot
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ IsNilpotent.{u_3, u_4} L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
have h : ∀ (x : L),
  _root_.IsNilpotent.{u_4} (R := 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)))
Tactic: rw [LieModule.isNilpotent_iff_forall' (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ _root_.IsNilpotent.{u_4} (R := 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)))
have h : ∀ (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),
  _root_.IsNilpotent.{u_4} (R := 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)))
Tactic: obtain ⟨k, hk⟩ := Filter.eventually_atTop.mp (toEnd R L M x).eventually_iInf_range_pow_eq
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ _root_.IsNilpotent.{u_4} (R := 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)))
have h : 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 =
  0
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ 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 =
    0
have h : ∀ (x_1 : HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) (m : M),
  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: ext ⟨m⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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
⊢ 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))
have 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)
Tactic: set F := posFittingComp R L M
Cleared hypotheses: x_1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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)
have 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)
Tactic: apply posFittingCompOf_le_posFittingComp R L M x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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) (γ := 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)
have 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)
Tactic: simp_rw [← LieSubmodule.mem_toSubmodule, posFittingCompOf, hk k (le_refl k)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
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
⊢ 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)
have 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)
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
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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 :
          (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
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 :
          (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)
have 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)
Tactic: have := LinearMap.congr_fun (Module.End.commute_pow_left_of_commute
    (LieSubmodule.Quotient.toEnd_comp_mk' F x) k) m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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₂
⊢ LieSubmodule.map f (posFittingComp R L M) ≤ posFittingComp R L M₂
have rw : LE.le.{u_5} (α := LieSubmodule R L M₂) (⨆ (i : L), LieSubmodule.map f (posFittingCompOf R M i))
  (⨆ (x : L), posFittingCompOf R M₂ x)
Tactic: rw [posFittingComp, posFittingComp, LieSubmodule.map_iSup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
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)
have 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)
Tactic: refine iSup_mono fun y ↦ LieSubmodule.map_le_iff_le_comap.mpr fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
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
⊢ m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)
have 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
Tactic: simp only [mem_posFittingCompOf] at hm
Cleared hypotheses: hm