-- Mathlib/ModelTheory/PartialEquiv.lean
theorem countable_self_fgequiv_of_countable [Countable M] :
    Countable (L.FGEquiv M M)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
⊢ Countable (L.FGEquiv M M)

Tactic:
let g : L.FGEquiv M M →
    Σ U : { S : L.Substructure M // S.FG }, U.val →[L] M :=
  fun f ↦ ⟨⟨f.val.dom, f.prop⟩, (subtype _).toHom.comp f.val.toEquiv.toHom⟩

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
⊢ Countable (L.FGEquiv M M)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
g_inj : Function.Injective g
this : ∀ (U : { S // S.FG }), Structure.FG L ↥↑U
⊢ Countable (L.FGEquiv M M)

Tactic:
exact Function.Embedding.countable ⟨g, g_inj⟩

Result:
no goals

Proof state:
case a.refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : cod_f.subtype.toHom.comp equiv_f.toHom = (↑f').cod.subtype.toHom.comp (↑f').toEquiv.toHom
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)

Tactic:
exact fun x hx ↦ congr_fun (congr_arg (↑) h) ⟨x, hx⟩

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
h : g f = g f'
⊢ f = f'

Tactic:
ext

Result:
case a
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
h : g f = g f'
⊢ ↑f = ↑f'

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
⊢ Function.Injective g

Tactic:
intro f f' h

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
h : g f = g f'
⊢ f = f'

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom = (↑f').dom

Tactic:
rfl

Result:
no goals

Proof state:
case a
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
h : g f = g f'
⊢ ↑f = ↑f'

Tactic:
let ⟨⟨dom_f, cod_f, equiv_f⟩, f_fin⟩ := f

Result:
case a
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
dom_f cod_f : L.Substructure M
equiv_f : ↥dom_f ≃[L] ↥cod_f
f_fin : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ↑⟨{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = ↑f'

Proof state:
case a.refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)

Tactic:
simp only [g, Sigma.mk.inj_iff, heq_eq_eq, true_and] at h

Result:
case a.refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : cod_f.subtype.toHom.comp equiv_f.toHom = (↑f').cod.subtype.toHom.comp (↑f').toEquiv.toHom
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)

Proof state:
case a.refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = ↑f'

Tactic:
apply PartialEquiv.ext (by rfl)

Result:
case a.refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
g_inj : Function.Injective g
⊢ Countable (L.FGEquiv M M)

Tactic:
have : ∀ U : { S : L.Substructure M // S.FG }, Structure.FG L U.val :=
  fun U ↦ (U.val.fg_iff_structure_fg.1 U.prop)

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f => ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
g_inj : Function.Injective g
this : ∀ (U : { S // S.FG }), Structure.FG L ↥↑U
⊢ Countable (L.FGEquiv M M)