-- Mathlib/ModelTheory/Order.lean
lemma dlo_age [Language.order.Structure M] [Mdlo : M ⊨ Language.order.dlo] [Nonempty M] :
    Language.order.age M = {M : CategoryTheory.Bundled.{w'} Language.order.Structure |
      Finite M ∧ M ⊨ Language.order.linearOrderTheory}

Proof state:
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ Language.order.age M = {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
rw [age]

Result:
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ {N | FG Language.order ↑N ∧ Nonempty (↑N ↪[Language.order] M)} =
    {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Proof state:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
⊢ N ∈ {N | FG Language.order ↑N ∧ Nonempty (↑N ↪[Language.order] M)} ↔
    N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
  fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩

Result:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
⊢ Nonempty (↑N ↪[Language.order] M)

Proof state:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
⊢ Nonempty (↑N ↪[Language.order] M)

Tactic:
letI := Language.order.linearOrderOfModels M

Result:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
this : LinearOrder M := Language.order.linearOrderOfModels M
⊢ Nonempty (↑N ↪[Language.order] M)

Proof state:
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ {N | FG Language.order ↑N ∧ Nonempty (↑N ↪[Language.order] M)} =
    {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
ext N

Result:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
⊢ N ∈ {N | FG Language.order ↑N ∧ Nonempty (↑N ↪[Language.order] M)} ↔
    N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Proof state:
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ Language.order.age M = {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
classical
rw [age]
ext N
refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
  fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
letI := Language.order.linearOrderOfModels M
letI := Language.order.linearOrderOfModels N
exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩

Result:
no goals

Proof state:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
this : LinearOrder M := Language.order.linearOrderOfModels M
⊢ Nonempty (↑N ↪[Language.order] M)

Tactic:
letI := Language.order.linearOrderOfModels N

Result:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
this✝ : LinearOrder M := Language.order.linearOrderOfModels M
this : LinearOrder ↑N := Language.order.linearOrderOfModels ↑N
⊢ Nonempty (↑N ↪[Language.order] M)

Proof state:
case h
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
x✝ : N ∈ {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
hF : Finite ↑N
h : ↑N ⊨ Language.order.linearOrderTheory
this✝ : LinearOrder M := Language.order.linearOrderOfModels M
this : LinearOrder ↑N := Language.order.linearOrderOfModels ↑N
⊢ Nonempty (↑N ↪[Language.order] M)

Tactic:
exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩

Result:
no goals