-- 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.mpr
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
⊢ (∃ i, M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)

Tactic:
rintro ⟨i, Mfg, ⟨e⟩⟩

Result:
case h.mpr.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
i : ι
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] G i
⊢ M ∈ L.age (DirectLimit G f)

Proof state:
case h.mp
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)

Tactic:
rintro ⟨Mfg, ⟨e⟩⟩

Result:
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)

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
⊢ e.toHom.range ≤ (DirectLimit.of L ι G f i).toHom.range

Tactic:
rw [← hs, closure_le]

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
⊢ ↑s ⊆ ↑(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) ↔ ∃ i, M ∈ L.age (G i)

Tactic:
constructor

Result:
case h.mp
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)

case h.mpr
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
⊢ (∃ i, M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)

Proof state:
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)

Tactic:
let out := @Quotient.out _ (DirectLimit.setoid G f)

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
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
⊢ ∃ i, M ∈ L.age (G i)

Proof state:
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)
⊢ L.age (DirectLimit G f) = ⋃ i, L.age (G i)

Tactic:
ext M

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) ↔ M ∈ ⋃ i, L.age (G i)

Proof state:
case h.mpr.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
i : ι
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] G i
⊢ M ∈ L.age (DirectLimit G f)

Tactic:
exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩

Result:
no goals

Proof state:
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
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
⊢ ∃ i, M ∈ L.age (G i)

Tactic:
obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))

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
⊢ ∃ i, M ∈ L.age (G i)