Cannot pattern match `fun` expressions?

Stream: mathlib4

[Li Xuanji]

import Mathlib

structure Struct where
  n₀ : ℤ

instance Struct.instCoe : Coe (ℕ → ℕ) Struct where
  coe := fun a ↦ {
    n₀ := a 0
  }

abbrev zero (a: Struct) : Prop :=
  a.n₀ = 0

lemma isZero_of_coe (a:ℕ → ℕ)
  : zero (a:Struct) ↔ 1 = 1 := by sorry

example : zero ((fun _:ℕ ↦ 3):Struct) := by
  rw [isZero_of_coe (fun _:ℕ ↦ 3)]

example : zero ((fun _:ℕ ↦ 3):Struct) := by
  rw [isZero_of_coe _]

Why does the first rw succeed but the second one fail? The error message is

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  zero { n₀ := ↑(?m.1419 0) }
⊢ zero { n₀ := ↑((fun x => 3) 0) }Lean 4

(This problem arose in a project using Mathlib, and I can't seem to make a repro case without Mathlib, so I'm tentatively posting it here)

[Robin Arnez]

Coercions are eagerly unfolded, so it sees (fun x => 3) 0 and immediately reduces it to 3 and it no longer matches f 0. You should probably use a dedicated coercion function instead:

@[coe]
def Struct.coe (a : ℕ → ℕ) : Struct where
  n₀ := a 0

instance : Coe (ℕ → ℕ) Struct where
  coe := Struct.coe

Then it turns ((fun _:ℕ ↦ 3):Struct) into Struct.coe (fun _:ℕ ↦ 3) and it can match just fine