lift (f \circ of) = f

Stream: general

[Johan Commelin]

How should I name this lemma?

@[simp] lemma lift'_of_comp (f : localization α S → β) [is_ring_hom f] :
  lift' (f ∘ of) (units.map f ∘ to_units) (λ s, rfl) = f :=