awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
χ : 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
⊢ ∃ (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)
have 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)
Tactic: have h : (toEnd R L M₂ x - χ x • ↑1) ∘ₗ f =
             f ∘ₗ (toEnd R L M x - χ x • ↑1) := by ext; simp
-- 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₂
χ : 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 : ℕ),
    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)
have 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)
Tactic: obtain ⟨k, hk⟩ := hm 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
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₂)
⊢ ∃ (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)
have 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)
Tactic: use 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
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 (α := 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)
have 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₂)
Tactic: rw [← map_zero f] at this
Cleared hypotheses: this
-- 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₂
χ : 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 (α := 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)
have 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₂)
Tactic: suffices f (((toEnd R L M x - χ x • ↑1) ^ k) m) = 0 by
      rw [← map_zero f] at this; exact hf this
-- 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₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)
have refine_2 : LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ
Tactic: rw [← LieSubmodule.map_le_iff_le_comap]
-- 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₂
χ : 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
have refine : genWeightSpace M₂ χ ⊓ f.range ≤ LieSubmodule.map f (genWeightSpace M χ)
Tactic: refine le_antisymm (le_inf_iff.mpr ⟨map_genWeightSpace_le f, LieSubmodule.map_le_range f⟩) ?_
-- 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₂
χ : 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₂)
⊢ Membership.mem (α := M₂) (LieSubmodule.map f (genWeightSpace M χ)) ((f : (a : M) → M₂) m : M₂)
have 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₂)
Tactic: simp only [← comap_genWeightSpace_eq_of_injective hf, LieSubmodule.mem_map,
    LieSubmodule.mem_comap]
-- 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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M) = posFittingComp R L M₂
have refine : posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
Tactic: refine le_antisymm (map_posFittingComp_le _) ?_
-- 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₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
have rw : LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
  LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
Tactic: rw [this]
-- 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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
have suffices : posFittingComp R L M₂ =
  LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
Tactic: suffices posFittingComp R L M₂ = ((posFittingComp R L M₂).map (e.symm : M₂ →ₗ⁅R,L⁆ M)).map e by
    rw [this]
    exact LieSubmodule.map_mono (map_posFittingComp_le _)
-- 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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
have rw : posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)
Tactic: rw [← LieSubmodule.map_comp]
-- 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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)
have h : posFittingComp R L M₂ =
  LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))
Tactic: convert! LieSubmodule.map_id
-- 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₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ posFittingComp R L M₂ =
    LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))
have h : ∀ (m : M₂),
  Membership.mem (γ := LieSubmodule R L M₂) (posFittingComp R L M₂) m ↔
    m ∈ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))
Tactic: ext
-- 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
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have obtain : ∀ (l : ℕ)
  (hl :
    ∀ b ≥ l,
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
          (lowerCentralSeries R L (↥N₁) b) ∧
        Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
            (lowerCentralSeries R L (↥N₂) b) ∧
          Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)),
  LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
Tactic: obtain ⟨l, hl⟩ := Filter.eventually_atTop.mp <|
    (eventually_iInf_lowerCentralSeries_eq R L N₁).and <|
    (eventually_iInf_lowerCentralSeries_eq R L N₂).and
    (eventually_iInf_lowerCentralSeries_eq R L M)
-- 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
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have hl₁ : Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
Tactic: obtain ⟨hl₁, hl₂, hl₃⟩ := hl l (le_refl _)
-- 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
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have hl₂ : Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
Tactic: obtain ⟨hl₁, hl₂, hl₃⟩ := hl l (le_refl _)