Discretize tactic

Stream: mathlib4

[Patrick Massot]

We have tactic#borelize but not the analogous tactic that would endow a type with the discrete topology and add the corresponding DiscreteTopology instance in the local context. @Filippo A. E. Nuccio and @María Inés de Frutos Fernández need the discrete uniformity version in the local class field project. I propose to have discretize and discretize_uniformly for those two tactics. For instance it allows really cool proofs like:

[Patrick Massot]

example {α β : Type _} (f : α → β) (s : Set α) (h : s.Finite) : (f '' s).Finite := by
  discretize α β
  rw [← isCompact_iff_finite] at *
  exact h.image continuous_of_discreteTopology

[Patrick Massot]

(and I’m told the applications to local class field theory are even more interesting).

[Patrick Massot]

Before opening a PR to mathlib, I’d be interested to know whether there is any reason we shouldn’t have this. I don’t know who wrote the Borel version, probably @Sébastien Gouëzel or @Yury G. Kudryashov?

[Yaël Dillies]

It looks totally reasonable to me, apart from the fact that discretize is way too generic as a tactic name

[Patrick Massot]

Any suggestion for a better name?

[Kim Morrison]

I think discretize is not so bad. If you're worried about naming conflicts with something outside topology, with_discrete_topology α β seems the obvious solution.

[Eric Wieser]

Perhaps the tactic notation could be in the Topology scope?

[Yury G. Kudryashov]

Should we just put the discrete metric space structure (dist a b := if a = b then 0 else 1)?