feat(Logic/Function/Basic) : lemmas about composition of and in onFun (leanprover-community#39776)

`(f.onFun g).onFun h = f.onFun (g ∘ h)` and its symmetric variant.

Author: Hagb

Mathlib/Logic/Function/Basic.lean

@@ -55,6 +55,12 @@ section onFun
 theorem onFun_apply (f : β → β → γ) (g : α → β) (a b : α) : onFun f g a b = f (g a) (g b) :=
   rfl
 
+theorem onFun_onFun_eq {δ : Sort*} (f : α → α → γ) (g : β → α) (h : δ → β) :
+    (f.onFun g).onFun h = f.onFun (g ∘ h) := rfl
+
+theorem onFun_comp_eq {δ : Sort*} (f : α → α → γ) (g : β → α) (h : δ → β) :
+    f.onFun (g ∘ h) = (f.onFun g).onFun h := rfl
+
 variable (r : β → β → Prop) (f : α → β)
 
 instance [Std.Refl r] : Std.Refl (r on f) where