Intersection_of_Equivalences

import Mathlib.Data.Set.Basic

theorem Intersection_of_Equivalences {α : Type _} (R₁ R₂ : α → α → Prop) (h₁refl : ∀ x, R₁ x x) (h₁sym : ∀ x y, R₁ x y → R₁ y x) (h₁trans : ∀ x y z, R₁ x y → R₁ y z → R₁ x z) (h₂refl : ∀ x, R₂ x x) (h₂sym : ∀ x y, R₂ x y → R₂ y x) (h₂trans : ∀ x y z, R₂ x y → R₂ y z → R₂ x z) : (∀ x, R₁ x x ∧ R₂ x x) ∧ (∀ x y, (R₁ x y ∧ R₂ x y) → (R₁ y x ∧ R₂ y x)) ∧ (∀ x y z, (R₁ x y ∧ R₂ x y) → (R₁ y z ∧ R₂ y z) → (R₁ x z ∧ R₂ x z)) := by sorry