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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
have apply : posFittingComp R L M ≤ LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ posFittingCompOf R M x
Tactic: apply le_antisymm <| sup_le_iff.mpr
        ⟨map_posFittingComp_le _, posFittingCompOf_le_posFittingComp R L 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 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ posFittingComp R L M ≤ LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ posFittingCompOf R M x
have rw : LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ LieSubmodule.map M₁ₓ.incl (posFittingComp R L ↥M₁ₓ) ≤
  LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ posFittingCompOf R M x
Tactic: rw [← posFittingComp_map_incl_sup_of_codisjoint h₁.codisjoint]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ IsCompl M₀ M₁
have h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
Tactic: have h₄ : M₀ₓ₁.map M₀ₓ.incl ⊔ M₁ₓ = M₁ := by
      apply le_antisymm <| sup_le_iff.mpr
        ⟨map_posFittingComp_le _, posFittingCompOf_le_posFittingComp R L M x⟩
      rw [← posFittingComp_map_incl_sup_of_codisjoint h₁.codisjoint]
      exact sup_le_sup_left LieSubmodule.map_incl_le _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ IsCompl M₀ M₁
have inr : IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ)
Tactic: rw [← h₃, ← h₄]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ)
have inr : Disjoint (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁)
Tactic: apply Disjoint.isCompl_sup_right_of_isCompl_sup_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
inr : Disjoint (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁)
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ)
have inr₁ : IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊔ LieSubmodule.map M₀ₓ.incl M₀ₓ₁) M₁ₓ
Tactic: apply Disjoint.isCompl_sup_right_of_isCompl_sup_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ Disjoint (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁)
have inr : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊓ LieSubmodule.map M₀ₓ.incl M₀ₓ₁ = ⊥
Tactic: rw [disjoint_iff, ← LieSubmodule.map_inf M₀ₓ.injective_incl, h₂.inf_eq_bot,
        LieSubmodule.map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
inr : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊓ LieSubmodule.map M₀ₓ.incl M₀ₓ₁ = ⊥
⊢ Disjoint (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁)
have inr₁ : LieSubmodule.map M₀ₓ.incl (M₀ₓ₀ ⊓ M₀ₓ₁) = ⊥
Tactic: rw [disjoint_iff, ← LieSubmodule.map_inf M₀ₓ.injective_incl, h₂.inf_eq_bot,
        LieSubmodule.map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
inr : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊓ LieSubmodule.map M₀ₓ.incl M₀ₓ₁ = ⊥
inr₁ : LieSubmodule.map M₀ₓ.incl (M₀ₓ₀ ⊓ M₀ₓ₁) = ⊥
⊢ Disjoint (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁)
have inr₂ : LieSubmodule.map M₀ₓ.incl ⊥ = ⊥
Tactic: rw [disjoint_iff, ← LieSubmodule.map_inf M₀ₓ.injective_incl, h₂.inf_eq_bot,
        LieSubmodule.map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
inr : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊓ LieSubmodule.map M₀ₓ.incl M₀ₓ₁ = ⊥
inr₁ : LieSubmodule.map M₀ₓ.incl (M₀ₓ₀ ⊓ M₀ₓ₁) = ⊥
inr₂ : LieSubmodule.map M₀ₓ.incl ⊥ = ⊥
⊢ Disjoint (LieSubmodule.map M₀ₓ.incl M₀ₓ₀) (LieSubmodule.map M₀ₓ.incl M₀ₓ₁)
have inr₃ : Eq.{u_4 + 1} (α := LieSubmodule R L M) ⊥ ⊥
Tactic: rw [disjoint_iff, ← LieSubmodule.map_inf M₀ₓ.injective_incl, h₂.inf_eq_bot,
        LieSubmodule.map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊔ LieSubmodule.map M₀ₓ.incl M₀ₓ₁) M₁ₓ
have inr : IsCompl (LieSubmodule.map M₀ₓ.incl (M₀ₓ₀ ⊔ M₀ₓ₁)) M₁ₓ
Tactic: rwa [← LieSubmodule.map_sup, h₂.sup_eq_top, LieModuleHom.map_top, LieSubmodule.range_incl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
inr : IsCompl (LieSubmodule.map M₀ₓ.incl (M₀ₓ₀ ⊔ M₀ₓ₁)) M₁ₓ
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊔ LieSubmodule.map M₀ₓ.incl M₀ₓ₁) M₁ₓ
have inr₁ : IsCompl (LieSubmodule.map M₀ₓ.incl ⊤) M₁ₓ
Tactic: rwa [← LieSubmodule.map_sup, h₂.sup_eq_top, LieModuleHom.map_top, LieSubmodule.range_incl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
inr : IsCompl (LieSubmodule.map M₀ₓ.incl (M₀ₓ₀ ⊔ M₀ₓ₁)) M₁ₓ
inr₁ : IsCompl (LieSubmodule.map M₀ₓ.incl ⊤) M₁ₓ
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊔ LieSubmodule.map M₀ₓ.incl M₀ₓ₁) M₁ₓ
have inr₂ : IsCompl M₀ₓ.incl.range M₁ₓ
Tactic: rwa [← LieSubmodule.map_sup, h₂.sup_eq_top, LieModuleHom.map_top, LieSubmodule.range_incl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
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)
this : P ⊤
e : ↥⊤ ≃ₗ⁅R,L⁆ M := LieModuleEquiv.ofTop R L M
⊢ IsCompl (α := LieSubmodule R L M) (genWeightSpace M 0) (posFittingComp R L M)
have rw : IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥⊤) 0))
  (LieSubmodule.map e.toLieModuleHom (posFittingComp R L ↥⊤))
Tactic: rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
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)
⊢ IsCompl (α := LieSubmodule R L M) (genWeightSpace M 0) (posFittingComp R L M)
have suffices : P ⊤
Tactic: suffices P ⊤ by
    let e := LieModuleEquiv.ofTop R L M
    rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e]
    exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mp 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 : 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)
⊢ P ⊤
have ind : ∀ (N : LieSubmodule R L M) (hN : ∀ y < N, P y), P N
Tactic: induction (⊤ : LieSubmodule R L M) using
    (LieSubmodule.wellFoundedLT_of_isArtinian R L M).induction with | ind N hN
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
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
⊢ P N
have ind : ∀ (N' : LieSubmodule R L ↥N) (hN' : N' < ⊤),
  IsCompl.{u_4} (α := LieSubmodule R L ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
Tactic: refine isCompl_genWeightSpace_zero_posFittingComp_aux R L N fun N' hN' ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
inst_9 : IsArtinian R M
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.{u_4} (α := LieSubmodule R L ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
have this₁ : 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
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 : 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 ↥N') (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
have 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'))
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
-- 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
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint (α := LieSubmodule R L M) (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x)
have rw : Disjoint (α := Submodule R M) (↑(genWeightSpaceOf M φ₁ x) : Submodule R M) (↑(genWeightSpaceOf M φ₂ x) : Submodule R M)
Tactic: rw [← LieSubmodule.disjoint_toSubmodule]
-- 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
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
⊢ Disjoint (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)
have obtain : ∀ (x : L) (hx : χ₁ x ≠ χ₂ x), Disjoint (α := LieSubmodule R L M) (genWeightSpace M χ₁) (genWeightSpace M χ₂)
Tactic: obtain ⟨x, hx⟩ : ∃ x, χ₁ x ≠ χ₂ x := Function.ne_iff.mp h
-- 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
χ₁ : 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 χ₂)
⊢ χ₁ = χ₂
have contrapose! : ∀ (hχ₂ : χ₁ ≠ χ₂), χ₂ ∉ {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}
Tactic: contrapose! hχ₂
Cleared hypotheses: hχ₂
-- 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
⊢ iSupIndep (α := LieSubmodule R L M) fun (χ : L → R) ↦ genWeightSpace M χ
have simp : iSupIndep (α := Submodule R M) fun (i : L → R) ↦ ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule R M)
Tactic: simp only [← LieSubmodule.iSupIndep_toSubmodule, genWeightSpace,
    LieSubmodule.iInf_toSubmodule]