chore(Topology/Instances/Discrete): merge 2 instances (#11296)

Prove `DiscreteTopology.secondCountableTopology_of_countable` directly,
deprecate `DiscreteTopology.secondCountableTopology_of_encodable`.

Mathlib/Topology/Instances/Discrete.lean

@@ -33,18 +33,19 @@ instance (priority := 100) DiscreteTopology.firstCountableTopology [DiscreteTopo
   nhds_generated_countable := by rw [nhds_discrete]; exact isCountablyGenerated_pure
 #align discrete_topology.first_countable_topology DiscreteTopology.firstCountableTopology
 
-instance (priority := 100) DiscreteTopology.secondCountableTopology_of_encodable
-    [hd : DiscreteTopology α] [Encodable α] : SecondCountableTopology α :=
+instance (priority := 100) DiscreteTopology.secondCountableTopology_of_countable
+    [hd : DiscreteTopology α] [Countable α] : SecondCountableTopology α :=
   haveI : ∀ i : α, SecondCountableTopology (↥({i} : Set α)) := fun i =>
     { is_open_generated_countable :=
         ⟨{univ}, countable_singleton _, by simp only [eq_iff_true_of_subsingleton]⟩ }
   secondCountableTopology_of_countable_cover (singletons_open_iff_discrete.mpr hd)
     (iUnion_of_singleton α)
-#align discrete_topology.second_countable_topology_of_encodable DiscreteTopology.secondCountableTopology_of_encodable
+#align discrete_topology.second_countable_topology_of_encodable DiscreteTopology.secondCountableTopology_of_countable
 
-instance (priority := 100) DiscreteTopology.secondCountableTopology_of_countable {α : Type*}
+@[deprecated DiscreteTopology.secondCountableTopology_of_countable] -- 2024-03-11
+theorem DiscreteTopology.secondCountableTopology_of_encodable {α : Type*}
     [TopologicalSpace α] [DiscreteTopology α] [Countable α] : SecondCountableTopology α :=
-  @DiscreteTopology.secondCountableTopology_of_encodable _ _ _ (Encodable.ofCountable _)
+  DiscreteTopology.secondCountableTopology_of_countable
 #align discrete_topology.second_countable_topology_of_countable DiscreteTopology.secondCountableTopology_of_countable
 
 theorem bot_topologicalSpace_eq_generateFrom_of_pred_succOrder [PartialOrder α] [PredOrder α]