Problem with `convert`

Stream: new members

[Vivek Rajesh Joshi]

image.png

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.

image.png

Could someone explain why, and what the goal means?

[Ruben Van de Velde]

Convert is going too far. Try convert cs4 using 1 with increasing numbers until you get something sensible

[Martin Dvořák]

What does using do?

[Damiano Testa]

using n instructs congr to descend n layers into the expressions before leaving what is left as a side-goal. Approximately.

[Damiano Testa]

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]

(note that congr attempts to prove the side-goal, so the c = c goal disappears due to this extra mechanism)

[Martin Dvořák]

I just tried congr 1 is it.

[Martin Dvořák]

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]

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]

(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]

Got it, my question was resolved with convert cs4 using 1. Thanks a lot!