Why does rewrite fail?

Stream: new members

[Dominic Steinitz]

import Mathlib

variable
  {m : ℕ}
  {n : ℕ}

lemma baz_eq {M N : Type*} [TopologicalSpace M] [TopologicalSpace N]
  (φ : Homeomorph N (EuclideanSpace ℝ (Fin n)))
  (ψ : Homeomorph M (EuclideanSpace ℝ (Fin m)))
  {f : M → N} : f ∘ (ψ.invFun ∘ ψ.toFun) = f := by
    funext x
    have h : ψ.invFun (ψ.toFun x) = x := ψ.left_inv x
    rw [h]

But I get

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
ψ.invFun (ψ.toFun x)

I can see such a pattern but what do I do to persuade lean to see it?

[Ruben Van de Velde]

Well, you need to squint to see it :)

You don't have a function application whose argument is a function application in your goal, you've got a single application of a composition of functions, so you need to get rid of those first:

    rw [Function.comp_apply, Function.comp_apply]