Effective epimorphisms in LightProfinite

This file proves that EffectiveEpi and Surjective are equivalent in LightProfinite. As a consequence we deduce from the material in Mathlib.Topology.Category.CompHausLike.EffectiveEpi that LightProfinite is Preregular and Precoherent.

theorem LightProfinite.effectiveEpi_iff_surjective {X Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

instance LightProfinite.instPreregular : CategoryTheory.Preregular LightProfinite