awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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
⊢ LinearMap.ker (LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule) = ⊥
have h : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
have rwa : ∀ (h : rootSpace H 0 ⊔ LieModule.posFittingComp R (↥H) 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
have rwa₅ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ Codisjoint H.toSubmodule (↑(LieModule.posFittingComp R (↥H) L) : Submodule R L)
have rwa₆ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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)
⊢ LinearMap.ker (LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule) = ⊥
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ LinearMap.ker (LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule) = ⊥
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun (γ : ↥H → K) ↦ α + (β + γ)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
Tactic: have hσ : ∀ γ, σ γ ≠ γ := fun γ ↦ by simpa only [σ, ← add_assoc] using add_ne_right.mpr hαβ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun (γ : ↥H → K) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
Tactic: have hf : ∀ γ, MapsTo f (rootSpace H γ) (rootSpace H (σ γ)) := fun γ ↦
    (mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (β + γ) hx).comp <|
      mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L β γ hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun (γ : ↥H → K) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have hds : DirectSum.IsInternal (S := Submodule K L) fun (i : ↥H → K) ↦ (↑(genWeightSpace L i) : Submodule K L)
Tactic: have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace K H L)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top K H L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun (γ : ↥H → K) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have have : ∀ (hds : DirectSum.IsInternal (S := Submodule K L) fun (i : ↥H → K) ↦ (↑(genWeightSpace L i) : Submodule K L)),
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
Tactic: classical
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace K H L)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top K H L)
  exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
⊢ Eq (α := L →ₗ[K] K) ((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) (0 : L →ₗ[K] K)
have h : ∀ (y : L),
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
have hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y
Tactic: have hy : y ∈ ⨆ β, rootSpace H β := by simp [iSup_genWeightSpace_eq_top K H L]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
have pos : ∀ (hαβ : α + β = 0),
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
Tactic: by_cases hαβ : α + β = 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
pos :
  ∀ (hαβ : α + β = 0),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
have neg : ∀ (hαβ : ¬α + β = 0),
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
Tactic: by_cases hαβ : α + β = 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
have h : ∀ (β : ↥H → K) (y : L) (hy : y ∈ rootSpace H β),
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
Tactic: induction hy using LieSubmodule.iSup_induction' with
  | mem β y hy =>
    by_cases hαβ : α + β = 0
    · exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
    · exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ
  | zero => simp
  | add => simp_all
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y
h :
  ∀ (β : ↥H → K) (y : L) (hy : y ∈ rootSpace H β),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
have h₁ : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K)
  ((0 : (a : L) → K) 0 : K)
Tactic: induction hy using LieSubmodule.iSup_induction' with
  | mem β y hy =>
    by_cases hαβ : α + β = 0
    · exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
    · exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ
  | zero => simp
  | add => simp_all
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y
h :
  ∀ (β : ↥H → K) (y : L) (hy : y ∈ rootSpace H β),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
h₁ :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K)
    ((0 : (a : L) → K) 0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)
have h₂ : ∀ (x_1 y : L),
  Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1 →
    Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y →
      Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) x_1 : K)
          ((0 : (a : L) → K) x_1 : K) →
        Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
            ((0 : (a : L) → K) y : K) →
          Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) (x_1 + y) : K)
            ((0 : (a : L) → K) (x_1 + y) : K)
Tactic: induction hy using LieSubmodule.iSup_induction' with
  | mem β y hy =>
    by_cases hαβ : α + β = 0
    · exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
    · exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ
  | zero => simp
  | add => simp_all
Cleared hypotheses: hy