awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI₁ : I = ⊤
hI₂ : IsLieAbelian.{u_2} ↥I
⊢ IsLieAbelian L
have non_abelian_of_isAtom : ∀ (hI₂ : IsLieAbelian.{u_2} ↥⊤), IsLieAbelian L
Tactic: rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂
Cleared hypotheses: hI₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI₁ : I = ⊤
hI₂ : IsLieAbelian.{u_2} ↥I
non_abelian_of_isAtom : ∀ (hI₂ : IsLieAbelian.{u_2} ↥⊤), IsLieAbelian L
⊢ IsLieAbelian L
have non_abelian_of_isAtom₁ : ∀ (hI₂ : IsLieAbelian L), IsLieAbelian L
Tactic: rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂
Cleared hypotheses: hI₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
h : IsLieAbelian L
⊢ Subsingleton L
have h₁ : Eq.{u_2 + 1} (α := LieIdeal R L) ⊥ ⊤
Tactic: rw [isLieAbelian_iff_center_eq_top R L, center_eq_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
⊢ IsLieAbelian.{u_2} ↥(radical R L)
have rw : IsLieAbelian.{u_2} ↥⊥
Tactic: rw [HasTrivialRadical.radical_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
⊢ IsLieAbelian.{u_2} ↥(radical R L) ↔ ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
have mp : IsLieAbelian.{u_2} ↥(radical R L) → ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
mp : IsLieAbelian.{u_2} ↥(radical R L) → ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
⊢ IsLieAbelian.{u_2} ↥(radical R L) ↔ ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
have mpr : (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I) → IsLieAbelian.{u_2} ↥(radical R L)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h₁ : IsLieAbelian.{u_2} ↥(radical R L)
I : LieIdeal R L
h₂ : IsSolvable.{u_2} ↥I
⊢ IsLieAbelian.{u_2} ↥I
have h₃ : I ≤ radical R L
Tactic: rw [LieIdeal.solvable_iff_le_radical] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h : ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
⊢ IsLieAbelian.{u_2} ↥(radical R L)
have mpr : IsSolvable.{u_2} ↥(radical R L)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
m₃ : M₃
⊢ m₃ ∈
      LinearMap.range (M := TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x))
        ((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ TensorProduct.mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x)) →
    Membership.mem (γ := Submodule R M₃) 𝕎(M₃, χ₁ + χ₂, x) m₃
have simp : ∀ (x_1 : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)),
  (g : (a : M₁ ⊗[R] M₂) → M₃)
        ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
              (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
            x_1 :
          M₁ ⊗[R] M₂) =
      m₃ →
    ∃ (k : ℕ),
      Eq (α := M₃)
        ((HSub.hSub (α := Module.End R M₃)
                  (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                    Module.End R M₃)
                  (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
                k :
              (a : M₃) → M₃)
            m₃ :
          M₃)
        (0 : M₃)
Tactic: simp only [TensorProduct.mapIncl, LinearMap.mem_range, LinearMap.coe_comp,
    LieModuleHom.coe_toLinearMap, Function.comp_apply, exists_imp, Module.End.mem_maxGenEigenspace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                    (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                  t :
                M₁ ⊗[R] M₂) :
            M₃) :
        M₃)
      (0 : M₃)
have refine_1 : ∃ (k : ℕ),
  Eq (α := M₃)
    ((HSub.hSub (α := Module.End R M₃)
              (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                Module.End R M₃)
              (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
            k :
          (a : M₃) → M₃)
        ((g : (a : M₁ ⊗[R] M₂) → M₃)
            ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
              0) :
          M₃) :
      M₃)
    (0 : M₃)
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
refine_1 :
  ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                  (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                0) :
            M₃) :
        M₃)
      (0 : M₃)
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                    (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                  t :
                M₁ ⊗[R] M₂) :
            M₃) :
        M₃)
      (0 : M₃)
have refine_2 : ∀ (x_1 : ↥𝕎(M₁, χ₁, x)) (y : ↥𝕎(M₂, χ₂, x)),
  ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                    (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                  (x_1 ⊗ₜ[R] y) :
                M₁ ⊗[R] M₂) :
            M₃) :
        M₃)
      (0 : M₃)
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                  (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                0) :
            M₃) :
        M₃)
      (0 : M₃)
have h : Eq (α := M₃)
  ((HPow.hPow (β := ℕ)
          (HSub.hSub (α := Module.End R M₃)
            (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
              Module.End R M₃)
            (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1))
          0 :
        (a : M₃) → M₃)
      ((g : (a : M₁ ⊗[R] M₂) → M₃)
          ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
              (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
            0) :
        M₃) :
    M₃)
  (0 : M₃)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
hm₁ : Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) m₁
m₂ : M₂
hm₂ : Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) m₂
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                    (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                  (Subtype.mk (p := fun (x_1 : M₁) ↦ Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) x_1) m₁ hm₁ ⊗ₜ[R]
                    Subtype.mk (p := fun (x_1 : M₂) ↦ Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) x_1) m₂ hm₂) :
                M₁ ⊗[R] M₂) :
            M₃) :
        M₃)
      (0 : M₃)
have refine_2 : ∃ (k : ℕ),
  Eq (α := M₃) ((F ^ k : (a : M₃) → M₃) (((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃) : M₃)
    (0 : M₃)
Tactic: change ∃ k, (F ^ k) ((g : M₁ ⊗[R] M₂ →ₗ[R] M₃) (m₁ ⊗ₜ m₂)) = (0 : M₃)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
hm₁ : Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) m₁
m₂ : M₂
hm₂ : Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) m₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor 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₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
⊢ F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
have a : ∀ (m₁ : M₁) (m₂ : M₂),
  Eq.{u_7 + 1} (α := M₃)
    (((((AlgebraTensorModule.curry (F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃)) : M₁ →ₗ[R] M₂ →ₗ[R] M₃) : (a : M₁) → M₂ →ₗ[R] M₃)
              m₁ :
            M₂ →ₗ[R] M₃) :
          (a : M₂) → M₃)
        m₂ :
      M₃)
    (((((AlgebraTensorModule.curry ((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)) : M₁ →ₗ[R] M₂ →ₗ[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₃)
              m₁ :
            M₂ →ₗ[R] M₃) :
          (a : M₂) → M₃)
        m₂ :
      M₃)
Tactic: ext m₁ m₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁_1 : M₁
hm₁ : Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) m₁_1
m₂_1 : M₂
hm₂ : Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) m₂_1
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor 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₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
m₁ : M₁
m₂ : M₂
⊢ Eq.{u_7 + 1} (α := M₃)
    (((((AlgebraTensorModule.curry (F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃)) : M₁ →ₗ[R] M₂ →ₗ[R] M₃) : (a : M₁) → M₂ →ₗ[R] M₃)
              m₁ :
            M₂ →ₗ[R] M₃) :
          (a : M₂) → M₃)
        m₂ :
      M₃)
    (((((AlgebraTensorModule.curry ((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)) : M₁ →ₗ[R] M₂ →ₗ[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₃)
              m₁ :
            M₂ →ₗ[R] M₃) :
          (a : M₂) → M₃)
        m₂ :
      M₃)
have a : HAdd.hAdd (α := M₃) (β := M₃) ((g : (a : M₁ ⊗[R] M₂) → M₃) (⁅x, m₁⁆ ⊗ₜ[R] m₂) : M₃)
      ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] ⁅x, m₂⁆) : M₃) -
    (HSMul.hSMul (β := M₃) χ₁ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃) +
      HSMul.hSMul (β := M₃) χ₂ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃)) =
  HSub.hSub (α := M₃) ((g : (a : M₁ ⊗[R] M₂) → M₃) (⁅x, m₁⁆ ⊗ₜ[R] m₂) : M₃)
      (HSMul.hSMul (β := M₃) χ₁ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃)) +
    HSub.hSub (α := M₃) ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] ⁅x, m₂⁆) : M₃)
      (HSMul.hSMul (β := M₃) χ₂ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃))
Tactic: simp only [f₁, f₂, F, ← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul,
      lie_tmul_right, tmul_smul, toEnd_apply_apply, map_smul, Module.End.one_apply,
      LieModuleHom.coe_toLinearMap, LinearMap.smul_apply, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply,
      LinearMap.lTensor_tmul, AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
      LinearMap.coe_restrictScalars]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
hm₁ : Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) m₁
m₂ : M₂
hm₂ : Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) m₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor 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₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((F ^ k : (a : M₃) → M₃) (((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃) : M₃) (0 : M₃)
have h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
Tactic: have h_comm_square : F ∘ₗ ↑g = (g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (f₁ + f₂) := by
    ext m₁ m₂
    simp only [f₁, f₂, F, ← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul,
      lie_tmul_right, tmul_smul, toEnd_apply_apply, map_smul, Module.End.one_apply,
      LieModuleHom.coe_toLinearMap, LinearMap.smul_apply, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply,
      LinearMap.lTensor_tmul, AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
      LinearMap.coe_restrictScalars]
    abel
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
hm₁ : Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) m₁
m₂ : M₂
hm₂ : Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) m₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor 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₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((F ^ k : (a : M₃) → M₃) (((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃) : M₃) (0 : M₃)
have refine_2 : ∀ (k : ℕ)
  (hk :
    Eq (α := M₁ ⊗[R] M₂) (((f₁ + f₂) ^ k : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)),
  ∃ (k : ℕ),
    Eq (α := M₃)
      ((F ^ k : (a : M₃) → M₃) (((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃) : M₃) (0 : M₃)
Tactic: rsuffices ⟨k, hk⟩ : ∃ k : ℕ, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ m₂) = 0