an equation lemma with autoParam arguments fails to rewrite

[Komyyy]

Description

When we use an equation lemma of a definition with autoParam arguments in rewrite tactic, it fails.

Steps to Reproduce

import Lean

open Lean Elab Tactic in
elab "exact_false" : tactic =>
  closeMainGoal (mkConst ``Bool.false)

def f (b : Bool := by exact_false) : Nat := bif b then 1 else 0

example : f false = bif false then 1 else 0 := by rw [f]
example : f true = bif true then 1 else 0 := by rw [f]
example (b : Bool) : f b = bif b then 1 else 0 := by rw [f]

Expected behavior:

Above all 3 examples succeed.

Actual behavior:

example : f false = bif false then 1 else 0 := by rw [f]
-- failed to rewrite using equation theorems for 'f'
example : f true = bif true then 1 else 0 := by rw [f]
-- failed to rewrite using equation theorems for 'f'
example (b : Bool) : f b = bif b then 1 else 0 := by rw [f]
-- failed to rewrite using equation theorems for 'f'

Versions

Lean (version 4.0.0-nightly-2023-05-16, commit ebc32af, Release)
Windows 11