-- Module: Mathlib.Order.DirectedInverseSystem
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_6 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_7 : IsDirectedOrder ι
x y z : (i : ι) × F i
h :
  ∃ (i : ι) (hx : x.fst (β := fun (i : ι) ↦ F i) ≤ i) (hy : y.fst (β := fun (i : ι) ↦ F i) ≤ i),
    Eq (α := F i)
      ((f (x.fst (β := fun (i : ι) ↦ F i)) i hx : (a : F x.fst) → F i) (x.snd (β := fun (i : ι) ↦ F i)) : F i)
      ((f (y.fst (β := fun (i : ι) ↦ F i)) i hy : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
h_1 :
  ∃ (i : ι) (hx : y.fst (β := fun (i : ι) ↦ F i) ≤ i) (hy : z.fst (β := fun (i : ι) ↦ F i) ≤ i),
    Eq (α := F i)
      ((f (y.fst (β := fun (i : ι) ↦ F i)) i hx : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
      ((f (z.fst (β := fun (i : ι) ↦ F i)) i hy : (a : F z.fst) → F i) (z.snd (β := fun (i : ι) ↦ F i)) : F i)
j : ι
hx : x.fst (β := fun (i : ι) ↦ F i) ≤ j
w : y.fst (β := fun (i : ι) ↦ F i) ≤ j
jeq :
  Eq (α := F j) ((f (x.fst (β := fun (i : ι) ↦ F i)) j hx : (a : F x.fst) → F j) (x.snd (β := fun (i : ι) ↦ F i)) : F j)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) j w : (a : F y.fst) → F j) (y.snd (β := fun (i : ι) ↦ F i)) : F j)
k : ι
w_1 : y.fst (β := fun (i : ι) ↦ F i) ≤ k
hz : z.fst (β := fun (i : ι) ↦ F i) ≤ k
keq :
  Eq (α := F k)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) k w_1 : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k)
    ((f (z.fst (β := fun (i : ι) ↦ F i)) k hz : (a : F z.fst) → F k) (z.snd (β := fun (i : ι) ↦ F i)) : F k)
i : ι
hji : j ≤ i
hki : k ≤ i
rw :
  Eq (α := F i)
    ((f j i hji : (a : F j) → F i)
        ((f (x.fst (β := fun (i : ι) ↦ F i)) j hx : (a : F x.fst) → F j) (x.snd (β := fun (i : ι) ↦ F i)) : F j) :
      F i)
    ((f (z.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F z.fst) → F i) (z.snd (β := fun (i : ι) ↦ F i)) : F i)
rw₁ :
  Eq (α := F i)
    ((f j i hji : (a : F j) → F i)
        ((f (x.fst (β := fun (i : ι) ↦ F i)) j hx : (a : F x.fst) → F j) (x.snd (β := fun (i : ι) ↦ F i)) : F j) :
      F i)
    ((f k i hki : (a : F k) → F i)
        ((f (z.fst (β := fun (i : ι) ↦ F i)) k hz : (a : F z.fst) → F k) (z.snd (β := fun (i : ι) ↦ F i)) : F k) :
      F i)
rw₂ :
  Eq (α := F i)
    ((f j i hji : (a : F j) → F i)
        ((f (y.fst (β := fun (i : ι) ↦ F i)) j w : (a : F y.fst) → F j) (y.snd (β := fun (i : ι) ↦ F i)) : F j) :
      F i)
    ((f k i hki : (a : F k) → F i)
        ((f (z.fst (β := fun (i : ι) ↦ F i)) k hz : (a : F z.fst) → F k) (z.snd (β := fun (i : ι) ↦ F i)) : F k) :
      F i)
rw₃ :
  Eq (α := F i)
    ((f j i hji : (a : F j) → F i)
        ((f (y.fst (β := fun (i : ι) ↦ F i)) j w : (a : F y.fst) → F j) (y.snd (β := fun (i : ι) ↦ F i)) : F j) :
      F i)
    ((f k i hki : (a : F k) → F i)
        ((f (y.fst (β := fun (i : ι) ↦ F i)) k w_1 : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k) :
      F i)
rw₄ :
  Eq (α := F i) ((f (y.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
    ((f k i hki : (a : F k) → F i)
        ((f (y.fst (β := fun (i : ι) ↦ F i)) k w_1 : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k) :
      F i)
rw₅ rw₆ :
  Eq (α := F i) ((f (y.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
⊢ Eq (α := F i) ((f (x.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F x.fst) → F i) (x.snd (β := fun (i : ι) ↦ F i)) : F i)
    ((f (z.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F z.fst) → F i) (z.snd (β := fun (i : ι) ↦ F i)) : F i)

Tactic:
rw [← map_map' _ hx hji, ← map_map' _ hz hki, jeq, ← keq, map_map', map_map']

Premises used: DirectedSystem.map_map'