Transporting a complete indecomposable family through an equivalence

theorem MagnitudeConjecture.CategoryTheory.complete_indecomposable_family_of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : C ≌ D) [E.functor.Additive] {ι : Type w} (F : ι → D) (hF : ∀ (Y : D), CategoryTheory.Indecomposable Y → ∃ (i : ι), Nonempty (Y ≅ F i)) (X : C) (hX : CategoryTheory.Indecomposable X) : ∃ (i : ι), Nonempty (X ≅ E.inverse.obj (F i))

Completeness transfers without unfolding the construction of the equivalence.