Rewrite rule not being applied inside lambda

Stream: general

[Juneyoung Lee]

This would be a fairly basic question, but sometimes the rewrite rule doesn't seem to apply inside the body of abstraction. When does it happen exactly?
For example, Lean4 has List.count_cons:

theorem count_cons {a b : α} {l : List α} :
    count a (b :: l) = count a l + if b == a then 1 else 0 := by
  simp [count, countP_cons]

however, rw [List.count_cons] doesn't apply even when the following goal has two counts inside.

...
⊢ map (fun x => (x, count x (h :: hd :: tl))) (hd :: tl).dedup = map (fun x => (x, count x (hd :: tl))) (hd :: tl).dedup

[Riccardo Brasca]

The precise explanation is quite complicated, but if you just want to make it working you can try simp_rw or conv mode.

[Snir Broshi]

or rw!

[Aaron Liu]

does rw! work here? I would think it fails for the same reason that rw fails (i.e. the pattern contains bound variables)

[Snir Broshi]

Nope, you're right:

import Mathlib
open List
variable {α : Type*} [DecidableEq α] {h hd : α} {tl : List α}

/--
error: Tactic `depRewrite` failed: did not find instance of the pattern in the target expression
  count ?m.34 (?m.35 :: ?m.36)

α : Type u_1
inst✝ : DecidableEq α
h hd : α
tl : List α
⊢ map (fun x => (x, count x (h :: hd :: tl))) (hd :: tl).dedup = map (fun x => (x, count x (hd :: tl))) (hd :: tl).dedup
-/
#guard_msgs in
theorem foo :
    map (fun x => (x, count x (h :: hd :: tl))) (hd :: tl).dedup =
      map (fun x => (x, count x (hd :: tl))) (hd :: tl).dedup := by
  rw! [List.count_cons]
  sorry

[Snir Broshi]

Though I don't understand why, I thought rw! can rewrite under binders

[Jovan Gerbscheid]

rw! doesn't rewrite bound variable. rw! is a solution to the other annoying rw error, the motive not type correct error. rw! fixes this by inserting casts in the right places to create a valid rewrite.