-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
h :
  (DirectLimit.of L ι G f i : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
h₁ :
  ⟦Structure.Sigma.mk (G := G) f i
        ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
          ((out x).snd (β := fun (i : ι) ↦ G i)))⟧ =
    x
h₂ :
  Structure.Sigma.mk (G := G) f i
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) ≈
    Quotient.out x
h₃ :
  Eq (α :=
    G
      ((Structure.Sigma.mk (G := G) f i
            ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
              ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
        (β := fun (i : ι) ↦ G i)))
    ((f
            ((Structure.Sigma.mk (G := G) f i
                  ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
                    ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
              (β := fun (i : ι) ↦ G i))
            ((Structure.Sigma.mk (G := G) f i
                  ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
                    ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
              (β := fun (i : ι) ↦ G i))
            ⋯ :
          (a : G (Structure.Sigma.mk f i ((f (out x).fst i ⋯ : (a : G (out x).fst) → G i) (out x).snd)).fst) →
            G (Structure.Sigma.mk f i ((f (out x).fst i ⋯ : (a : G (out x).fst) → G i) (out x).snd)).fst)
        ((Structure.Sigma.mk (G := G) f i
              ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
                ((out x).snd (β := fun (i : ι) ↦ G i)))).snd
          (β := fun (i : ι) ↦ G i)) :
      G
        ((Structure.Sigma.mk (G := G) f i
              ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
                ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
          (β := fun (i : ι) ↦ G i)))
    ((f ((Quotient.out x).fst (β := fun (i : ι) ↦ G i))
            ((Structure.Sigma.mk (G := G) f i
                  ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
                    ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
              (β := fun (i : ι) ↦ G i))
            ⋯ :
          (a : G (Quotient.out x).fst) →
            G (Structure.Sigma.mk f i ((f (out x).fst i ⋯ : (a : G (out x).fst) → G i) (out x).snd)).fst)
        ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
      G
        ((Structure.Sigma.mk (G := G) f i
              ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
                ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
          (β := fun (i : ι) ↦ G i)))
⊢ (Embedding.toHom (DirectLimit.of L ι G f i) : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
have h₄ : (Structure.Sigma.mk (G := G) f i
        ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (out x).fst) → G i)
          ((out x).snd (β := fun (i : ι) ↦ G i)))).snd
    (β := fun (i : ι) ↦ G i) =
  (f ((Quotient.out x).fst (β := fun (i : ι) ↦ G i))
        ((Structure.Sigma.mk (G := G) f i
              ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (out x).fst) → G i)
                ((out x).snd (β := fun (i : ι) ↦ G i)))).fst
          (β := fun (i : ι) ↦ G i))
        sorry :
      (a : G (Quotient.out x).fst) →
        G (Structure.Sigma.mk f i ((f (out x).fst i sorry : (a : G (out x).fst) → G i) (out x).snd)).fst)
    ((Quotient.out x).snd (β := fun (i : ι) ↦ G i))
Tactic: rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]