## Stream: general

### Topic: convert with congr lemmas

#### Yury G. Kudryashov (Jun 11 2020 at 04:40):

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 (Jun 11 2020 at 04:41):

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

#### Johan Commelin (Jun 11 2020 at 11:37):

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

#### Yury G. Kudryashov (Jun 12 2020 at 02:29):

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

#### Yury G. Kudryashov (Jun 12 2020 at 02:30):

Who understands internals of this tactic? @Mario Carneiro ?

#### Mario Carneiro (Jun 12 2020 at 02:31):

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

#### Mario Carneiro (Jun 12 2020 at 02:31):

Unfortunately congr doesn't do funext

#### Mario Carneiro (Jun 12 2020 at 02:32):

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

#### Yury G. Kudryashov (Jun 12 2020 at 02:34):

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

#### Yury G. Kudryashov (Jun 12 2020 at 02:39):

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.

I thought it did

#### Mario Carneiro (Jun 12 2020 at 02:53):

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

#### Yury G. Kudryashov (Jun 12 2020 at 03:36):

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 (Jun 17 2020 at 14:59):

@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.

Last updated: Dec 20 2023 at 11:08 UTC