-- Mathlib/ModelTheory/Fraisse.lean
theorem age.countable_quotient [h : Countable M] : (Quotient.mk' '' L.age M).Countable

Proof state:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ⟦N⟧ ∈ range fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧

Tactic:
simp only [mem_range, Quotient.eq]

Result:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ∃ y, equivSetoid { α := ↥((closure L).toFun ↑y), str := inferInstance } N

Proof state:
case mpr.intro.intro.intro.mk.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ ∃ y, equivSetoid { α := ↥((closure L).toFun ↑y), str := inferInstance } N

Tactic:
refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩

Result:
case mpr.intro.intro.intro.mk.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥((closure L).toFun ↑(Finset.image (⇑PM) s)), str := inferInstance } ≈ P

Proof state:
case mpr.intro.intro.intro.mk.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥PM.toHom.range, str := inferInstance } ≈ P

Tactic:
exact ⟨PM.equivRange.symm⟩

Result:
no goals

Proof state:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ∃ y, equivSetoid { α := ↥((closure L).toFun ↑y), str := inferInstance } N

Tactic:
rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩

Result:
case mpr.intro.intro.intro.mk.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ ∃ y, equivSetoid { α := ↥((closure L).toFun ↑y), str := inferInstance } N

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ (⟦N⟧ ∈ range fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) ↔ ⟦N⟧ ∈ Quotient.mk' '' L.age M

Tactic:
constructor

Result:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ (⟦N⟧ ∈ range fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) → ⟦N⟧ ∈ Quotient.mk' '' L.age M

case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ⟦N⟧ ∈ range fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧

Proof state:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ (⟦N⟧ ∈ range fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) → ⟦N⟧ ∈ Quotient.mk' '' L.age M

Tactic:
rintro ⟨s, hs⟩

Result:
case mp.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs : (fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) s = ⟦N⟧
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M

Proof state:
case mp.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs : (fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) s = ⟦N⟧
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M

Tactic:
use Bundled.of (closure L (s : Set M))

Result:
case h
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs : (fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) s = ⟦N⟧
⊢ Bundled.of ↥((closure L).toFun ↑s) ∈ L.age M ∧ Quotient.mk' (Bundled.of ↥((closure L).toFun ↑s)) = ⟦N⟧

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
⊢ (Quotient.mk' '' L.age M).Countable

Tactic:
refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
  (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ (⟦N⟧ ∈ range fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) ↔ ⟦N⟧ ∈ Quotient.mk' '' L.age M

Proof state:
case mpr.intro.intro.intro.mk.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥((closure L).toFun ↑(Finset.image (⇑PM) s)), str := inferInstance } ≈ P

Tactic:
rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]

Result:
case mpr.intro.intro.intro.mk.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥PM.toHom.range, str := inferInstance } ≈ P

Proof state:
case h
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs : (fun s => ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧) s = ⟦N⟧
⊢ Bundled.of ↥((closure L).toFun ↑s) ∈ L.age M ∧ Quotient.mk' (Bundled.of ↥((closure L).toFun ↑s)) = ⟦N⟧

Tactic:
exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩

Result:
no goals