[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
h : Countable M
⊢ Set.Countable (Quotient.mk' '' age L M)
[PROOFSTEP]
classical
refine'
  (congr_arg _ (Set.ext <| forall_quotient_iff.2 fun N => _)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
constructor
· rintro ⟨s, hs⟩
  use Bundled.of (closure L (s : Set M))
  exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
· simp only [mem_range, Quotient.eq]
  rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
  have : P ≈ N := by apply Quotient.eq'.mp; rw [hP2];
    rfl
      -- Porting note: added
  refine' ⟨s.image PM, Setoid.trans (b := P) _ this⟩
  rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
  exact ⟨PM.equivRange.symm⟩
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
h : Countable M
⊢ Set.Countable (Quotient.mk' '' age L M)
[PROOFSTEP]
refine'
  (congr_arg _ (Set.ext <| forall_quotient_iff.2 fun N => _)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N : Bundled (Structure L)
⊢ (Quotient.mk equivSetoid N ∈
      range fun s => Quotient.mk equivSetoid (Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑s })) ↔
    Quotient.mk equivSetoid N ∈ Quotient.mk' '' age L M
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N : Bundled (Structure L)
⊢ (Quotient.mk equivSetoid N ∈
      range fun s => Quotient.mk equivSetoid (Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑s })) →
    Quotient.mk equivSetoid N ∈ Quotient.mk' '' age L M
[PROOFSTEP]
rintro ⟨s, hs⟩
[GOAL]
case mp.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N : Bundled (Structure L)
s : Finset M
hs :
  (fun s => Quotient.mk equivSetoid (Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑s })) s =
    Quotient.mk equivSetoid N
⊢ Quotient.mk equivSetoid N ∈ Quotient.mk' '' age L M
[PROOFSTEP]
use Bundled.of (closure L (s : Set M))
[GOAL]
case h
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N : Bundled (Structure L)
s : Finset M
hs :
  (fun s => Quotient.mk equivSetoid (Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑s })) s =
    Quotient.mk equivSetoid N
⊢ Bundled.of { x // x ∈ LowerAdjoint.toFun (closure L) ↑s } ∈ age L M ∧
    Quotient.mk' (Bundled.of { x // x ∈ LowerAdjoint.toFun (closure L) ↑s }) = Quotient.mk equivSetoid N
[PROOFSTEP]
exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
[GOAL]
case mpr
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N : Bundled (Structure L)
⊢ Quotient.mk equivSetoid N ∈ Quotient.mk' '' age L M →
    Quotient.mk equivSetoid N ∈
      range fun s => Quotient.mk equivSetoid (Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑s })
[PROOFSTEP]
simp only [mem_range, Quotient.eq]
[GOAL]
case mpr
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N : Bundled (Structure L)
⊢ Quotient.mk equivSetoid N ∈ Quotient.mk' '' age L M →
    ∃ y, Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑y } ≈ N
[PROOFSTEP]
rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
[GOAL]
case mpr.intro.intro.intro.mk.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
⊢ ∃ y, Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑y } ≈ N
[PROOFSTEP]
have : P ≈ N := by apply Quotient.eq'.mp; rw [hP2];
  rfl
    -- Porting note: added
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
⊢ P ≈ N
[PROOFSTEP]
apply Quotient.eq'.mp
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
⊢ Quotient.mk' P = Quotient.mk' N
[PROOFSTEP]
rw [hP2]
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
⊢ Quotient.mk equivSetoid N = Quotient.mk' N
[PROOFSTEP]
rfl
  -- Porting note: added
[GOAL]
case mpr.intro.intro.intro.mk.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
this : P ≈ N
⊢ ∃ y, Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑y } ≈ N
[PROOFSTEP]
refine' ⟨s.image PM, Setoid.trans (b := P) _ this⟩
[GOAL]
case mpr.intro.intro.intro.mk.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
this : P ≈ N
⊢ Bundled.mk { x // x ∈ LowerAdjoint.toFun (closure L) ↑(Finset.image (↑PM) s) } ≈ P
[PROOFSTEP]
rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
[GOAL]
case mpr.intro.intro.intro.mk.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : Countable M
N P : Bundled (Structure L)
hP2 : Quotient.mk' P = Quotient.mk equivSetoid N
s : Finset ↑P
hs : LowerAdjoint.toFun (closure L) ↑s = ⊤
PM : ↑P ↪[L] M
this : P ≈ N
⊢ Bundled.mk { x // x ∈ Hom.range (Embedding.toHom PM) } ≈ P
[PROOFSTEP]
exact ⟨PM.equivRange.symm⟩
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝⁶ : Structure L M
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
⊢ age L (DirectLimit G f) = ⋃ (i : ι), age L (G i)
[PROOFSTEP]
classical
ext M
simp only [mem_iUnion]
constructor
· rintro ⟨Mfg, ⟨e⟩⟩
  obtain ⟨s, hs⟩ := Mfg.range e.toHom
  let out := @Quotient.out _ (DirectLimit.setoid G f)
  obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
  have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
  refine' ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion _).comp e.equivRange.toEmbedding)⟩⟩
  rw [← hs, closure_le]
  intro x hx
  refine' ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, _⟩
  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]
  rfl
· rintro ⟨i, Mfg, ⟨e⟩⟩
  exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝⁶ : Structure L M
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
⊢ age L (DirectLimit G f) = ⋃ (i : ι), age L (G i)
[PROOFSTEP]
ext M
[GOAL]
case h
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
⊢ M ∈ age L (DirectLimit G f) ↔ M ∈ ⋃ (i : ι), age L (G i)
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
case h
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
⊢ M ∈ age L (DirectLimit G f) ↔ ∃ i, M ∈ age L (G i)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
⊢ M ∈ age L (DirectLimit G f) → ∃ i, M ∈ age L (G i)
[PROOFSTEP]
rintro ⟨Mfg, ⟨e⟩⟩
[GOAL]
case h.mp.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
⊢ ∃ i, M ∈ age L (G i)
[PROOFSTEP]
obtain ⟨s, hs⟩ := Mfg.range e.toHom
[GOAL]
case h.mp.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
⊢ ∃ i, M ∈ age L (G i)
[PROOFSTEP]
let out := @Quotient.out _ (DirectLimit.setoid G f)
[GOAL]
case h.mp.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
⊢ ∃ i, M ∈ age L (G i)
[PROOFSTEP]
obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
[GOAL]
case h.mp.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
⊢ ∃ i, M ∈ age L (G i)
[PROOFSTEP]
have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
[GOAL]
case h.mp.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
⊢ ∃ i, M ∈ age L (G i)
[PROOFSTEP]
refine' ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion _).comp e.equivRange.toEmbedding)⟩⟩
[GOAL]
case h.mp.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
⊢ Hom.range (Embedding.toHom e) ≤ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))
[PROOFSTEP]
rw [← hs, closure_le]
[GOAL]
case h.mp.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
⊢ ↑s ⊆ ↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)))
[PROOFSTEP]
intro x hx
[GOAL]
case h.mp.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ x ∈ ↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)))
[PROOFSTEP]
refine' ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, _⟩
[GOAL]
case h.mp.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ ↑(Embedding.toHom (DirectLimit.of L ι G f i)) (↑(f (out x).fst i (_ : (out x).fst ≤ i)) (out x).snd) = x
[PROOFSTEP]
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]
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (Structure.Sigma.mk f i (↑(f (out x).fst i (_ : (out x).fst ≤ i)) (out x).snd)).fst ≤ i
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (closure L) ↑s = Hom.range (Embedding.toHom e)
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ Finset.image (Sigma.fst ∘ out) s → i_1 ≤ i
e' : { x // x ∈ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i)) } ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (Structure.Sigma.mk f i (↑(f (out x).fst i (_ : (out x).fst ≤ i)) (out x).snd)).fst ≤ i
[PROOFSTEP]
rfl
[GOAL]
case h.mpr
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
⊢ (∃ i, M ∈ age L (G i)) → M ∈ age L (DirectLimit G f)
[PROOFSTEP]
rintro ⟨i, Mfg, ⟨e⟩⟩
[GOAL]
case h.mpr.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M✝ : Type w
inst✝⁶ : Structure L M✝
N : Type w
inst✝⁵ : Structure L N
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → Structure L (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 (Structure L)
i : ι
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] G i
⊢ M ∈ age L (DirectLimit G f)
[PROOFSTEP]
exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
obtain ⟨F, hF⟩ := hc.exists_eq_range (hn.image _)
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : Quotient.mk' '' K = range F
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
simp only [Set.ext_iff, forall_quotient_iff, mem_image, mem_range, Quotient.eq'] at hF 
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF :
  ∀ (a : Bundled (Structure L)),
    (∃ x, x ∈ K ∧ Quotient.mk' x = Quotient.mk equivSetoid a) ↔ ∃ y, F y = Quotient.mk equivSetoid a
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
simp_rw [Quotient.eq_mk_iff_out] at hF 
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
have hF' : ∀ n : ℕ, (F n).out ∈ K := by
  intro n
  obtain ⟨P, hP1, hP2⟩ :=
    (hF (F n).out).2
      ⟨n, Setoid.refl _⟩
        -- Porting note: fix hP2 because `Quotient.out (Quotient.mk' x) ≈ a` was not simplified
            -- to `x ≈ a` in hF
  replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
  exact (h _ _ hP2).1 hP1
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
⊢ ∀ (n : ℕ), Quotient.out (F n) ∈ K
[PROOFSTEP]
intro n
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
n : ℕ
⊢ Quotient.out (F n) ∈ K
[PROOFSTEP]
obtain ⟨P, hP1, hP2⟩ :=
  (hF (F n).out).2
    ⟨n, Setoid.refl _⟩
      -- Porting note: fix hP2 because `Quotient.out (Quotient.mk' x) ≈ a` was not simplified
          -- to `x ≈ a` in hF
[GOAL]
case intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
n : ℕ
P : Bundled (Structure L)
hP1 : P ∈ K
hP2 : Quotient.out (Quotient.mk' P) ≈ Quotient.out (F n)
⊢ Quotient.out (F n) ∈ K
[PROOFSTEP]
replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
[GOAL]
case intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
n : ℕ
P : Bundled (Structure L)
hP1 : P ∈ K
hP2 : P ≈ Quotient.out (F n)
⊢ Quotient.out (F n) ∈ K
[PROOFSTEP]
exact (h _ _ hP2).1 hP1
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
choose P hPK hP hFP using fun (N : K) (n : ℕ) => jep N N.2 (F (n + 1)).out (hF' _)
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
let G : ℕ → K :=
  @Nat.rec (fun _ => K) ⟨(F 0).out, hF' 0⟩ fun n N =>
    ⟨P N n, hPK N n⟩
      -- Poting note: was
        -- let f : ∀ i j, i ≤ j → G i ↪[L] G j := DirectedSystem.natLeRec fun n => (hP _ n).some
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
let f : ∀ (i j : ℕ), i ≤ j → (G i).val ↪[L] (G j).val :=
  by
  refine DirectedSystem.natLERec (G' := fun i => (G i).val) (L := L) ?_
  dsimp only
  exact (fun n => (hP _ n).some)
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
⊢ (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j)
[PROOFSTEP]
refine DirectedSystem.natLERec (G' := fun i => (G i).val) (L := L) ?_
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
⊢ (n : ℕ) → (fun i => ↑↑(G i)) n ↪[L] (fun i => ↑↑(G i)) (n + 1)
[PROOFSTEP]
dsimp only
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
⊢ (n : ℕ) →
    ↑↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
            (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n) ↪[L]
      ↑↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
            (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) (n + 1))
[PROOFSTEP]
exact (fun n => (hP _ n).some)
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
have : DirectedSystem (fun n ↦ (G n).val) fun i j h ↦ ↑(f i j h) := by dsimp; infer_instance
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
⊢ DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
[PROOFSTEP]
dsimp
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
⊢ DirectedSystem
    (fun n =>
      ↑↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
            (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
    fun i j h =>
    ↑(DirectedSystem.natLERec
        (fun n =>
          Nonempty.some
            (_ :
              (fun M N => Nonempty (↑M ↪[L] ↑N))
                (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                    (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
                (P
                  (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                    (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
                  n)))
        i j h)
[PROOFSTEP]
infer_instance
[GOAL]
case intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
⊢ ∃ M, Structure.CG L ↑M ∧ age L ↑M = K
[PROOFSTEP]
refine ⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩
[GOAL]
case intro.refine_1
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
⊢ Structure.CG L ↑(Bundled.of (DirectLimit (fun n => ↑↑(G n)) f))
[PROOFSTEP]
exact DirectLimit.cg _ (fun n => (fg _ (G n).2).cg)
[GOAL]
case intro.refine_2
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
⊢ age L ↑(Bundled.of (DirectLimit (fun n => ↑↑(G n)) f)) = K
[PROOFSTEP]
refine
  (age_directLimit (fun n ↦ (G n).val) f).trans
    (subset_antisymm (iUnion_subset fun n N hN => hp (G n).val (G n).2 hN) fun N KN => ?_)
[GOAL]
case intro.refine_2
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
⊢ N ∈ ⋃ (i : ℕ), age L ↑↑(G i)
[PROOFSTEP]
have : Quotient.out (Quotient.mk' N) ≈ N := Quotient.eq_mk_iff_out.mp rfl
[GOAL]
case intro.refine_2
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
⊢ N ∈ ⋃ (i : ℕ), age L ↑↑(G i)
[PROOFSTEP]
obtain ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, this⟩
[GOAL]
case intro.refine_2.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
n : ℕ
e : ↑(Quotient.out (F n)) ≃[L] ↑N
⊢ N ∈ ⋃ (i : ℕ), age L ↑↑(G i)
[PROOFSTEP]
refine mem_iUnion_of_mem n ⟨fg _ KN, ⟨Embedding.comp ?_ e.symm.toEmbedding⟩⟩
[GOAL]
case intro.refine_2.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
n : ℕ
e : ↑(Quotient.out (F n)) ≃[L] ↑N
⊢ ↑(Quotient.out (F n)) ↪[L] ↑↑(G n)
[PROOFSTEP]
cases' n with n
[GOAL]
case intro.refine_2.intro.intro.zero
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
e : ↑(Quotient.out (F Nat.zero)) ≃[L] ↑N
⊢ ↑(Quotient.out (F Nat.zero)) ↪[L] ↑↑(G Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case intro.refine_2.intro.intro.zero
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
e : ↑(Quotient.out (F Nat.zero)) ≃[L] ↑N
⊢ ↑(Quotient.out (F 0)) ↪[L] ↑(Quotient.out (F 0))
[PROOFSTEP]
exact Embedding.refl _ _
[GOAL]
case intro.refine_2.intro.intro.succ
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
n : ℕ
e : ↑(Quotient.out (F (Nat.succ n))) ≃[L] ↑N
⊢ ↑(Quotient.out (F (Nat.succ n))) ↪[L] ↑↑(G (Nat.succ n))
[PROOFSTEP]
dsimp
[GOAL]
case intro.refine_2.intro.intro.succ
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
hn : Set.Nonempty K
h : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
hc : Set.Countable (Quotient.mk' '' K)
fg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled (Structure L)), (∃ x, x ∈ K ∧ Quotient.out (Quotient.mk' x) ≈ a) ↔ ∃ y, Quotient.out (F y) ≈ a
hF' : ∀ (n : ℕ), Quotient.out (F n) ∈ K
P : ↑K → ℕ → Bundled (Structure L)
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N => Nonempty (↑M ↪[L] ↑N)) (Quotient.out (F (n + 1))) (P N n)
G : ℕ → ↑K :=
  Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) } fun n N =>
    { val := P N n, property := (_ : P N n ∈ K) }
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) :=
  DirectedSystem.natLERec
    (id fun n =>
      Nonempty.some
        (_ :
          (fun M N => Nonempty (↑M ↪[L] ↑N))
            (↑(Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n))
            (P
              (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
                (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
              n)))
this✝ : DirectedSystem (fun n => ↑↑(G n)) fun i j h => ↑(f i j h)
N : Bundled (Structure L)
KN : N ∈ K
this : Quotient.out (Quotient.mk' N) ≈ N
n : ℕ
e : ↑(Quotient.out (F (Nat.succ n))) ≃[L] ↑N
⊢ ↑(Quotient.out (F (Nat.succ n))) ↪[L]
    ↑(P
        (Nat.rec { val := Quotient.out (F 0), property := (_ : Quotient.out (F 0) ∈ K) }
          (fun n N => { val := P N n, property := (_ : P N n ∈ K) }) n)
        n)
[PROOFSTEP]
exact (hFP _ n).some
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝² : Structure L M
N : Type w
inst✝¹ : Structure L N
inst✝ : Countable ((l : ℕ) × Functions L l)
⊢ (∃ M, Countable ↑M ∧ age L ↑M = K) ↔
    Set.Nonempty K ∧
      (∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        Set.Countable (Quotient.mk' '' K) ∧
          (∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝² : Structure L M
N : Type w
inst✝¹ : Structure L N
inst✝ : Countable ((l : ℕ) × Functions L l)
⊢ (∃ M, Countable ↑M ∧ age L ↑M = K) →
    Set.Nonempty K ∧
      (∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        Set.Countable (Quotient.mk' '' K) ∧
          (∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K
[PROOFSTEP]
rintro ⟨M, h1, h2, rfl⟩
[GOAL]
case mp.intro.intro.refl
L : Language
M✝ : Type w
inst✝² : Structure L M✝
N : Type w
inst✝¹ : Structure L N
inst✝ : Countable ((l : ℕ) × Functions L l)
M : Bundled (Structure L)
h1 : Countable ↑M
⊢ Set.Nonempty (age L ↑M) ∧
    (∀ (M_1 N : Bundled (Structure L)), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ age L ↑M ↔ N ∈ age L ↑M)) ∧
      Set.Countable (Quotient.mk' '' age L ↑M) ∧
        (∀ (M_1 : Bundled (Structure L)), M_1 ∈ age L ↑M → Structure.FG L ↑M_1) ∧
          Hereditary (age L ↑M) ∧ JointEmbedding (age L ↑M)
[PROOFSTEP]
refine'
  ⟨age.nonempty M, age.is_equiv_invariant L M, age.countable_quotient M, fun N hN => hN.1, age.hereditary M,
    age.jointEmbedding M⟩
[GOAL]
case mpr
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝² : Structure L M
N : Type w
inst✝¹ : Structure L N
inst✝ : Countable ((l : ℕ) × Functions L l)
⊢ Set.Nonempty K ∧
      (∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        Set.Countable (Quotient.mk' '' K) ∧
          (∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K →
    ∃ M, Countable ↑M ∧ age L ↑M = K
[PROOFSTEP]
rintro ⟨Kn, eqinv, cq, hfg, hp, jep⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝² : Structure L M
N : Type w
inst✝¹ : Structure L N
inst✝ : Countable ((l : ℕ) × Functions L l)
Kn : Set.Nonempty K
eqinv : ∀ (M N : Bundled (Structure L)), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
cq : Set.Countable (Quotient.mk' '' K)
hfg : ∀ (M : Bundled (Structure L)), M ∈ K → Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Countable ↑M ∧ age L ↑M = K
[PROOFSTEP]
obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn eqinv cq hfg hp jep
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro
L : Language
M✝ : Type w
inst✝² : Structure L M✝
N : Type w
inst✝¹ : Structure L N
inst✝ : Countable ((l : ℕ) × Functions L l)
M : Bundled (Structure L)
hM : Structure.CG L ↑M
Kn : Set.Nonempty (age L ↑M)
eqinv : ∀ (M_1 N : Bundled (Structure L)), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ age L ↑M ↔ N ∈ age L ↑M)
cq : Set.Countable (Quotient.mk' '' age L ↑M)
hfg : ∀ (M_1 : Bundled (Structure L)), M_1 ∈ age L ↑M → Structure.FG L ↑M_1
hp : Hereditary (age L ↑M)
jep : JointEmbedding (age L ↑M)
⊢ ∃ M_1, Countable ↑M_1 ∧ age L ↑M_1 = age L ↑M
[PROOFSTEP]
exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩
[GOAL]
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N : Type w
inst✝ : Structure L N
h : IsUltrahomogeneous L M
⊢ Amalgamation (age L M)
[PROOFSTEP]
rintro N P Q NP NQ ⟨Nfg, ⟨-⟩⟩ ⟨Pfg, ⟨PM⟩⟩ ⟨Qfg, ⟨QM⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
⊢ ∃ Q_1 NQ_1 PQ, Q_1 ∈ age L M ∧ Embedding.comp NQ_1 NP = Embedding.comp PQ NQ
[PROOFSTEP]
obtain ⟨g, hg⟩ := h (PM.comp NP).toHom.range (Nfg.range _) ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
⊢ ∃ Q_1 NQ_1 PQ, Q_1 ∈ age L M ∧ Embedding.comp NQ_1 NP = Embedding.comp PQ NQ
[PROOFSTEP]
let s := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
⊢ ∃ Q_1 NQ_1 PQ, Q_1 ∈ age L M ∧ Embedding.comp NQ_1 NP = Embedding.comp PQ NQ
[PROOFSTEP]
refine'
  ⟨Bundled.of s, Embedding.comp (Substructure.inclusion le_sup_left) (g.toEmbedding.comp PM).equivRange.toEmbedding,
    Embedding.comp (Substructure.inclusion le_sup_right) QM.equivRange.toEmbedding,
    ⟨(fg_iff_structure_fg _).1 (FG.sup (Pfg.range _) (Qfg.range _)), ⟨Substructure.subtype _⟩⟩, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
⊢ Embedding.comp
      (Embedding.comp
        (Substructure.inclusion
          (_ :
            Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
              Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
        (Equiv.toEmbedding (Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM))))
      NP =
    Embedding.comp
      (Embedding.comp
        (Substructure.inclusion
          (_ :
            Hom.range (Embedding.toHom QM) ≤
              Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
        (Equiv.toEmbedding (Embedding.equivRange QM)))
      NQ
[PROOFSTEP]
ext n
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.h
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
n : ↑N
⊢ ↑(Embedding.comp
          (Embedding.comp
            (Substructure.inclusion
              (_ :
                Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
                  Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
            (Equiv.toEmbedding (Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM))))
          NP)
      n =
    ↑(Embedding.comp
          (Embedding.comp
            (Substructure.inclusion
              (_ :
                Hom.range (Embedding.toHom QM) ≤
                  Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
            (Equiv.toEmbedding (Embedding.equivRange QM)))
          NQ)
      n
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
n : ↑N
⊢ ↑(↑(Embedding.comp
            (Embedding.comp
              (Substructure.inclusion
                (_ :
                  Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
                    Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
              (Equiv.toEmbedding (Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM))))
            NP)
        n) =
    ↑(↑(Embedding.comp
            (Embedding.comp
              (Substructure.inclusion
                (_ :
                  Hom.range (Embedding.toHom QM) ≤
                    Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
              (Equiv.toEmbedding (Embedding.equivRange QM)))
            NQ)
        n)
[PROOFSTEP]
have hgn := (Embedding.ext_iff.1 hg) ((PM.comp NP).equivRange n)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
n : ↑N
hgn :
  ↑(Embedding.comp (Embedding.comp QM NQ)
          (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))))
      (↑(Embedding.equivRange (Embedding.comp PM NP)) n) =
    ↑(Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP)))))
      (↑(Embedding.equivRange (Embedding.comp PM NP)) n)
⊢ ↑(↑(Embedding.comp
            (Embedding.comp
              (Substructure.inclusion
                (_ :
                  Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
                    Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
              (Equiv.toEmbedding (Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM))))
            NP)
        n) =
    ↑(↑(Embedding.comp
            (Embedding.comp
              (Substructure.inclusion
                (_ :
                  Hom.range (Embedding.toHom QM) ≤
                    Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
              (Equiv.toEmbedding (Embedding.equivRange QM)))
            NQ)
        n)
[PROOFSTEP]
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.symm_apply_apply, Substructure.coeSubtype,
  Embedding.equivRange_apply] at hgn 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
n : ↑N
hgn : ↑QM (↑NQ n) = ↑g (↑PM (↑NP n))
⊢ ↑(↑(Embedding.comp
            (Embedding.comp
              (Substructure.inclusion
                (_ :
                  Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
                    Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
              (Equiv.toEmbedding (Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM))))
            NP)
        n) =
    ↑(↑(Embedding.comp
            (Embedding.comp
              (Substructure.inclusion
                (_ :
                  Hom.range (Embedding.toHom QM) ≤
                    Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
              (Equiv.toEmbedding (Embedding.equivRange QM)))
            NQ)
        n)
[PROOFSTEP]
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
n : ↑N
hgn : ↑QM (↑NQ n) = ↑g (↑PM (↑NP n))
⊢ ↑(↑(Substructure.inclusion
            (_ :
              Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
                Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
        (↑(Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM)) (↑NP n))) =
    ↑(↑(Substructure.inclusion
            (_ :
              Hom.range (Embedding.toHom QM) ≤
                Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)))
        (↑(Embedding.equivRange QM) (↑NQ n)))
[PROOFSTEP]
erw [Substructure.coe_inclusion, Substructure.coe_inclusion]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
K : Set (Bundled (Structure L))
M : Type w
inst✝¹ : Structure L M
N✝ : Type w
inst✝ : Structure L N✝
h : IsUltrahomogeneous L M
N P Q : Bundled (Structure L)
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg :
  Embedding.comp (Embedding.comp QM NQ) (Equiv.toEmbedding (Equiv.symm (Embedding.equivRange (Embedding.comp PM NP)))) =
    Embedding.comp (Equiv.toEmbedding g) (subtype (Hom.range (Embedding.toHom (Embedding.comp PM NP))))
s : Substructure L M := Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM)
n : ↑N
hgn : ↑QM (↑NQ n) = ↑g (↑PM (↑NP n))
⊢ ↑(Set.inclusion
        (_ :
          Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ≤
            Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM))
        (↑(Embedding.equivRange (Embedding.comp (Equiv.toEmbedding g) PM)) (↑NP n))) =
    ↑(Set.inclusion
        (_ :
          Hom.range (Embedding.toHom QM) ≤
            Hom.range (Hom.comp (Equiv.toHom g) (Embedding.toHom PM)) ⊔ Hom.range (Embedding.toHom QM))
        (↑(Embedding.equivRange QM) (↑NQ n)))
[PROOFSTEP]
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Set.coe_inclusion, Embedding.equivRange_apply, hgn]
