Lean guessing the wrong function

Stream: new members

[Nicolò Cavalleri]

In this example

import topology.algebra.monoid

example {α : Type*} {β : Type*} [topological_space α] [monoid α]
  [topological_space β] [monoid β]
  (x : β × β) {f : β →* α} (hf : continuous_at (λ p : β × β, (f p.fst) * (f p.snd)) x)
  {g : α → β} (hg : continuous_at g ((f x.fst) * (f x.snd))) :
  continuous_at (λ p : β × β, g ((f p.1) * (f p.2))) x :=
begin
  exact hg.comp hf,
end

Lean guesses the wrong function to perform the composition. I am pretty sure what I wrote makes sense mathematically and it is just Lean making a random assumption on the form of the hypothesis. How can I fix it?

[Sebastien Gouezel]

Sometimes you need to use the @ version, where you can give all the information, to help Lean. In this case, it looks like continuous_at.comp hg hf is enough.

[Kenny Lau]

sometimes (hg.comp hf : _) works

[Kenny Lau]

i.e. have Lean infer the type of the expression instead of trying to elaborate it to match the expected type

[Nicolò Cavalleri]

Sebastien Gouezel said:

Sometimes you need to use the @ version, where you can give all the information, to help Lean. In this case, it looks like continuous_at.comp hg hf is enough.

Ok thanks! Just for the records, if someone encounters a similar problem, this did not work in the original lemma I was trying to prove where the two hypotheses hg and hf were obtained with have but it did work the combination of this and substituting the haves with the original proofs