feat(Logic/Relation): more lemmas relating Relation.Map and Function.onFun

Author: SnirBroshi

Mathlib/Logic/Relation.lean

@@ -240,19 +240,36 @@ lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : 
     ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y :=
   fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩
 
+lemma le_onFun_map {r : α → α → Prop} (f : α → β) :
+    ∀ x y, r x y → (Relation.Map r f f on f) x y := by
+  grind [Relation.Map]
+
+lemma onFun_map_eq_of_injective {r : α → α → Prop} {f : α → β} (hinj : f.Injective) :
+    (Relation.Map r f f on f) = r := by
+  ext x y
+  exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩
+
 lemma map_onFun_le {r : β → β → Prop} (f : α → β) :
-    ∀ x y, Relation.Map (Function.onFun r f) f f x y → r x y := by
+    ∀ x y, Relation.Map (r on f) f f x y → r x y := by
   grind [Relation.Map]
 
-lemma map_onFun_eq_of_surjective {r : β → β → Prop} {f : α → β} (hsurj : Function.Surjective f) :
-    Relation.Map (Function.onFun r f) f f = r := by
+lemma map_onFun_eq_of_surjective {r : β → β → Prop} {f : α → β} (hsurj : f.Surjective) :
+    Relation.Map (r on f) f f = r := by
   ext x y
   have _ := hsurj x
   have _ := hsurj y
   grind [Relation.Map]
 
-lemma map_onFun_iff {r : β → β → Prop} (f : α → β) (a₁ a₂ : α) :
-    Relation.Map (Function.onFun r f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂) := by
+lemma map_onFun_map_eq_map {r : α → α → Prop} (f : α → β) :
+    Relation.Map (Relation.Map r f f on f) f f = Relation.Map r f f := by
+  grind [Relation.Map]
+
+lemma onFun_map_onFun_eq_onFun {r : β → β → Prop} (f : α → β) :
+    (Relation.Map (r on f) f f on f) = (r on f) := by
+  grind [Relation.Map]
+
+lemma onFun_map_onFun_iff_onFun {r : β → β → Prop} (f : α → β) (a₁ a₂ : α) :
+    Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂) := by
   grind [Relation.Map]
 
 end Map