nth_rw

Stream: mathlib4

[Kenny Lau]

import Mathlib.Tactic.NthRewrite

theorem id_apply_mul {a b : Nat} : id (a * b) = a * b := rfl

example : (2 * 3) + (5 * 6) = 4 := by nth_rw 1 2 [← id_apply_mul]
-- ⊢ id (2 * 3) + 5 * 6 = 4

example : (2 * 3) + (2 * 3) = 4 := by nth_rw 1 2 [← id_apply_mul]
-- ⊢ id (2 * 3) + id (2 * 3) = 4

Is this intentional? That nth_rw for more than one n only works on the exact previous match of the pattern

[Aaron Liu]

Yes

[Kenny Lau]

(Note that it doesn't help if I write it a second time inside the same call)

[Kenny Lau]

what should I write if I want to make it id (2 * 3) + id (5 * 6)?

[Aaron Liu]

You have to rewrite twice then

[Aaron Liu]

Kenny Lau said:

(Note that it doesn't help if I write it a second time inside the same call)

What do you mean by this?

[Kenny Lau]

import Mathlib.Tactic.NthRewrite

theorem id_apply_mul {a b : Nat} : id (a * b) = a * b := rfl

example : (2 * 3) + (5 * 6) = 4 := by nth_rw 1 2 [← id_apply_mul, ← id_apply_mul]
-- ⊢ id (id (2 * 3)) + 5 * 6 = 4

[Kenny Lau]

I understand that I need to write nth_rw twice

[Aaron Liu]

In any case, I'd recommend using conv mode over nth_rw

[Aaron Liu]

Kenny Lau said:

import Mathlib.Tactic.NthRewrite

theorem id_apply_mul {a b : Nat} : id (a * b) = a * b := rfl

example : (2 * 3) + (5 * 6) = 4 := by nth_rw 1 2 [← id_apply_mul, ← id_apply_mul]
-- ⊢ id (id (2 * 3)) + 5 * 6 = 4

This matches 2 * 3 twice independently

[Kenny Lau]

Aaron Liu said:

In any case, I'd recommend using conv mode over nth_rw

why?

[Aaron Liu]

It feels better to me? I'm not sure.

[Kenny Lau]

import Mathlib.Tactic.NthRewrite

theorem id_apply_mul {a b : Nat} : id (a * b) = a * b := rfl

example : (2 * 3) + (5 * 6) = 4 := by
  conv => rw [← id_apply_mul]; enter [1,2]; rw [← id_apply_mul]
  -- ⊢ id (2 * 3) + id (5 * 6) = 4

[Kenny Lau]

so you would prefer this?

[Aaron Liu]

What I'd actually do in this situation would be to make {a b : Nat} explicit in id_apply_mul

[Kenny Lau]

good call, that actually helped!

[Kenny Lau]

i forgot about matching patterns