∀ {ι : Type u_2} [inst : Preorder ι] {F₁ : ι → Type u_3} {F₂ : ι → Type u_5} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_4}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι] {C : Sort u_1}
  (ih : (i : ι) → F₁ i → F₂ i → C)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (x : (i : ι) × F₁ i) (x_1 : (i : ι) × F₂ i) (x_2 : (i : ι) × F₁ i) (x_3 : (i : ι) × F₂ i) (j : ι) (hx : x.fst ≤ j)
  (hyj : x_2.fst ≤ j),
  (f₁ x.fst j hx) x.snd = (f₁ x_2.fst j hyj) x_2.snd →
    ∀ (k : ι) (hyk : x_1.fst ≤ k) (hz : x_3.fst ≤ k),
      (f₂ x_1.fst k hyk) x_1.snd = (f₂ x_3.fst k hz) x_3.snd →
        (fun x1 x2 => ↑(DirectLimit.lift₂Aux✝ f₁ f₂ ih compat x1 x2)) x x_1 =
          (fun x1 x2 => ↑(DirectLimit.lift₂Aux✝¹ f₁ f₂ ih compat x1 x2)) x_2 x_3