Minor improvement

Author: ocfnash

Mathlib/Algebra/Lie/Basis/Prod.lean

@@ -192,9 +192,10 @@ lemma surjective_snd_prod :
     ← b₁.basisProd_aux eι b₂, map_lieSpan, image_union, h₁, h₂]
   simp [range_comp]
 
-lemma lie_fst_eq_zero_of_mem_prodCartan [IsLieAbelian H₁]
+lemma lie_fst_eq_zero_of_mem_prodCartan
     {y : b₁.prod eι b₂} (hy : y ∈ prodCartan eι b₁ b₂) (x : H₁) :
     ⁅(y : L₁ × L₂).fst, (x : L₁)⁆ = 0 := by
+  have := b₁.isLieAbelian_cartan
   induction hy using lieSpan_induction with
   | mem u hu =>
     obtain ⟨i, rfl⟩ := hu
@@ -205,7 +206,7 @@ lemma lie_fst_eq_zero_of_mem_prodCartan [IsLieAbelian H₁]
   | smul t u hu hu' => simp [hu']
   | lie u v hu hv hu' hv' => simp [hu', hv']
 
-lemma lie_snd_eq_zero_of_mem_prodCartan [IsLieAbelian H₂]
+lemma lie_snd_eq_zero_of_mem_prodCartan
     {y : b₁.prod eι b₂} (hy : y ∈ prodCartan eι b₁ b₂) (x : H₂) :
     ⁅(y : L₁ × L₂).snd, (x : L₂)⁆ = 0 := by
   suffices (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁ from
@@ -228,7 +229,7 @@ variable {K : Type*} [Field K] [CharZero K]
   (hA : b₁.A.reindex eι eι = b₂.A)
 include hA
 
-lemma prod_lt_top [IsKilling K L₁] [IsKilling K L₂] [Nontrivial L₂] :
+lemma prod_lt_top [Nontrivial L₂] :
     b₁.prod eι b₂ < ⊤ := by
   /- This innocent-looking result is the key. The informal literature seems only to contain
   somewhat heavy-weight proofs (e.g., [Chapter IV, Theorem 14.2](humphreys1972) makes an