Products of Hom ideals under equivalences

theorem MagnitudeConjecture.homIdealProduct_comap_equivalence {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (E : C ≌ D) [E.functor.Additive] (I J : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal D) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap E.functor I ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap E.functor J = QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap E.functor (I ⋆ᵢ J)

An equivalence identifies the product of pulled-back ideals with the pullback of their product. Intermediates downstairs lift using the counit.