## Stream: new members

### Topic: Lean guessing the wrong function

#### Nicolò Cavalleri (Sep 03 2020 at 17:59):

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 (Sep 03 2020 at 18:23):

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 (Sep 03 2020 at 20:05):

sometimes (hg.comp hf : _) works

#### Kenny Lau (Sep 03 2020 at 20:06):

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

#### Nicolò Cavalleri (Sep 04 2020 at 10:16):

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

Last updated: May 14 2021 at 07:19 UTC