Type synonyms and let

Stream: mathlib4

[Sébastien Gouëzel]

I need to introduce a type synonym in a proof. I tried to do it with let M' := M, but this is too transparent. Is that intended? Is there a standard way to do this? I can do it with a custom def MyCopy (M : Type*) : Type _ := M, but it seems a little bit too much.

class Topo (M : Type _)

theorem foo {M : Type _} [Topo M] : true := by
  let M' := M
  letI : Topo M' := by infer_instance -- works, too bad
  trivial

def MyCopy (M : Type _) : Type _ := M

theorem bar {M : Type _} [Topo M] : true := by
  let M' := MyCopy M
  letI : Topo M' := by infer_instance -- fails, good
  trivial

[Kenny Lau]

@Sébastien Gouëzel I used generalize to get the behaviour wanted:

theorem bar {M : Type _} [Topo M] : true := by
  generalize h : M = M'
  letI : Topo M' := by infer_instance -- fails, good
  trivial

[Sébastien Gouëzel]

It doesn't work for me because I want M' and M to be defeq.

[Andrew Yang]

How about

theorem foo {M : Type _} [Topo M] : true := by
  let M' := id M
  letI : Topo M' := by infer_instance -- fails, good

[Sébastien Gouëzel]

Perfect, thanks !

[Kevin Buzzard]

I am now surprised that I didn't run into this in my proof that the product of the module topolgoies was the module topology, but on re-examining the proof I think that I get away with this

  -- In this proof, `M × N` always denotes the product with its *product* topology.
  ...
  -- Or equivalently, if `P` denotes `M × N` with the module topology,
  let P := M × N
  let τP : TopologicalSpace P := moduleTopology R P
  ...

because although I've just learnt that apparently P would have got the product topology, I immediately overrid it with the module topology, giving me defeq P and M × N with typeclass inference putting two different topologies on them anyway.