# Zulip Chat Archive

## Stream: new members

### Topic: Problem with `convert`

#### Vivek Rajesh Joshi (Aug 24 2023 at 04:55):

I want to use cs4 to close the goal, and according to what I have read in "Mathematics in Lean", `convert`

should do the job. But instead it is leaving me with a goal that I cannot understand.

Could someone explain why, and what the goal means?

#### Ruben Van de Velde (Aug 24 2023 at 05:16):

Convert is going too far. Try `convert cs4 using 1`

with increasing numbers until you get something sensible

#### Martin Dvořák (Aug 24 2023 at 06:35):

What does `using`

do?

#### Damiano Testa (Aug 24 2023 at 07:16):

`using n`

instructs `congr`

to descend `n`

layers into the expressions before leaving what is left as a side-goal. Approximately.

#### Damiano Testa (Aug 24 2023 at 07:19):

So (untested) `congr`

on

```
a + b + c = b + a + c
```

probably asks to prove all equalities of the variables. `congr 2`

(or 1?) might leave

```
a + b = b + a
```

Definitely test this!!

#### Damiano Testa (Aug 24 2023 at 07:20):

(note that congr attempts to prove the side-goal, so the `c = c`

goal disappears due to this extra mechanism)

#### Martin Dvořák (Aug 24 2023 at 07:21):

I just tried `congr 1`

is it.

#### Martin Dvořák (Aug 24 2023 at 07:26):

Using

```
example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 0
```

produces

```
⊢ R (b + a + c) ↔ R (a + b + c)
```

Using

```
example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 1
```

produces

```
⊢ b + a + c = a + b + c
```

Using

```
example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 2
```

produces

```
⊢ b + a = a + b
```

Using

```
example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 3
```

produces

```
⊢ b = a
⊢ a = b
```

#### Damiano Testa (Aug 24 2023 at 08:13):

Ah, `using 0`

converts to `↔`

: of course, this must be how `congr`

begins its descent into the expressions!

EDIT[I was confused by the fact that this is now `convert`

, and no longer `congr`

!]

#### Kyle Miller (Aug 24 2023 at 08:54):

(Small point of information, `convert`

starts with `=`

. It uses `congr!`

internally to apply congruence lemmas, and as a cleanup operation `congr!`

converts `=`

to `↔`

when both sides are Props.)

#### Vivek Rajesh Joshi (Aug 24 2023 at 10:35):

Got it, my question was resolved with `convert cs4 using 1`

. Thanks a lot!

Last updated: Dec 20 2023 at 11:08 UTC