# Zulip Chat Archive

## 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 `have`

s with the original proofs

Last updated: Dec 20 2023 at 11:08 UTC