def kostant_base_change_iso_local {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) (V : Type u_2) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) : ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) ≃ₗ[ℂ] ↥(WeightSpace Δ V 0)

theorem corollary_14_3_dim_eq {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) (V : Type u_2) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) : Module.finrank ℂ ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) = Module.finrank ℂ ↥(WeightSpace Δ V 0)

def HomAdEquivariant.postcomp {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {V : Type u_3} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] {N : LieBimodule R 𝔤} {M : LieBimodule R 𝔤} (π : N.carrier →ₗ[R] M.carrier) (hπ_left : ∀ (u : UniversalEnvelopingAlgebra R 𝔤) (n : N.carrier), π ((N.leftAction u) n) = (M.leftAction u) (π n)) (hπ_right : ∀ (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (n : N.carrier), π ((N.rightAction u) n) = (M.rightAction u) (π n)) : ↥(HomAdEquivariant V N) →ₗ[R] ↥(HomAdEquivariant V M)

theorem corollary_14_5 {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [Module.Finite ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (hlocfin : IsHarishChandraBimodule M) : (∃ (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) (V : Type u_hc_bim) (x : AddCommGroup V) (x_1 : Module ℂ V) (x_2 : LieRingModule 𝔤 V) (x_3 : LieModule ℂ 𝔤 V) (_ : Module.Finite ℂ V) (_ : LieModule.IsIrreducible ℂ 𝔤 V) (surj : TensorProduct ℂ V (MaximalQuotient χ) →ₗ[ℂ] M.carrier), Function.Surjective ⇑surj ∧ ∀ (x_6 : 𝔤) (t : TensorProduct ℂ V (MaximalQuotient χ)), surj (((tensorBimodule (LieBimodule.trivial V) χ).adjointAction x_6) t) = (M.adjointAction x_6) (surj t)) ∧ ∀ (W : Type) [inst : AddCommGroup W] [inst_1 : Module ℂ W] [inst_2 : LieRingModule 𝔤 W] [inst_3 : LieModule ℂ 𝔤 W] [Module.Finite ℂ W], LieModule.IsIrreducible ℂ 𝔤 W → Module.Finite ℂ ↥(HomAdEquivariant W M)