awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (hypothesis)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
have this : Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K)))
  ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
          n :
        (a : M) → M)
      m₂ :
    M)
Tactic: have := toEnd_pow_apply_mem hx hm₂ n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
this :
  Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K)))
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
have h : ∀
  (this :
    Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) ⊥
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)),
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
Tactic: rwa [hn, LieSubmodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
this :
  Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K)))
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
h :
  ∀
    (this :
      Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) ⊥
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            m₂ :
          M)),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
have h₁ : ∀
  (this :
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)),
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
Tactic: rwa [hn, LieSubmodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
hm₁' :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₁ :
        M)
      (0 : M)
hm₂' :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)
have add : ∀ (n₁ : ℕ)
  (hn₁ :
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n₁ :
            (a : M) → M)
          m₁ :
        M)
      (0 : M)),
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)
Tactic: obtain ⟨n₁, hn₁⟩ := hm₁'
Cleared hypotheses: hm₁'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
hm₂' :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)
have add : ∀ (n₂ : ℕ)
  (hn₂ :
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n₂ :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)),
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)
Tactic: obtain ⟨n₂, hn₂⟩ := hm₂'
Cleared hypotheses: hm₂'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)
have add : Eq (α := M)
  ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
          (max n₁ n₂) :
        (a : M) → M)
      (m₁ + m₂) :
    M)
  (0 : M)
Tactic: refine ⟨max n₁ n₂, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        (m₁ + m₂) :
      M)
    (0 : M)
have add : HAdd.hAdd (α := M) (β := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        m₁ :
      M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        m₂ :
      M) =
  0
Tactic: rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
add :
  HAdd.hAdd (α := M) (β := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₁ :
        M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        (m₁ + m₂) :
      M)
    (0 : M)
have add₁ : HAdd.hAdd (α := M) (β := M) (0 : M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        m₂ :
      M) =
  0
Tactic: rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
add :
  HAdd.hAdd (α := M) (β := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₁ :
        M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
add₁ :
  HAdd.hAdd (α := M) (β := M) (0 : M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        (m₁ + m₂) :
      M)
    (0 : M)
have add₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
add :
  HAdd.hAdd (α := M) (β := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₁ :
        M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
add₁ :
  HAdd.hAdd (α := M) (β := M) (0 : M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
add₂ : HAdd.hAdd (α := M) 0 0 = 0
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        (m₁ + m₂) :
      M)
    (0 : M)
have add₃ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
hm :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (χ : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑χ : (a : ↥H) → K)) m
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
have zero : ∃ (n : ℕ),
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        0 :
      M)
    (0 : M)
Tactic: induction hm using LieSubmodule.iSup_induction' with
  | zero => exact ⟨0, map_zero _⟩
  | mem χ₂ m₂ hm₂ =>
    obtain ⟨n, -, hn⟩ := exists_genWeightSpace_smul_add_eq_bot M χ χ₂ hχ
    use n
    have := toEnd_pow_apply_mem hx hm₂ n
    rwa [hn, LieSubmodule.mem_bot] at this
  | add m₁ m₂ hm₁ hm₂ hm₁' hm₂' =>
    obtain ⟨n₁, hn₁⟩ := hm₁'
    obtain ⟨n₂, hn₂⟩ := hm₂'
    refine ⟨max n₁ n₂, ?_⟩
    rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
hm :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (χ : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑χ : (a : ↥H) → K)) m
zero :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          0 :
        M)
      (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
have mem : ∀ (χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M) (m₂ : M)
  (hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂),
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
Tactic: induction hm using LieSubmodule.iSup_induction' with
  | zero => exact ⟨0, map_zero _⟩
  | mem χ₂ m₂ hm₂ =>
    obtain ⟨n, -, hn⟩ := exists_genWeightSpace_smul_add_eq_bot M χ χ₂ hχ
    use n
    have := toEnd_pow_apply_mem hx hm₂ n
    rwa [hn, LieSubmodule.mem_bot] at this
  | add m₁ m₂ hm₁ hm₂ hm₁' hm₂' =>
    obtain ⟨n₁, hn₁⟩ := hm₁'
    obtain ⟨n₂, hn₂⟩ := hm₂'
    refine ⟨max n₁ n₂, ?_⟩
    rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]
Cleared hypotheses: hm