Merge remote-tracking branch 'origin/master' into filtered-is-connected

Mathlib/CategoryTheory/IsConnected.lean

@@ -347,7 +347,7 @@
 #align category_theory.equiv_relation CategoryTheory.equiv_relation
 
 /-- In a connected category, any two objects are related by `Zigzag`. -/
-theorem isConnected_zigzag [IsPreconnected J] (j₁ j₂ : J) : Zigzag j₁ j₂ :=
+theorem isPreconnected_zigzag [IsPreconnected J] (j₁ j₂ : J) : Zigzag j₁ j₂ :=
   equiv_relation _ zigzag_equivalence
     (@fun _ _ f => Relation.ReflTransGen.single (Or.inl (Nonempty.intro f))) _ _
 #align category_theory.is_connected_zigzag CategoryTheory.isPreconnected_zigzag
@@ -365,7 +365,7 @@
     rcases hj with (⟨⟨hj⟩⟩|⟨⟨hj⟩⟩)
     exacts [hF hj, (hF hj).symm]
 
 theorem zigzag_isPreconnected (h : ∀ j₁ j₂ : J, Zigzag j₁ j₂) : IsPreconnected J := by
   apply IsPreconnected.of_constant_of_preserves_morphisms
   intro α F hF j j'
   specialize h j j'
@@ -440,7 +440,7 @@
     ext j
     apply nat_trans_from_is_connected f (Classical.arbitrary J) j
 
-instance nonempty_hom_of_connected_groupoid {G} [Groupoid G] [IsPreconnected G] :
+theorem nonempty_hom_of_preconnected_groupoid {G} [Groupoid G] [IsPreconnected G] :
     ∀ x y : G, Nonempty (x ⟶ y) := by
   refine' equiv_relation _ _ @fun j₁ j₂ => Nonempty.intro
   exact