awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
ind :
  ∀ (N' : LieSubmodule R L ↥N) (hN' : N' < ⊤),
    IsCompl.{u_4} (α := LieSubmodule R L ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
⊢ P N

Tactic:
refine isCompl_genWeightSpace_zero_posFittingComp_aux R L N fun N' hN' ↦ ?_

Premises used: Membership.mem, Subtype, _private.0.LieModule.isCompl_genWeightSpace_zero_posFittingComp_aux
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
this :
  IsCompl.{u_4} (α := LieSubmodule R L ↥(LieSubmodule.map N.incl N')) (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0)
    (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
⊢ IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥N') 0))
    (LieSubmodule.map e.toLieModuleHom (posFittingComp R L ↥N'))

Tactic:
rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e] at this

Premises used: LieModule.map_genWeightSpace_eq, LieModule.map_posFittingComp_eq
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
this :
  IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥N') 0))
    (LieSubmodule.map e.toLieModuleHom (posFittingComp R L ↥N'))
⊢ IsCompl.{u_4} (α := LieSubmodule R L ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
(LieSubmodule.orderIsoMapComap e).isCompl_iff.mpr this

Premises used: Iff.mpr, LieSubmodule.orderIsoMapComap, OrderIso.isCompl_iff
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
this :
  IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥N') 0))
    (LieSubmodule.map e.toLieModuleHom (posFittingComp R L ↥N'))
⊢ IsCompl.{u_4} (α := LieSubmodule R L ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mpr this

Premises used: Iff.mpr, LieSubmodule.orderIsoMapComap, OrderIso.isCompl_iff
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
ind :
  IsCompl.{u_4} (α := LieSubmodule R L ↥(LieSubmodule.map N.incl N')) (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0)
    (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
⊢ IsCompl.{u_4} (α := LieSubmodule R L ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
suffices IsCompl (genWeightSpace (N'.map N.incl) 0) (posFittingComp R L (N'.map N.incl)) by
    let e := LieSubmodule.equivMapOfInjective N' N.injective_incl
    rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e] at this
    exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mpr this
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
⊢ IsCompl.{u_4} (α := LieSubmodule R L ↥(LieSubmodule.map N.incl N')) (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0)
    (posFittingComp R L ↥(LieSubmodule.map N.incl N'))

Tactic:
hN _ (LieSubmodule.map_incl_lt_iff_lt_top.mpr hN')

Premises used: Iff.mpr, LieSubmodule.map_incl_lt_iff_lt_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
P : LieSubmodule R L M → Prop :=
  fun (N : LieSubmodule R L M) ↦
    IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
⊢ IsCompl.{u_4} (α := LieSubmodule R L ↥(LieSubmodule.map N.incl N')) (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0)
    (posFittingComp R L ↥(LieSubmodule.map N.incl N'))

Tactic:
exact hN _ (LieSubmodule.map_incl_lt_iff_lt_top.mpr hN')

Premises used: Iff.mpr, LieSubmodule.map_incl_lt_iff_lt_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
rw :
  Disjoint (α := Submodule R M) (↑(genWeightSpaceOf M φ₁ x) : Submodule R M)
    (↑(genWeightSpaceOf M φ₂ x) : Submodule R M)
⊢ Disjoint (α := LieSubmodule R L M) (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x)

Tactic:
rw [← LieSubmodule.disjoint_toSubmodule]

Premises used: LieSubmodule.disjoint_toSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint.{u_4} (α := 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) φ₁)
    (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:
Module.End.disjoint_genEigenspace _ h _ _

Premises used: Module.End.disjoint_genEigenspace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint.{u_4} (α := 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) φ₁)
    (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:
exact Module.End.disjoint_genEigenspace _ h _ _

Premises used: Module.End.disjoint_genEigenspace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
⊢ ∃ (x : L), χ₁ x ≠ χ₂ x

Tactic:
Function.ne_iff.mp h

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
obtain : ∀ (x : L) (hx : χ₁ x ≠ χ₂ x), Disjoint (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)
⊢ Disjoint (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, χ₁ x ≠ χ₂ x := Function.ne_iff.mp h

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
x : L
hx : χ₁ x ≠ χ₂ x
⊢ Disjoint (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Tactic:
(disjoint_genWeightSpaceOf R L M hx).mono
    (genWeightSpace_le_genWeightSpaceOf M x χ₁) (genWeightSpace_le_genWeightSpaceOf M x χ₂)

Premises used: LieModule.disjoint_genWeightSpaceOf, LieModule.genWeightSpace_le_genWeightSpaceOf, Disjoint.mono
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
x : L
hx : χ₁ x ≠ χ₂ x
⊢ Disjoint (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Tactic:
exact (disjoint_genWeightSpaceOf R L M hx).mono
    (genWeightSpace_le_genWeightSpaceOf M x χ₁) (genWeightSpace_le_genWeightSpaceOf M x χ₂)

Premises used: LieModule.disjoint_genWeightSpaceOf, LieModule.genWeightSpace_le_genWeightSpaceOf, Disjoint.mono
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
χ₁ : L → R
h : Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} χ₁
χ₂ : L → R
hχ₂ : Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} χ₂
hχ₁₂ : Eq (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)
contrapose! : ∀ (hχ₂ : χ₁ ≠ χ₂), χ₂ ∉ {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}
⊢ χ₁ = χ₂

Tactic:
contrapose! hχ₂
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
χ₁ : L → R
h : Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} χ₁
χ₂ : L → R
hχ₁₂ : Eq (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}

Tactic:
simpa [hχ₁₂] using disjoint_genWeightSpace R L M hχ₂

Premises used: LieModule.disjoint_genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
simp : iSupIndep (α := Submodule R M) fun (i : L → R) ↦ ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule R M)
⊢ iSupIndep (α := LieSubmodule R L M) fun (χ : L → R) ↦ genWeightSpace M χ

Tactic:
simp only [← LieSubmodule.iSupIndep_toSubmodule, genWeightSpace,
    LieSubmodule.iInf_toSubmodule]

Premises used: LieSubmodule.iInf_toSubmodule, LieModule.genWeightSpace, LieSubmodule.iSupIndep_toSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ iSupIndep (α := Submodule R M) fun (i : L → R) ↦ ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule R M)

Tactic:
Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)

Premises used: LieModule.genWeightSpaceOf, LieSubmodule.lie_mem, LieModule.toEnd, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ iSupIndep (α := Submodule R M) fun (i : L → R) ↦ ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule R M)

Tactic:
exact Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)

Premises used: LieModule.genWeightSpaceOf, LieSubmodule.lie_mem, LieModule.toEnd, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ iSupIndep (α := LieSubmodule R L M) fun (χ : Weight R L M) ↦ genWeightSpace M (⇑χ : (a : L) → R)

Tactic:
(iSupIndep_genWeightSpace R L M).comp <|
    Subtype.val_injective.comp (Weight.equivSetOf R L M).injective

Premises used: iInf, Subtype.val_injective, iSupIndep.comp, LieModule.Weight.equivSetOf, Function.Injective.comp, LieModule.iSupIndep_genWeightSpace, Equiv.injective, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
rw : iSupIndep.{u_2 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i x) : Submodule R M)
⊢ iSupIndep.{u_2 + 1, u_4} (α := LieSubmodule R L M) fun (χ : R) ↦ genWeightSpaceOf M χ x

Tactic:
rw [← LieSubmodule.iSupIndep_toSubmodule]

Premises used: LieSubmodule.iSupIndep_toSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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} (α := Submodule R M) fun (i : 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) i

Tactic:
(toEnd R L M x).independent_genEigenspace _

Premises used: Module.End.independent_genEigenspace, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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} (α := Submodule R M) fun (i : 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) i

Tactic:
exact (toEnd R L M x).independent_genEigenspace _

Premises used: Module.End.independent_genEigenspace, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_10 : IsNoetherian R M
x : L
⊢ Set.Finite.{u_2} (α := R) {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ x) ⊥}

Tactic:
WellFoundedGT.finite_ne_bot_of_iSupIndep (iSupIndep_genWeightSpaceOf R L M x)

Premises used: WellFoundedGT.finite_ne_bot_of_iSupIndep, setOf, LieModule.iSupIndep_genWeightSpaceOf
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_10 : IsNoetherian R M
⊢ Set.Finite (α := L → R) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}

Tactic:
WellFoundedGT.finite_ne_bot_of_iSupIndep (iSupIndep_genWeightSpace R L M)

Premises used: WellFoundedGT.finite_ne_bot_of_iSupIndep, setOf, LieModule.iSupIndep_genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 (↑{χ : 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
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
this : Finite (↑{χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} : Type (max u_2 u_3))
⊢ Finite (Weight R L M)

Tactic:
Finite.of_injective (equivSetOf R L M) (equivSetOf R L M).injective

Premises used: LieModule.Weight.equivSetOf, Equiv.injective, DFunLike.coe, Finite.of_injective
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
this : Finite (↑{χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} : Type (max u_2 u_3))
⊢ Finite (Weight R L M)

Tactic:
exact Finite.of_injective (equivSetOf R L M) (equivSetOf R L M).injective

Premises used: LieModule.Weight.equivSetOf, Equiv.injective, DFunLike.coe, Finite.of_injective
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 : IsTriangularizable R L M
x : L
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      Module.End.maxGenEigenspace
        ((toEnd R (↥(LieHom.range (toEnd R L M))) M : (a : ↥(toEnd R L M).range) → Module.End R M)
          (Subtype.mk (p := fun (x : Module.End R M) ↦
              Membership.mem (γ := LieSubalgebra R (Module.End R M)) (LieHom.range (toEnd R L M)) x)
              ((((↑(toEnd R L M) : LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (Module.End R M)) :
                    LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (Module.End R M)) :
                  (a : L) → Module.End R M)
                x)
              ⋯ :
            ↥(LieHom.range (toEnd R L M))))
        φ)
    ⊤

Tactic:
IsTriangularizable.maxGenEigenspace_eq_top x

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 : IsTriangularizable R L M
x : L
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      Module.End.maxGenEigenspace
        ((toEnd R (↥(LieHom.range (toEnd R L M))) M : (a : ↥(toEnd R L M).range) → Module.End R M)
          (Subtype.mk (p := fun (x : Module.End R M) ↦
              Membership.mem (γ := LieSubalgebra R (Module.End R M)) (LieHom.range (toEnd R L M)) x)
              ((((↑(toEnd R L M) : LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (Module.End R M)) :
                    LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (Module.End R M)) :
                  (a : L) → Module.End R M)
                x)
              ⋯ :
            ↥(LieHom.range (toEnd R L M))))
        φ)
    ⊤

Tactic:
exact IsTriangularizable.maxGenEigenspace_eq_top x

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top