ext refl

Stream: new members

[Joachim Breitner]

Is := by { ext, refl } or := ext (λ _ , rfl) or something else preferred?

[Arthur Paulino]

Not that it says a lot, but searching through mathlib, I found 24 occurrences of := by { ext, refl } and no occurrences of := ext (λ _ , rfl)

[Arthur Paulino]

129 results for by { ext, refl } and no results for ext (λ _ , rfl)

[Kyle Miller]

Without context, I'd prefer the first. A #mwe would be helpful to judge, though (maybe there's yet another proof that's more preferred than either?)

[Kyle Miller]

@Arthur Paulino You get a few results with git grep 'ext (λ ., rfl)' and 138 results with git grep 'ext \$ λ ., rfl'

[Joachim Breitner]

Context is https://github.com/leanprover-community/mathlib/pull/11456/files#diff-550fc0afdc9ac16171ae2a2f7760792f6464d9eb31476d5e54ba14069f1bd460R511

[Joachim Breitner]

But I guess the by … version is fine, thanks!

[Eric Wieser]

ext (λ _ , rfl) would normally be spelt ext $ λ _, rfl I think

[Eric Wieser]

For that particular line, fun_like.coe_injective rfl probably works

[Eric Wieser]

And avoids an axiom vs the ext, reflproof, but no one cares anyway

[Kyle Miller]

@Eric Wieser The second git grep I mentioned agrees with you regarding its normal spelling, though it's basically a tie between that and the by { ext, refl } proof.

[Yaël Dillies]

ext $ λ _, rfl has the advantage of not going into tactic mode, but really both are fine.

[Kyle Miller]

(I don't really think it matters -- this is one of those small places where you can really express yourself :smile:)

[Eric Wieser]

Note that sometimes ext as a tactic can do far more than you need it to - for instance, on a map between polynomials it will not only apply the map but also extract coefficients - this can end up slowing things down if you're just going to do refl afterwards anyway

[Johan Commelin]

by { ext1, refl } to the rescue (-;