# Zulip Chat Archive

## 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`

.

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

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