rewrite inside `ite`?

Stream: new members

[Yannick Seurin]

It does not seem possible to do a rewrite inside an ite construction, for example :

import Mathlib

variable {α β : Type} [DecidableEq α] [DecidableEq β]
         (a : α) (b : β) (c : ℕ)

example (a b : α) (c d : β) : (a, c) = (b, d) ↔ a = b ∧ c = d := Prod.mk_inj

example : (∑' (p : α × β), if (p.1, p.2) = (a, b) then c else 0) = c := by
  exact tsum_ite_eq (a, b) c

example : (∑' (p : α × β), if p.1 = a ∧ p.2 = b then c else 0) = c := by
  -- rewrite `p.1 = a ∧ p.2 = b` as `(p.1, p.2) = (a, b)` to apply `tsum_ite_eq`
  rw [← Prod.mk_inj]
  /-
  Tactic `rewrite` failed: Did not find an occurrence of the pattern
    ?m.22 = ?m.23 ∧ ?m.24 = ?m.25
  in the target expression
    (∑' (p : α × β), if p.1 = a ∧ p.2 = b then c else 0) = c
  -/

Is there some fundamental reason why it is not possible, or is it just that it's not implemented? Also, how should I finish the proof of the second example without rewriting the if condition?

[Aaron Liu]

rw can't rewrite expressions containing bound variables

[Riccardo Brasca]

The usual solution is to try simp_rw. If it doesn't work you can use conv, but it's a little more annoying.

[Yannick Seurin]

simp_rw works, thanks! Always nice to learn new tactics.

[Alex Meiburg]

Quick note: the problem is not the ite, but the sum ∑' (p : α × β),, which is a binder. Under the hood, you're dealing with a function fun (p : α × β) => if p.1 = a ∧ p.2 = b then c else 0, and rw doesn't go into the function.