awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hj : k₂ ≤ (i, j).2
h :
  Eq (α := M₁ ⊗[R] M₂)
    ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
    (0 : M₁ ⊗[R] M₂)
h₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) 0) 0
h₂ h₃ : Eq (α := M₁ ⊗[R] M₂) 0 0
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)

Tactic:
rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hf₂, map_zero]

Premises used: map_zero, Module.End.pow_map_zero_of_le, Module.End.mul_apply
-- 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
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
a :
  Membership.mem (γ := Submodule R M)
    (LinearMap.range (M := TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x))
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x)))
    ⁅y, m⁆
⊢ Membership.mem (γ := Submodule R M) 𝕎(M, χ₁ + χ₂, x) ⁅y, m⁆

Tactic:
apply LieModule.weight_vector_multiplication L M M (toModuleHom R L M) χ₁ χ₂

Premises used: LieModule.toModuleHom, LieModule.weight_vector_multiplication
-- 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
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
a :
  ∃ (y_1 : TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x)),
    (toModuleHom R L M : (a : L ⊗[R] M) → M)
        ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
              (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
            y_1 :
          L ⊗[R] M) =
      ⁅y, m⁆
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.range (M := TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x))
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x)))
    ⁅y, m⁆

Tactic:
simp only [LieModuleHom.coe_toLinearMap, Function.comp_apply, LinearMap.coe_comp,
    TensorProduct.mapIncl, LinearMap.mem_range]

Premises used: TensorProduct.mapIncl, LieModuleHom.coe_toLinearMap, LinearMap.coe_comp, LinearMap.mem_range, Function.comp_apply
-- 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
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
h :
  (toModuleHom R L M : (a : L ⊗[R] M) → M)
      ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
            (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
          (Subtype.mk (p := fun (x_1 : L) ↦ Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) x_1) y hy ⊗ₜ[R]
            Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) x_1) m hm) :
        L ⊗[R] M) =
    ⁅y, m⁆
⊢ ∃ (y_1 : TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x)),
    (toModuleHom R L M : (a : L ⊗[R] M) → M)
        ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
              (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
            y_1 :
          L ⊗[R] M) =
      ⁅y, m⁆

Tactic:
use ⟨y, hy⟩ ⊗ₜ ⟨m, hm⟩
-- 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
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
⊢ (toModuleHom R L M : (a : L ⊗[R] M) → M)
      ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
            (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
          (Subtype.mk (p := fun (x_1 : L) ↦ Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) x_1) y hy ⊗ₜ[R]
            Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) x_1) m hm) :
        L ⊗[R] M) =
    ⁅y, m⁆

Tactic:
simp only [Submodule.subtype_apply, toModuleHom_apply, TensorProduct.map_tmul]

Premises used: Submodule.subtype_apply, LieModule.toModuleHom_apply, TensorProduct.map_tmul
-- 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
χ : R
x y : L
m : M
hm :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid 𝕎(M, χ, x)))) m
⊢ Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) m

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid] at hm ⊢

Premises used: AddSubsemigroup.mem_carrier, Submodule.mem_toAddSubmonoid, AddSubmonoid.mem_toSubsemigroup
-- 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
χ : R
x y : L
m : M
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) m
rw : Membership.mem (γ := Submodule R M) 𝕎(M, 0 + χ, x) ⁅y, m⁆
⊢ Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) ⁅y, m⁆

Tactic:
rw [← zero_add χ]

Premises used: zero_add
-- 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
χ : R
x y : L
m : M
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) m
⊢ Membership.mem (γ := Submodule R L) 𝕎(L, 0, x) y

Tactic:
simp
-- 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
χ : R
x y : L
m : M
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) m
⊢ Membership.mem (γ := Submodule R M) 𝕎(M, 0 + χ, x) ⁅y, m⁆

Tactic:
exact lie_mem_maxGenEigenspace_toEnd (by simp) hm

Premises used: LieModule.lie_mem_maxGenEigenspace_toEnd
-- 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
χ : R
x : L
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpaceOf M χ x) m ↔
    ∃ (k : ℕ),
      Eq (α := M)
        ((HSub.hSub (α := Module.End R 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 :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) χ 1) ^
                k :
              (a : M) → M)
            m :
          M)
        (0 : M)

Tactic:
simp [genWeightSpaceOf]

Premises used: LieModule.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
x : L
⊢ Eq (α := Submodule R M) (↑(genWeightSpaceOf M 0 x) : Submodule R M)
    (⨆ (k : ℕ),
      (HPow.hPow (α := Module.End R 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 : Module.End R M)
          k).ker)

Tactic:
simp [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq]

Premises used: LieModule.genWeightSpaceOf, Module.End.iSup_genEigenspace_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
χ : L → R
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m ↔
    ∀ (x : L),
      ∃ (k : ℕ),
        Eq (α := M)
          ((HSub.hSub (α := Module.End R 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 :
                      Module.End R M)
                    (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                  k :
                (a : M) → M)
              m :
            M)
          (0 : M)

Tactic:
simp [genWeightSpace, mem_genWeightSpaceOf]

Premises used: LieModule.mem_genWeightSpaceOf, 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
x : L
χ : L → R
⊢ LE.le (α := LieSubmodule R L M) (genWeightSpace M χ) (genWeightSpaceOf M (χ x) x)

Tactic:
iInf_le _ x

Premises used: Set.Mem, iInf_le
-- 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
χ : L → R
h : ∀ (i : L), LE.le (α := LieSubmodule R L M) (weightSpace M χ) (genWeightSpaceOf M (χ i) i)
⊢ LE.le (α := LieSubmodule R L M) (weightSpace M χ) (genWeightSpace M χ)

Tactic:
apply le_iInf

Premises used: le_iInf
-- 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
χ : L → R
x : L
h :
  LE.le.{u_4} (α := Submodule R M)
    (Module.End.eigenspace (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      (χ x))
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M)
      (genWeightSpaceOf M (χ x) x))
⊢ LE.le (α := Submodule R M)
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M) (weightSpace M χ) :
      Submodule R M)
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M)
        (genWeightSpaceOf M (χ x) x) :
      Submodule R M)

Tactic:
apply (iInf_le _ x).trans

Premises used: LE.le.trans, iInf_le
-- 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
χ : L → R
x : L
⊢ LE.le.{u_4} (α := Submodule R M)
    (Module.End.eigenspace (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      (χ x))
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M)
      (genWeightSpaceOf M (χ x) x))

Tactic:
((toEnd R L M x).genEigenspace (χ x)).monotone le_top

Premises used: OrderHom.monotone, Set.Mem, setOf, le_top, LieModule.toEnd, Module.End.genEigenspace, 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
χ : L → R
x : L
⊢ LE.le.{u_4} (α := Submodule R M)
    (Module.End.eigenspace (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      (χ x))
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M)
      (genWeightSpaceOf M (χ x) x))

Tactic:
exact ((toEnd R L M x).genEigenspace (χ x)).monotone le_top

Premises used: OrderHom.monotone, le_top, LieModule.toEnd, Module.End.genEigenspace, DFunLike.coe
-- 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
χ₁ χ₂ : Weight R L M
h : Eq (α := (a : L) → R) ((fun (χ : Weight R L M) ↦ χ.toFun) χ₁) ((fun (χ : Weight R L M) ↦ χ.toFun) χ₂)
mk :
  ∀ (toFun : L → R) (genWeightSpace_ne_bot' : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun) ⊥)
    (h :
      Eq (α := (a : L) → R)
        ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
        ((fun (χ : Weight R L M) ↦ χ.toFun) χ₂)),
    { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } = χ₂
⊢ χ₁ = χ₂

Tactic:
cases χ₁
-- 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
χ₂ : Weight R L M
toFun : L → R
genWeightSpace_ne_bot' : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun) ⊥
h :
  Eq (α := (a : L) → R)
    ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
    ((fun (χ : Weight R L M) ↦ χ.toFun) χ₂)
mk :
  ∀ (toFun_1 : L → R) (genWeightSpace_ne_bot'_1 : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun_1) ⊥)
    (h :
      Eq (α := (a : L) → R)
        ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
        ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 })),
    { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } =
      { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 }
⊢ { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } = χ₂

Tactic:
cases χ₂
-- 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
toFun : L → R
genWeightSpace_ne_bot' : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun) ⊥
toFun_1 : L → R
genWeightSpace_ne_bot'_1 : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun_1) ⊥
h :
  Eq (α := (a : L) → R)
    ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
    ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 })
⊢ { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } =
    { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 }

Tactic:
simp_all
-- 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
χ : L → R
h : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
⊢ (⇑{ toFun := χ, genWeightSpace_ne_bot' := h : Weight R L M } : (a : L) → R) = χ

Tactic:
rfl

Premises used: rfl
-- 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
χ : Weight R L M
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (⇑χ : (a : L) → R)) ⊥

Tactic:
χ.genWeightSpace_ne_bot'

Premises used: LieModule.Weight.genWeightSpace_ne_bot'
-- 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
χ₁ χ₂ : Weight R L M
h : ∀ (x : L), Eq.{u_2 + 1} (α := R) ((χ₁ : (a : L) → R) x : R) ((χ₂ : (a : L) → R) x : R)
⊢ χ₁ = χ₂

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- 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
χ₁ χ₂ : Weight R L M
⊢ Eq (α := (a : L) → R) (⇑χ₁ : (a : L) → R) (⇑χ₂ : (a : L) → R) ↔ χ₁ = χ₂

Tactic:
simp
-- 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
χ : Weight R L M
⊢ ∃ (x : M), Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M (⇑χ : (a : L) → R)) x ∧ x ≠ 0

Tactic:
simpa [LieSubmodule.eq_bot_iff] using χ.genWeightSpace_ne_bot

Premises used: LieModule.Weight.genWeightSpace_ne_bot, LieSubmodule.eq_bot_iff
-- 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 : Subsingleton M
⊢ IsEmpty (Weight R L M)

Tactic:
⟨fun h ↦ h.2 (Subsingleton.elim _ _)⟩

Premises used: Bot.bot, IsEmpty.mk, LieModule.genWeightSpace, Subsingleton.elim, LieModule.Weight.toFun, LieModule.Weight.genWeightSpace_ne_bot'
-- 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 : Nontrivial.{u_4} ↥(genWeightSpace M 0)
⊢ Eq (α := (a : L) → R) (⇑0 : (a : L) → R) 0

Tactic:
rfl

Premises used: rfl
-- 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 : Nontrivial.{u_4} ↥(genWeightSpace M 0)
x : L
⊢ Eq.{u_2 + 1} (α := R) ((0 : (a : L) → R) x : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- 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
χ : Weight R L M
hχ : χ.IsZero
⊢ Eq (α := (a : L) → R) (⇑χ : (a : L) → R) 0

Tactic:
hχ

Premises used: LieModule.Weight.IsZero
-- 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
χ : Weight R L M
⊢ Eq (α := (a : L) → R) (⇑χ : (a : L) → R) 0 ↔ χ.IsZero

Tactic:
Iff.rfl

Premises used: Iff.rfl, LieModule.Weight.IsZero
-- 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 : Nontrivial.{u_4} ↥(genWeightSpace M 0)
χ : Weight R L M
⊢ χ.IsZero ↔ χ = 0

Tactic:
Weight.ext_iff' (χ₂ := 0)

Premises used: LieModule.Weight.ext_iff', LieModule.Weight.IsZero
-- 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 : Nontrivial.{u_4} ↥(genWeightSpace M 0)
⊢ IsZero.{u_2, u_3, u_4} (R := R) (L := L) (M := M) 0

Tactic:
rfl

Premises used: LieModule.Weight.IsZero, rfl
-- 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 : Nontrivial.{u_4} ↥(genWeightSpace M 0)
χ : Weight R L M
⊢ χ.IsNonZero ↔ χ ≠ 0

Tactic:
isZero_iff_eq_zero.not

Premises used: Iff.not, LieModule.Weight.isZero_iff_eq_zero