∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Type u_5} {f : M →ₙ+ N},
  Function.Injective ⇑f →
    ∀ (S : ι → AddSubsemigroup M), AddSubsemigroup.comap f (⨅ i, AddSubsemigroup.map f (S i)) = iInf S