-- Module: Mathlib.ModelTheory.Fraisse
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)))
h₄ 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)))).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 ⋯ : (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))
⊢ (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

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]

Premises used: le_refl, Quotient.mk_eq_iff_out, FirstOrder.Language.DirectedSystem.map_self, FirstOrder.Language.DirectLimit.equiv_iff, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.DirectLimit.of_apply