relation.lean

import tactic

inductive the_rel {X Y : Type} (R : X → Y → Prop) : X ⊕ Y → X ⊕ Y → Prop
| fwd {x y} : R x y → the_rel (sum.inl x) (sum.inr y)

def mkl {X Y : Type} (R : X → Y → Prop) (x : X) : quot (the_rel R) := quot.mk _ (sum.inl x)
def mkr {X Y : Type} (R : X → Y → Prop) (y : Y) : quot (the_rel R) := quot.mk _ (sum.inr y)

example {X Y : Type} {R : X → Y → Prop} : 
  (∀ x₁ x₂ y₁ y₂, R x₁ y₁ → R x₂ y₁ → R x₂ y₂ → R x₁ y₂) ↔
  ∃ (Z : Type) (f₁ : X → Z) (f₂ : Y → Z), (∀ x y, R x y ↔ f₁ x = f₂ y) :=
begin
  split,
  {
    intros h,
    refine ⟨_, mkl R, mkr R, _⟩,
    intros x y,
    split,
    {
      intros h',
      apply quot.sound,
      apply the_rel.fwd h',
    },
    {
      intros h',
      dsimp [mkl, mkr] at h',
      rw quot.eq at h',
      have : ∀ {a b}, eqv_gen (the_rel R) a b →
        (∃ x y, a = sum.inl x ∧ b = sum.inr y ∧ R x y) ∨
        (∃ x y, a = sum.inr y ∧ b = sum.inl x ∧ R x y) ∨
        (∃ x₁ x₂ y, a = sum.inl x₁ ∧ b = sum.inl x₂ ∧ R x₁ y ∧ R x₂ y) ∨
        (∃ x y₁ y₂, a = sum.inr y₁ ∧ b = sum.inr y₂ ∧ R x y₁ ∧ R x y₂) ∨
        a = b,
      {
        clear h' x y,
        intros a b h',
        induction h' with c d h' c c d h' ih c d e h' h'' ih ih',
        {
          cases h' with x y h'',
          left,
          refine ⟨_, _, rfl, rfl, h''⟩,
        },
        {
          right,
          right,
          right,
          right,
          refl,
        },
        {
          rcases ih with ⟨x, y, h₁, h₂, h₃⟩ | ⟨x, y, h₁, h₂, h₃⟩ | ⟨x₁, x₂, y, h₁, h₂, h₃, h₄⟩ | ⟨x₁, y₁, y₂, h₁, h₂, h₃, h₄⟩ | rfl,
          {
            right,
            left,
            refine ⟨_, _, h₂, h₁, h₃⟩,
          },
          {
            left,
            refine ⟨_, _, h₂, h₁, h₃⟩,
          },
          {
            right,
            right,
            left,
            refine ⟨_, _, _, h₂, h₁, h₄, h₃⟩,
          },
          {
            right,
            right,
            right,
            left,
            refine ⟨_, _, _, h₂, h₁, h₄, h₃⟩,
          },
          {
            right,
            right,
            right,
            right,
            refl,
          },
        },
        {
          rcases ih with ⟨x, y, h₁, h₂, h₃⟩ | ⟨x, y, h₁, h₂, h₃⟩ | ⟨x₁, x₂, y, h₁, h₂, h₃, h₄⟩ | ⟨x₁, y₁, y₂, h₁, h₂, h₃, h₄⟩ | rfl,
          {
            rcases ih' with ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x₁', x₂', y', h₁', h₂', h₃', h₄'⟩ | ⟨x₁', y₁', y₂', h₁', h₂', h₃', h₄'⟩ | rfl,
            {
              subst d,
              contradiction,
            },
            {
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂', h₃, _⟩,
              convert h₃',
              subst h₂,
              injection h₁',
            },
            {
              subst d,
              contradiction,
            },
            {
              left,
              refine ⟨_, _, h₁, h₂', _⟩,
              apply h _ _ _ _ _ h₃' h₄',
              convert h₃,
              subst h₁',
              injection h₂,
            },
            {
              left,
              refine ⟨_, _, h₁, h₂, h₃⟩,
            },
          },
          {
            rcases ih' with ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x₁', x₂', y', h₁', h₂', h₃', h₄'⟩ | ⟨x₁', y₁', y₂', h₁', h₂', h₃', h₄'⟩ | rfl,
            {
              right,
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂', h₃, _⟩,
              convert h₃',
              subst h₂,
              injection h₁',
            },
            {
              subst d,
              contradiction,
            },
            {
              right,
              left,
              refine ⟨_, _, h₁, h₂', _⟩,
              apply h _ _ _ _ h₄' _ h₃,
              convert h₃',
              subst h₂,
              injection h₁',
            },
            {
              subst d,
              contradiction,
            },
            {
              right,
              left,
              refine ⟨_, _, h₁, h₂, h₃⟩,
            },
          },
          {
            rcases ih' with ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x₁', x₂', y', h₁', h₂', h₃', h₄'⟩ | ⟨x₁', y₁', y₂', h₁', h₂', h₃', h₄'⟩ | rfl,
            {
              left,
              refine ⟨_, _, h₁, h₂', _⟩,
              apply h _ _ _ _ h₃ _ h₃',
              convert h₄,
              subst h₁',
              injection h₂,
            },
            {
              subst d,
              contradiction,
            },
            {
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂', h₃, _⟩,
              apply h _ _ _ _ h₄' _ h₄,
              convert h₃',
              subst h₂,
              injection h₁',
            },
            {
              subst d,
              contradiction,
            },
            {
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂, h₃, h₄⟩,
            },
          },
          {
            rcases ih' with ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x', y', h₁', h₂', h₃'⟩ | ⟨x₁', x₂', y', h₁', h₂', h₃', h₄'⟩ | ⟨x₁', y₁', y₂', h₁', h₂', h₃', h₄'⟩ | rfl,
            {
              subst d,
              contradiction,
            },
            {
              right,
              left,
              refine ⟨_, _, h₁, h₂', _⟩,
              apply h _ _ _ _ _ h₄ h₃,
              convert h₃',
              subst h₂,
              injection h₁',
            },
            {
              subst d,
              contradiction,
            },
            {
              right,
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂', h₃, _⟩,
              apply h _ _ _ _ h₄ _ h₄',
              convert h₃',
              subst h₂,
              injection h₁',
            },
            {
              right,
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂, h₃, h₄⟩,
            },
          },
          {
            rcases ih' with ⟨x, y, h₁, h₂, h₃⟩ | ⟨x, y, h₁, h₂, h₃⟩ | ⟨x₁, x₂, y, h₁, h₂, h₃, h₄⟩ | ⟨x₁, y₁, y₂, h₁, h₂, h₃, h₄⟩ | rfl,
            {
              left,
              refine ⟨_, _, h₁, h₂, h₃⟩,
            },
            {
              right,
              left,
              refine ⟨_, _, h₁, h₂, h₃⟩,
            },
            {
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂, h₃, h₄⟩,
            },
            {
              right,
              right,
              right,
              left,
              refine ⟨_, _, _, h₁, h₂, h₃, h₄⟩,
            },
            {
              right,
              right,
              right,
              right,
              refl,
            },
          },
        },
      },
      specialize this h',
      rcases this with ⟨x₁, y₁, h₁, h₂, h₃⟩ | ⟨x₁, y₁, h₁, h₂, h₃⟩ | ⟨x₁, x₂, y₁, h₁, h₂, h₃, h₄⟩ | ⟨x₁, y₁, y₂, h₁, h₂, h₃, h₄⟩ | h₁,
      {
        cases h₁,
        cases h₂,
        apply h₃,
      },
      {
        contradiction,
      },
      {
        contradiction,
      },
      {
        contradiction,
      },
      {
        contradiction,
      },
    },
  },
  {
    rintros ⟨Z, f, g, h⟩,
    simp_rw h,
    intros x₁ x₂ y₁ y₂ h₁ h₂ h₃,
    rw [h₁, ← h₂, h₃],
  },
end