Zulip Chat Archive

Stream: new members

Topic: Lean guessing the wrong function


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 03 2020 at 20:05):

sometimes (hg.comp hf : _) works

view this post on Zulip 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

view this post on Zulip 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