Congruence and `liftFun`s

Stream: mathlib4

[Andrés Goens]

I found these two small lemmas to be useful when working with congruence over an equivalence relation to use functions like Quotient.map as they expect the congruence expressed using liftFun and not the more direct (in my opinion) version of congruence

lemma congr_liftFun {α β : Type} [HasEquiv α] [HasEquiv β] {f : α → β}
    (h : ∀ x y, x ≈ y → f x ≈ f y) : ((· ≈ ·) ⇒ (· ≈ ·)) f f := by
  intro x y hxy; exact h x y hxy

lemma congr_liftFun₂ {α β γ : Type} [HasEquiv α] [HasEquiv β] [HasEquiv γ] {f : α → β → γ}
    (h : ∀ (x₁ x₂ : α) (y₁ y₂ : β), x₁ ≈ x₂ → y₁ ≈ y₂ → f x₁ y₁ ≈ f x₂ y₂) :
 ((· ≈ ·) ⇒ (· ≈ ·) ⇒ (· ≈ ·)) f f := by
  intro x₁ x₂ hx y₁ y₂ hy; exact h x₁ x₂ y₁ y₂ hx hy

I've made a small PR with these two lemmas, thinking it might be useful to have them in Mathlib, if they're not (or I missed them somewhere else), please also let me know: https://github.com/leanprover-community/mathlib4/pull/15127

Not 100% sure about the names conforming to the naming conventions, as the congruence is not explicitly named, but I thought that made sense this way.

[Eric Wieser]

There's nothing special about ≈ here right? These would work for an arbitrary R

[Eric Wieser]

(also the first one can be proved with := h)

[Andrés Goens]

ah, you're right, it works just the same with any relation, thanks for the hints!