-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
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 ι
C : Sort u_9
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 : (a : F₁ i) → F₁ j) x) ((f₂ i j h : (a : F₂ i) → F₂ j) y)
z : DirectLimit F₁ (T := T₁) f₁
w : DirectLimit F₂ (T := T₂) f₂
x : (i : ι) × F₁ i
x_1 : (i : ι) × F₂ i
x_2 : (i : ι) × F₁ i
x_3 : (i : ι) × F₂ i
h : x ≈ x_2
h_1 : x_1 ≈ x_3
j : ι
hx : x.fst (β := fun (i : ι) ↦ F₁ i) ≤ j
hyj : x_2.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₁ (x_2.fst (β := fun (i : ι) ↦ F₁ i)) j hyj : (a : F₁ x_2.fst) → F₁ j) (x_2.snd (β := fun (i : ι) ↦ F₁ i)) :
      F₁ j)
k : ι
hyk : x_1.fst (β := fun (i : ι) ↦ F₂ i) ≤ k
hz : x_3.fst (β := fun (i : ι) ↦ F₂ i) ≤ k
keq :
  Eq (α := F₂ k)
    ((f₂ (x_1.fst (β := fun (i : ι) ↦ F₂ i)) k hyk : (a : F₂ x_1.fst) → F₂ k) (x_1.snd (β := fun (i : ι) ↦ F₂ i)) :
      F₂ k)
    ((f₂ (x_3.fst (β := fun (i : ι) ↦ F₂ i)) k hz : (a : F₂ x_3.fst) → F₂ k) (x_3.snd (β := fun (i : ι) ↦ F₂ i)) : F₂ k)
i : ι
hji : j ≤ i
hki : k ≤ i
simp_rw simp_rw₁ :
  (↑(lift₂Aux (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat x x_1) : C) =
    (↑(lift₂Aux (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat x_2 x_3) : C)
simp_rw₂ :
  ih i ((f₁ (x.fst (β := fun (i : ι) ↦ F₁ i)) i ⋯ : (a : F₁ x.fst) → F₁ i) (x.snd (β := fun (i : ι) ↦ F₁ i)))
      ((f₂ (x_1.fst (β := fun (i : ι) ↦ F₂ i)) i ⋯ : (a : F₂ x_1.fst) → F₂ i) (x_1.snd (β := fun (i : ι) ↦ F₂ i))) =
    (↑(lift₂Aux (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat x_2 x_3) : C)
⊢ Eq.{u_9} (α :=
    (fun (x : Quotient (α := (i : ι) × F₁ i) (setoid (F := F₁) (T := T₁) f₁))
          (x_4 : Quotient (α := (i : ι) × F₂ i) (setoid (F := F₂) (T := T₂) f₂)) ↦
        C)
      ⟦x⟧ ⟦x_1⟧)
    ((fun (x1 : (i : ι) × F₁ i) (x2 : (i : ι) × F₂ i) ↦
        (↑(lift₂Aux (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat x1 x2) : C))
      x x_1)
    ((fun (x1 : (i : ι) × F₁ i) (x2 : (i : ι) × F₂ i) ↦
        (↑(lift₂Aux (F₁ := F₁) (F₂ := F₂) (T₁ := T₁) f₁ (T₂ := T₂) f₂ ih compat x1 x2) : C))
      x_2 x_3)
have simp_rw₃ : ih i ((f₁ (x.fst (β := fun (i : ι) ↦ F₁ i)) i sorry : (a : F₁ x.fst) → F₁ i) (x.snd (β := fun (i : ι) ↦ F₁ i)))
    ((f₂ (x_1.fst (β := fun (i : ι) ↦ F₂ i)) i sorry : (a : F₂ x_1.fst) → F₂ i) (x_1.snd (β := fun (i : ι) ↦ F₂ i))) =
  ih i ((f₁ (x_2.fst (β := fun (i : ι) ↦ F₁ i)) i sorry : (a : F₁ x_2.fst) → F₁ i) (x_2.snd (β := fun (i : ι) ↦ F₁ i)))
    ((f₂ (x_3.fst (β := fun (i : ι) ↦ F₂ i)) i sorry : (a : F₂ x_3.fst) → F₂ i) (x_3.snd (β := fun (i : ι) ↦ F₂ i)))
Tactic: simp_rw [(lift₂Aux ..).2 _ (hx.trans hji) (hyk.trans hki),
        (lift₂Aux ..).2 _ (hyj.trans hji) (hz.trans hki),
        ← map_map' _ hx hji, jeq, ← map_map' _ hz hki, ← keq, map_map']