convert with congr lemmas

Stream: general

[Yury G. Kudryashov]

Is there a version of convert that uses congr lemmas to dive into structures? E.g., I want to convert ∑ i in s, f i ≤ ∑ i in s, g i to ∑ i in s, f' i ≤ ∑ i in s, g' i and get goals ∀ i ∈ s, f i = f' i and ∀ i ∈ s, g i = g' i.

[Yury G. Kudryashov]

Of course, I can use convert ... using ...; apply sum_congr rfl; ... but I'd prefer to use a tactic.

[Johan Commelin]

Hmm, I'm actually surprised that convert doesn't just do that (modulo a funext)...

[Yury G. Kudryashov]

Currently it generates goals λ i, f i = λ i, f' i and λ i, g i = λ i, g' i.

[Yury G. Kudryashov]

Who understands internals of this tactic? @Mario Carneiro ?

[Mario Carneiro]

convert is a wrapper around congr', which is a thin veneer over core's congr

[Mario Carneiro]

Unfortunately congr doesn't do funext

[Mario Carneiro]

You can find plenty of examples of congr, funext, congr if you search mathlib

[Yury G. Kudryashov]

Would it be hard to write a version that uses @[congr] lemmas? funext is not the main problem here.

[Yury G. Kudryashov]

I mean, for me as a user the main problem is that it asks me to prove λ i, f i = λ i, f' i instead of ∀ i ∈ s, f i = f' i.

[Mario Carneiro]

I thought it did

[Mario Carneiro]

When you give it the equality goal does congr do the right thing?

[Yury G. Kudryashov]

Tried these examples right after lemma prod_congr in algebra/big_operators:

example [has_le β] (h : 1 ≤ ∏ x in s₁, f x) : 1 ≤ ∏ x in s₂, g x :=
begin
  convert h,
end

α : Type u,
β : Type v,
s₁ s₂ : finset α,
f g : α → β,
_inst_1 : comm_monoid β,
_inst_2 : has_le β,
h : 1 ≤ ∏ (x : α) in s₁, f x
⊢ 1 ≤ ∏ (x : α) in s₂, g x

example : (∏ x in s₁, f x) = ∏ x in s₂, f x :=
begin
  congr,
end

α : Type u,
β : Type v,
s₁ s₂ : finset α,
f : α → β,
_inst_1 : comm_monoid β
⊢ s₁ = s₂

[Yury G. Kudryashov]

@Gabriel Ebner says that this is the intended behaviour: neither congr nor convert use @[congr]. It seems that none of @Mario Carneiro , @Johan Commelin and me knew for sure about this fact. I'll make a doc PR tonight.