-- Mathlib/ModelTheory/Fraisse.lean
theorem isFraisseLimit_of_countable_infinite
    (M : Type*) [Countable M] [Infinite M] [Language.empty.Structure M] :
    IsFraisseLimit { S : Bundled Language.empty.Structure | Finite S } M where
  age

Proof state:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
⊢ S ∈ Language.empty.age M ↔ S ∈ {S | Finite ↑S}

Tactic:
simp only [age, Structure.fg_iff_finite, mem_setOf_eq, and_iff_left_iff_imp]

Result:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
⊢ Finite ↑S → Nonempty (↑S ↪[Language.empty] M)

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝¹ : Finite ↥S
this✝ : Infinite { x // x ∉ S }
this : Finite ↥f.toHom.range
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
have : Infinite { x // x ∉ f.toHom.range } := ((Set.toFinite _).infinite_compl ).to_subtype

Result:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Proof state:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
⊢ Finite ↑S → Nonempty (↑S ↪[Language.empty] M)

Tactic:
intro hS

Result:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
hS : Finite ↑S
⊢ Nonempty (↑S ↪[Language.empty] M)

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩

Result:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ f = (StrongHomClass.toEquiv (f.equivRange.subtypeCongr ⋯.some)).toEmbedding.comp S.subtype

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝ : Finite ↥S
this : Infinite { x // x ∉ S }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
have : Finite f.toHom.range := (((Substructure.fg_iff_structure_fg S).1 hS).range _).finite

Result:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝¹ : Finite ↥S
this✝ : Infinite { x // x ∉ S }
this : Finite ↥f.toHom.range
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
⊢ Language.empty.age M = {S | Finite ↑S}

Tactic:
ext S

Result:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
⊢ S ∈ Language.empty.age M ↔ S ∈ {S | Finite ↑S}

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
have : Finite S := hS.finite

Result:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this : Finite ↥S
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Proof state:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
x : ↥S
⊢ f x = ((StrongHomClass.toEquiv (f.equivRange.subtypeCongr ⋯.some)).toEmbedding.comp S.subtype) x

Tactic:
simp [Equiv.subtypeCongr]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this : Finite ↥S
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype

Result:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝ : Finite ↥S
this : Infinite { x // x ∉ S }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Proof state:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
hS : Finite ↑S
⊢ Nonempty (↑S ↪[Language.empty] M)

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
classical
have : Finite S := hS.finite
have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype
have : Finite f.toHom.range := (((Substructure.fg_iff_structure_fg S).1 hS).range _).finite
have : Infinite { x // x ∉ f.toHom.range } := ((Set.toFinite _).infinite_compl ).to_subtype
refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩
ext x
simp [Equiv.subtypeCongr]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ f = (StrongHomClass.toEquiv (f.equivRange.subtypeCongr ⋯.some)).toEmbedding.comp S.subtype

Tactic:
ext x

Result:
case h
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
x : ↥S
⊢ f x = ((StrongHomClass.toEquiv (f.equivRange.subtypeCongr ⋯.some)).toEmbedding.comp S.subtype) x