-- Mathlib/ModelTheory/Fraisse.lean
theorem age_directLimit {ι : Type w} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (G : ι → Type max w w') [∀ i, L.Structure (G i)] (f : ∀ i j, i ≤ j → G i ↪[L] G j)
    [DirectedSystem G fun i j h => f i j h] : L.age (DirectLimit G f) = ⋃ i : ι, L.age (G i)

Proof state:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ x ∈ ↑(DirectLimit.of L ι G f i).toHom.range

Tactic:
refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩

Result:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (DirectLimit.of L ι G f i).toHom ((f (out x).fst i ⋯) (out x).snd) = x

Proof state:
case h.mp.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
⊢ ∃ i, M ∈ L.age (G i)

Tactic:
obtain ⟨s, hs⟩ := Mfg.range e.toHom

Result:
case h.mp.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
⊢ ∃ i, M ∈ L.age (G i)

Proof state:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ ↑s ⊆ ↑(DirectLimit.of L ι G f i).toHom.range

Tactic:
intro x hx

Result:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ x ∈ ↑(DirectLimit.of L ι G f i).toHom.range

Proof state:
case h
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) ↔ M ∈ ⋃ i, L.age (G i)

Tactic:
simp only [mem_iUnion]

Result:
case h
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) ↔ ∃ i, M ∈ L.age (G i)

Proof state:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (DirectLimit.of L ι G f i).toHom ((f (out x).fst i ⋯) (out x).snd) = x

Tactic:
rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
  DirectLimit.equiv_iff G f _ (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
  DirectedSystem.map_self]

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
⊢ ∃ i, M ∈ L.age (G i)

Tactic:
have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding

Result:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ ∃ i, M ∈ L.age (G i)