-- Mathlib/ModelTheory/Fraisse.lean
theorem nonempty_equiv : Nonempty (M ≃[L] N)

Proof state:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ { α := ↥S, str := inferInstance } ∈ L.age N

Tactic:
rw [hN.age, ← hM.age]

Result:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Proof state:
case intro.intro
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
⊢ Nonempty (M ≃[L] N)

Tactic:
let v : M ≃ₚ[L] N := {
  dom := S
  cod := emb_S.toHom.range
  toEquiv := emb_S.equivRange
}

Result:
case intro.intro
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
v : M ≃ₚ[L] N := { dom := S, cod := emb_S.toHom.range, toEquiv := emb_S.equivRange }
⊢ Nonempty (M ≃[L] N)

Proof state:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ Nonempty (M ≃[L] N)

Tactic:
obtain ⟨_, ⟨emb_S : S ↪[L] N⟩⟩ : ⟨S, inferInstance⟩ ∈ L.age N := by
  rw [hN.age, ← hM.age]
  exact ⟨S_fg, ⟨subtype _⟩⟩

Result:
case intro.intro
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
⊢ Nonempty (M ≃[L] N)

Proof state:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
⊢ Nonempty (M ≃[L] N)

Tactic:
have S_fg : FG L S := (fg_iff_structure_fg _).1 Substructure.fg_bot

Result:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ Nonempty (M ≃[L] N)

Proof state:
case intro.intro
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
v : M ≃ₚ[L] N := { dom := S, cod := emb_S.toHom.range, toEquiv := emb_S.equivRange }
⊢ Nonempty (M ≃[L] N)

Tactic:
exact ⟨Exists.choose (equiv_between_cg cg_of_countable cg_of_countable
  ⟨v, ((Substructure.fg_iff_structure_fg _).2 S_fg)⟩ (hM.isExtensionPair hN)
    (hN.isExtensionPair hM))⟩

Result:
no goals

Proof state:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨S_fg, ⟨subtype _⟩⟩

Result:
no goals

Proof state:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
⊢ Nonempty (M ≃[L] N)

Tactic:
let S : L.Substructure M := ⊥

Result:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
⊢ Nonempty (M ≃[L] N)