-- Mathlib/ModelTheory/Fraisse.lean
theorem exists_countable_is_age_of_iff [Countable (Σ l, L.Functions l)] :
    (∃ M : Bundled.{w} L.Structure, Countable M ∧ L.age M = K) ↔
      K.Nonempty ∧ (∀ M N : Bundled.{w} L.Structure, Nonempty (M ≃[L] N) → (M ∈ K ↔ N ∈ K)) ∧
      (Quotient.mk' '' K).Countable ∧ (∀ M : Bundled.{w} L.Structure, M ∈ K → Structure.FG L M) ∧
      Hereditary K ∧ JointEmbedding K

Proof state:
case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K →
    ∃ M, Countable ↑M ∧ L.age ↑M = K

Tactic:
rintro ⟨Kn, _, cq, hfg, hp, jep⟩

Result:
case mpr.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
Kn : K.Nonempty
left✝ : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
cq : (Quotient.mk' '' K).Countable
hfg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Countable ↑M ∧ L.age ↑M = K

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
hM : Structure.CG L ↑M
Kn : (L.age ↑M).Nonempty
left✝ : ∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)
cq : (Quotient.mk' '' L.age ↑M).Countable
hfg : ∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1
hp : Hereditary (L.age ↑M)
jep : JointEmbedding (L.age ↑M)
⊢ ∃ M_1, Countable ↑M_1 ∧ L.age ↑M_1 = L.age ↑M

Tactic:
exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩

Result:
no goals

Proof state:
case mp.intro.intro.refl
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
h1 : Countable ↑M
⊢ (L.age ↑M).Nonempty ∧
    (∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)) ∧
      (Quotient.mk' '' L.age ↑M).Countable ∧
        (∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1) ∧ Hereditary (L.age ↑M) ∧ JointEmbedding (L.age ↑M)

Tactic:
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⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
Kn : K.Nonempty
left✝ : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
cq : (Quotient.mk' '' K).Countable
hfg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Countable ↑M ∧ L.age ↑M = K

Tactic:
obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
hM : Structure.CG L ↑M
Kn : (L.age ↑M).Nonempty
left✝ : ∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)
cq : (Quotient.mk' '' L.age ↑M).Countable
hfg : ∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1
hp : Hereditary (L.age ↑M)
jep : JointEmbedding (L.age ↑M)
⊢ ∃ M_1, Countable ↑M_1 ∧ L.age ↑M_1 = L.age ↑M

Proof state:
case mp
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) →
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
rintro ⟨M, h1, h2, rfl⟩

Result:
case mp.intro.intro.refl
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
h1 : Countable ↑M
⊢ (L.age ↑M).Nonempty ∧
    (∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)) ∧
      (Quotient.mk' '' L.age ↑M).Countable ∧
        (∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1) ∧ Hereditary (L.age ↑M) ∧ JointEmbedding (L.age ↑M)

Proof state:
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
constructor

Result:
case mp
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) →
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K →
    ∃ M, Countable ↑M ∧ L.age ↑M = K