awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
mem :
  ∀ (n : ℕ) (hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥),
    ∃ (n : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            m₂ :
          M)
        (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)

Tactic:
obtain ⟨n, -, hn⟩ := exists_genWeightSpace_smul_add_eq_bot M χ χ₂ hχ

Premises used: LieModule.exists_genWeightSpace_smul_add_eq_bot, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
h :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)

Tactic:
use n
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K)))
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)

Tactic:
have := toEnd_pow_apply_mem hx hm₂ n
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
this :
  Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K)))
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
h :
  ∀
    (this :
      Membership.mem (α := M) (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) ⊥
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            m₂ :
          M)),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
h₁ h₂ h₃ h₄ :
  ∀
    (this :
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            m₂ :
          M)
        (0 : M)),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)

Tactic:
rwa [hn, LieSubmodule.mem_bot] at this

Premises used: LieSubmodule.mem_bot
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
hm₁' :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₁ :
        M)
      (0 : M)
hm₂' :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
add :
  ∀ (n₁ : ℕ)
    (hn₁ :
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n₁ :
              (a : M) → M)
            m₁ :
          M)
        (0 : M)),
    ∃ (n : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            (m₁ + m₂) :
          M)
        (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)

Tactic:
obtain ⟨n₁, hn₁⟩ := hm₁'
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
hm₂' :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m₂ :
        M)
      (0 : M)
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
add :
  ∀ (n₂ : ℕ)
    (hn₂ :
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n₂ :
              (a : M) → M)
            m₂ :
          M)
        (0 : M)),
    ∃ (n : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            (m₁ + m₂) :
          M)
        (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)

Tactic:
obtain ⟨n₂, hn₂⟩ := hm₂'
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)

Tactic:
⟨max n₁ n₂, ?_⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
add :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        (m₁ + m₂) :
      M)
    (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          (m₁ + m₂) :
        M)
      (0 : M)

Tactic:
refine ⟨max n₁ n₂, ?_⟩
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁
hm₂ :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂
n₁ : ℕ
hn₁ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₁ :
          (a : M) → M)
        m₁ :
      M)
    (0 : M)
n₂ : ℕ
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            n₂ :
          (a : M) → M)
        m₂ :
      M)
    (0 : M)
add :
  HAdd.hAdd (α := M) (β := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₁ :
        M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
add₁ :
  HAdd.hAdd (α := M) (β := M) (0 : M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) (max n₁ n₂) :
            (a : M) → M)
          m₂ :
        M) =
    0
add₂ : HAdd.hAdd (α := M) 0 0 = 0
add₃ add₄ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq (α := M)
    ((HPow.hPow (α := End K M) (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)
            (max n₁ n₂) :
          (a : M) → M)
        (m₁ + m₂) :
      M)
    (0 : M)

Tactic:
rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]

Premises used: le_sup_left, map_add, le_sup_right, Module.End.pow_map_zero_of_le, add_zero
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieAlgebra K L
H : LieSubalgebra K L
inst_4 : LieRing.IsNilpotent.{u_2} ↥H
inst_5 : IsTriangularizable K (↥H) L
inst_6 : FiniteDimensional K L
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)

Tactic:
isNilpotent_toEnd_of_mem_rootSpace (M := L) H hχ hx

Premises used: LieModule.isNilpotent_toEnd_of_mem_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
⊢ LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule = LieModule.traceForm R (↥H) L

Tactic:
rfl

Premises used: LinearMap.restrictScalars, Set.Mem, LinearMap.compr₂, LinearMap.domRestrict₁₂, LinearMap.domRestrict, LinearMap.BilinForm.restrict, rfl, LieModule.traceForm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
⊢ Codisjoint (rootSpace H 0) (LieModule.posFittingComp R (↥H) L)

Tactic:
have h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R H L) :=
    (LieModule.isCompl_genWeightSpace_zero_posFittingComp R H L).codisjoint
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R (↥H) L)
rwa :
  ∀ (h : rootSpace H 0 ⊔ LieModule.posFittingComp R (↥H) L = ⊤),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
rwa₁ :
  ∀ (h : (↑(rootSpace H 0 ⊔ LieModule.posFittingComp R (↥H) L) : Submodule R L) = (↑⊤ : Submodule R L)),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
rwa₂ :
  ∀
    (h :
      (↑(rootSpace H 0) : Submodule R L) ⊔ (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L) =
        (↑⊤ : Submodule R L)),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
rwa₃ :
  ∀ (h : (↑(rootSpace H 0) : Submodule R L) ⊔ (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L) = ⊤),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
rwa₄ :
  ∀ (h : (↑H.toLieSubmodule : Submodule R L) ⊔ (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L) = ⊤),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
rwa₅ :
  ∀ (h : H.toSubmodule ⊔ (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L) = ⊤),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
rwa₆ rwa₇ rwa₈ rwa₉ :
  ∀ (h : Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)),
    Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)

Tactic:
rwa [codisjoint_iff, ← LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule,
      LieSubmodule.top_toSubmodule, rootSpace_zero_eq R L H, LieSubalgebra.coe_toLieSubmodule,
      ← codisjoint_iff] at h

Premises used: codisjoint_iff, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, LieAlgebra.rootSpace_zero_eq, LieSubmodule.sup_toSubmodule, LieSubalgebra.coe_toLieSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R (↥H) L)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)

Tactic:
replace h : Codisjoint (H : Submodule R L) (LieModule.posFittingComp R H L : Submodule R L) := by
    rwa [codisjoint_iff, ← LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule,
      LieSubmodule.top_toSubmodule, rootSpace_zero_eq R L H, LieSubalgebra.coe_toLieSubmodule,
      ← codisjoint_iff] at h
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
h : Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
this :
  ∀ m₀ ∈ H,
    ∀ (m₁ : L),
      Membership.mem (γ := LieSubmodule R (↥H) L) (LieModule.posFittingComp R (↥H) L) m₁ →
        Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) m₀ : L →ₗ[R] R) : (a : L) → R) m₁ : R) (0 : R)
⊢ LinearMap.ker (LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule) = ⊥

Tactic:
simp [LinearMap.BilinForm.ker_restrict_eq_of_codisjoint h this]

Premises used: LinearMap.BilinForm.ker_restrict_eq_of_codisjoint
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
h : Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
suffices :
  ∀ m₀ ∈ H,
    ∀ (m₁ : L),
      Membership.mem (γ := LieSubmodule R (↥H) L) (LieModule.posFittingComp R (↥H) L) m₁ →
        Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) m₀ : L →ₗ[R] R) : (a : L) → R) m₁ : R) (0 : R)
⊢ LinearMap.ker (LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule) = ⊥

Tactic:
suffices this : ∀ m₀ ∈ H, ∀ m₁ ∈ LieModule.posFittingComp R H L, killingForm R L m₀ m₁ = 0 by
    simp [LinearMap.BilinForm.ker_restrict_eq_of_codisjoint h this]
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
h : Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
m₀ : L
h₀ : m₀ ∈ H
m₁ : L
h₁ : Membership.mem (γ := LieSubmodule R (↥H) L) (LieModule.posFittingComp R (↥H) L) m₁
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) m₀ : L →ₗ[R] R) : (a : L) → R) m₁ : R) (0 : R)

Tactic:
killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting R L H (le_zeroRootSubalgebra R L H h₀) h₁

Premises used: killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting, LieAlgebra.le_zeroRootSubalgebra
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
h : Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
m₀ : L
h₀ : m₀ ∈ H
m₁ : L
h₁ : Membership.mem (γ := LieSubmodule R (↥H) L) (LieModule.posFittingComp R (↥H) L) m₁
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) m₀ : L →ₗ[R] R) : (a : L) → R) m₁ : R) (0 : R)

Tactic:
exact killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting R L H (le_zeroRootSubalgebra R L H h₀) h₁

Premises used: killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting, LieAlgebra.le_zeroRootSubalgebra
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
⊢ Eq (α := Submodule R ↥H) (LinearMap.ker (LieModule.traceForm R (↥H) L)) ⊥

Tactic:
ker_restrict_eq_bot_of_isCartanSubalgebra R L H

Premises used: LinearMap.restrictScalars, Set.Mem, LinearMap.compr₂, LinearMap.domRestrict₁₂, LinearMap.domRestrict, LinearMap.BilinForm.restrict, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, LieModule.traceForm