unknown free variable in `rewrite`

Stream: lean4

[Aaron Liu]

I think this has something to do with the metavariables depending on the thing being rewritten

def Set (α : Type u) : Type u := sorry
def Set.preimage (f : α → β) (s : Set β) : Set α := sorry
def Set.univ : Set α := sorry
def Set.range (f : α → β) : Set β := sorry
instance : Inter (Set α) := sorry

theorem Set.inter_univ (a : Set α) : a ∩ Set.univ = a := sorry
theorem Set.preimage_range (f : α → β) : Set.preimage f (Set.range f) = Set.univ := sorry
theorem Set.preimage_inter {f : α → β} {s t : Set β} :
    Set.preimage f (s ∩ t) = Set.preimage f s ∩ Set.preimage f t := sorry

theorem completelyNormalSpace_iff_forall_isOpen_normalSpace.extracted_1_1.extracted_1_1
    {X : Type u} {Y : Type v} (s t : Set X) (f : Y → X)
    (U : Set X) (hsU : Set.preimage f s = sorry)
    (V : Set X) (htV : Set.preimage f t = sorry)
    (hUV : U = V) : False := by
  -- unknown free variable `_fvar.434`
  rewrite [← Set.inter_univ (Set.preimage _ _),
    ← Set.preimage_range, ← Set.preimage_inter] at hsU htV