question about `le` on sets

Stream: general

[Scott Morrison]

import data.set.lattice

-- FAILS:
example {X : Type*} {ι : Type*} (U : ι → set X) {x} {i} (h : x ∈ U i) : x ∈ supr U :=
(le_supr U i) h -- function expected at `le_supr U i` term has type `complete_lattice.le (U i) (supr U)`

-- WORKS, but makes me sad:
example {X : Type*} {ι : Type*} (U : ι → set X) {x} {i} (h : x ∈ U i) : x ∈ supr U :=
begin
  have := le_supr U i,
  exact this h
end

[Scott Morrison]

What is one meant to do here to write a term-mode proof?

[Yury G. Kudryashov]

(show ..., from ...) h

[Sebastien Gouezel]

-- WORKS:
example {X : Type*} {ι : Type*} (U : ι → set X) {x} {i} (h : x ∈ U i) : x ∈ supr U :=
(le_supr U i : _) h

[Scott Morrison]

I'd forgotten that trick.

[Mario Carneiro]

alternatively

example {X : Type*} {ι : Type*} : ∀ (U : ι → set X) {i x}, x ∈ U i → x ∈ supr U := le_supr

[Eric Wieser]

Can you explain what's going on in that trick @Sebastien Gouezel?

[Kenny Lau]

Lean elaborates from outside to inside

[Kenny Lau]

that trick forces Lean to evaluate the inside first

[Gabriel Ebner]

@Eric Wieser During elaboration, Lean keeps track of the "expected type" of a subexpression. For example, if we elaborate (x + y : ℕ), then the expected type of x will be ℕ, no matter how little we know about x.
This works by propagating the expected type to the arguments when elaborating function applications. I believe this is what goes wrong in the first example. The (e : _) pattern is idiomatically used to prevent the expected type propagation.

[Eric Wieser]

Is there somewhere sensible to collect tricks like this, along with the trick of by letI := ....; exact for letI in term mode, etc?

[Johan Commelin]

I don't think we have anything more organised than Zulip atm...

[Johan Commelin]

But feel free to PR them to the "extra" docs

[Johan Commelin]

https://github.com/leanprover-community/mathlib/tree/master/docs/extras

[Kevin Buzzard]

Eric, if you can list ten tips which newcomers can only find out by running into them and asking, I could write a blog post :-)

[Eric Wieser]

@Johan Commelin, I assume you mean https://github.com/leanprover-community/leanprover-community.github.io/tree/newsite/templates/extras?

[Johan Commelin]

Probably, yes

[Johan Commelin]

I'm getting old

[Johan Commelin]

We should burn that other directory with fire (or just leave a README with a pointer to the new location).

[Patrick Massot]

I thought the old one already disappeared

[Eric Wieser]

A redirect from the old page would be more useful - I think google indexes it above the new one

[Chris Wong]

I don't think GitHub Pages supports automatic redirects, sadly. But maybe <link rel="canonical"> can help with the Google issue?
https://en.wikipedia.org/wiki/Canonical_link_element

[Bryan Gin-ge Chen]

Johan Commelin said:

We should burn that other directory with fire (or just leave a README with a pointer to the new location).

I've added some README files in #3623.