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 : IsDomain R
inst_9 : Module.IsTorsionFree R M
x : L
⊢ iSupIndep.{u_2 + 1, u_4} (α := LieSubmodule R L M) fun (χ : R) ↦ genWeightSpaceOf M χ x
have rw : iSupIndep.{u_2 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i x) : Submodule R M)
Tactic: rw [← LieSubmodule.iSupIndep_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
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 : IsDomain R
inst_9 : Module.IsTorsionFree R M
inst_10 : IsNoetherian R M
⊢ Finite (Weight R L M)
have this : Finite (↑{χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} : Type (max u_2 u_3))
Tactic: have : Finite {χ : L → R | genWeightSpace M χ ≠ ⊥} := finite_genWeightSpace_ne_bot 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
this :
  ∃ (φ : R),
    Ne.{u_4 + 1} (α := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
      ⊥
⊢ ∃ (φ : R),
    Module.End.HasEigenvalue.{u_2, u_4} (M := 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) φ
have obtain : ∀ (φ : R)
  (hφ :
    Ne.{u_4 + 1} (α := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
      ⊥),
  ∃ (φ : R),
    Module.End.HasEigenvalue.{u_2, u_4} (M := 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) φ
Tactic: obtain ⟨φ, hφ⟩ := 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
⊢ ∃ (φ : R),
    Module.End.HasEigenvalue.{u_2, u_4} (M := 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) φ
have suffices : ∃ (φ : R),
  Ne.{u_4 + 1} (α := Submodule R M)
    (Module.End.maxGenEigenspace
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
    ⊥
Tactic: suffices ∃ φ, (toEnd R L M x).maxGenEigenspace φ ≠ ⊥ by
    obtain ⟨φ, hφ⟩ := this
    exact ⟨φ, (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one ENat.top_pos).mp hφ⟩
-- 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
⊢ ∃ (φ : R),
    Ne.{u_4 + 1} (α := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
      ⊥
have this : Eq.{u_4 + 1} (α := Submodule R M)
  (⨆ (φ : R),
    Module.End.maxGenEigenspace
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
  ⊤
Tactic: have := maxGenEigenspace_eq_top (R := R) (L := L) (M := 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
this :
  Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
    ⊤
⊢ ∃ (φ : R),
    Ne.{u_4 + 1} (α := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
      ⊥
have contrapose! : ∀
  (this :
    ∀ (φ : R),
      Eq.{u_4 + 1} (α := Submodule R M)
        (Module.End.maxGenEigenspace
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
        ⊥),
  Ne.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) φ)
    ⊤
Tactic: contrapose! 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
inst_8 : IsTriangularizable R L M
x : L
⊢ Eq.{u_4 + 1} (α := LieSubmodule R L M) (⨆ (φ : R), genWeightSpaceOf M φ x) ⊤
have rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : R), (↑(genWeightSpaceOf M i x) : Submodule R M)) ⊤
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule,
    LieSubmodule.top_toSubmodule]
-- 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 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
this :
  _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id))
⊢ (trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
have this₁ : Eq.{u_2 + 1} (α := R)
  ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (HSub.hSub (α := End R ↥(genWeightSpace M χ))
        (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
              (a : L) → End R ↥(genWeightSpace M χ))
            x :
          End R ↥(genWeightSpace M χ))
        (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id)) :
    R)
  (0 : R)
Tactic: replace this := (isNilpotent_trace_of_isNilpotent this).eq_zero
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
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
this :
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (HSub.hSub (α := End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              x :
            End R ↥(genWeightSpace M χ))
          (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id)) :
      R)
    (0 : R)
⊢ (trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
have rwa : ∀
  (this :
    HSub.hSub (α := R) (β := R)
        ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                    LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                  (a : L) → End R ↥(genWeightSpace M χ))
                x :
              End R ↥(genWeightSpace M χ)) :
          R)
        ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
            (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id) :
          R) =
      0),
  (trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
Tactic: rwa [map_sub, map_smul, trace_id, sub_eq_zero, smul_eq_mul, mul_comm,
      ← nsmul_eq_mul] 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
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
⊢ (trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
have suffices : _root_.IsNilpotent
  (HSub.hSub (α := End R ↥(genWeightSpace M χ))
    (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
          (a : L) → End R ↥(genWeightSpace M χ))
        x :
      End R ↥(genWeightSpace M χ))
    (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id))
Tactic: suffices _root_.IsNilpotent ((toEnd R L (genWeightSpace M χ) x) - χ x • LinearMap.id) by
    replace this := (isNilpotent_trace_of_isNilpotent this).eq_zero
    rwa [map_sub, map_smul, trace_id, sub_eq_zero, smul_eq_mul, mul_comm,
      ← nsmul_eq_mul] at 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
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
⊢ _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id))
have rw : _root_.IsNilpotent
  (HSub.hSub (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
    (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
          (a : L) → End R ↥(genWeightSpace M χ))
        x :
      End R ↥(genWeightSpace M χ))
    ((algebraMap R (End R ↥(genWeightSpace M χ)) : (a : R) → End R ↥(genWeightSpace M χ)) (χ x) :
      End R ↥(genWeightSpace M χ)))
Tactic: rw [← Module.algebraMap_end_eq_smul_id]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
⊢ IsTriangularizable.{u_1, u_3, u_4} K L ↥N
have refine : ∀ (y : L),
  Eq.{u_4 + 1} (α := Submodule K ↥N)
    (⨆ (φ : K),
      End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
        (((toEnd.{u_1, u_3, u_4} K L ↥N : LieHom.{u_1, u_3, u_4} K L (End K ↥N)) : (a : L) → End K ↥N) y) φ)
    ⊤
Tactic: refine ⟨fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
y : L
⊢ Eq.{u_4 + 1} (α := Submodule K ↥N)
    (⨆ (φ : K),
      End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
        (((toEnd.{u_1, u_3, u_4} K L ↥N : LieHom.{u_1, u_3, u_4} K L (End K ↥N)) : (a : L) → End K ↥N) y) φ)
    ⊤
have rw : Eq.{u_4 + 1} (α := Submodule K ↥N)
  (⨆ (φ : K),
    End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
      (LinearMap.restrict (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) sorry) φ)
  ⊤
Tactic: rw [← N.toEnd_restrict_eq_toEnd y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : L → K), genWeightSpace M χ) ⊤
have simp : Eq.{u_4 + 1} (α := Submodule K M) (⨆ (i : L → K), ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule K M)) ⊤
Tactic: simp only [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule,
    LieSubmodule.iInf_toSubmodule, LieSubmodule.top_toSubmodule, genWeightSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (i : L → K), ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule K M)) ⊤
have refine : ∀ (i : L),
  Eq.{u_4 + 1} (α := Submodule K M)
    (⨆ (μ : K), End.maxGenEigenspace (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) i) μ) ⊤
Tactic: refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : Weight K L M), genWeightSpace M (⇑χ : (a : L) → K)) ⊤
have this : Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : L → K), genWeightSpace M χ) ⊤
Tactic: have := iSup_genWeightSpace_eq_top K L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
this : Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : L → K), genWeightSpace M χ) ⊤
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : Weight K L M), genWeightSpace M (⇑χ : (a : L) → K)) ⊤
have this₁ : Eq.{u_4 + 1} (α := LieSubmodule K L M)
  (⨆ (x : Weight K L M),
    genWeightSpace M
      (↑((Weight.equivSetOf K L M : (a : Weight K L M) → (↑{χ : L → K | genWeightSpace M χ ≠ ⊥} : Type (max u_1 u_3)))
            x) :
        L → K))
  ⊤
Tactic: erw [← iSup_ne_bot_subtype, ← (Weight.equivSetOf K L M).iSup_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ N = ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
have refine : N ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
Tactic: refine le_antisymm ?_ (iSup_le fun χ ↦ inf_le_left)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
| N
have rw : ⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K))
Tactic: rw [← N.map_incl_top, ← iSup_genWeightSpace_eq_top' K L N, LieSubmodule.map_iSup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ N ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
have conv_lhs : LE.le.{u_4} (α := LieSubmodule K L M)
  (⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K)))
  (⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K))
Tactic: conv_lhs => rw [← N.map_incl_top, ← iSup_genWeightSpace_eq_top' K L N, LieSubmodule.map_iSup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ LE.le.{u_4} (α := LieSubmodule K L M)
    (⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K)))
    (⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K))
have refine : ∀ (χ_N : Weight.{u_1, u_3, u_4} K L ↥N),
  LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤
    ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
Tactic: refine iSup_le fun χ_N ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
⊢ LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤
    ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
have hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
Tactic: have hN := (LieSubmodule.map_mono (le_top : genWeightSpace N χ_N ≤ ⊤)).trans N.map_incl_top.le
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
⊢ N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
have pos : ∀ (h : Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥),
  N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
Tactic: by_cases h : genWeightSpace M (χ_N : L → K) = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
pos :
  ∀ (h : Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥),
    N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
⊢ N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
have neg : ∀ (h : ¬Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥),
  N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
Tactic: by_cases h : genWeightSpace M (χ_N : L → K) = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
x : L
hx : x ∈ corootSubmodule α
⊢ x ∈ LieSubmodule.restr I H
have obtain : ∀ (a : ↥H.toLieSubmodule)
  (ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a)
  (hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)),
  Membership.mem (α := L) (LieSubmodule.restr I H) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
Tactic: obtain ⟨a, ha, rfl⟩ := (LieSubmodule.mem_map _).mp hx
Cleared hypotheses: x, hx