-- 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
⊢ (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₃ : Eq (α :=
  G
    ((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)))
  ((f
          ((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))
          ((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 (Structure.Sigma.mk f i ((f (out x).fst i sorry : (a : G (out x).fst) → G i) (out x).snd)).fst) →
          G (Structure.Sigma.mk f i ((f (out x).fst i sorry : (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 sorry : (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 sorry : (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 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)) :
    G
      ((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)))
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]