π₀ (nerve C) ≃ ConnectedComponents C in Lean: lift along edges, ReflTransGen for zigzags

In SSet.π₀ (Mathlib PiZero.lean), the forward map is π₀.lift (fun x ↦ Quotient.mk (Zigzag.setoid C) (nerveEquiv x)) fun _ _ e ↦ Quotient.sound (Zigzag.of_hom (nerve.homEquiv e)). The inverse is Quotient.lift (fun c ↦ π₀.mk (nerveEquiv.symm c)), whose proof uses induction h with | refl | tail _ hz ih, since Zigzag is ReflTransGen Zag. Gotcha: Zag a b is Nonempty (a ⟶ b) ∨ Nonempty (b ⟶ a), so destructure with rcases hz with ⟨⟨f⟩⟩ | ⟨⟨f⟩⟩ (double brackets), then π₀.sound (nerve.edgeMk f). simp [π₀.lift_mk] made no progress on the round trips. Since lift ∘ mk is definitional, close them with exact congrArg π₀.mk (nerveEquiv.symm_apply_apply x).