chore(ModelTheory): Tweaks involving the empty language (#16192)

Makes `FirstOrder.Language.emptyStructure` a `def` instead of an `instance`
Removes `def`s that could be accomplished with `StrongHomClass.toEmbedding` and `StrongHomClass.toEquiv`

Author: awainverse

Mathlib/ModelTheory/Basic.lean

@@ -934,14 +934,24 @@ end SumStructure
 
 section Empty
 
-section
+/-- Any type can be made uniquely into a structure over the empty language. -/
+def emptyStructure : Language.empty.Structure M :=
+  ⟨Empty.elim, Empty.elim⟩
+
+instance : Unique (Language.empty.Structure M) :=
+  ⟨⟨Language.emptyStructure⟩, fun a => by
+    ext _ f <;> exact Empty.elim f⟩
 
 variable [Language.empty.Structure M] [Language.empty.Structure N]
 
+instance (priority := 100) strongHomClassEmpty {F} [FunLike F M N] :
+    StrongHomClass Language.empty F M N :=
+  ⟨fun _ _ f => Empty.elim f, fun _ _ r => Empty.elim r⟩
+
 @[simp]
 theorem empty.nonempty_embedding_iff :
     Nonempty (M ↪[Language.empty] N) ↔ Cardinal.lift.{w'} #M ≤ Cardinal.lift.{w} #N :=
-  _root_.trans ⟨Nonempty.map fun f => f.toEmbedding, Nonempty.map fun f => { toEmbedding := f }⟩
+  _root_.trans ⟨Nonempty.map fun f => f.toEmbedding, Nonempty.map StrongHomClass.toEmbedding⟩
     Cardinal.lift_mk_le'.symm
 
 @[simp]
@@ -950,47 +960,12 @@ theorem empty.nonempty_equiv_iff :
   _root_.trans ⟨Nonempty.map fun f => f.toEquiv, Nonempty.map fun f => { toEquiv := f }⟩
     Cardinal.lift_mk_eq'.symm
 
-end
-
-instance emptyStructure : Language.empty.Structure M :=
-  ⟨Empty.elim, Empty.elim⟩
-
-instance : Unique (Language.empty.Structure M) :=
-  ⟨⟨Language.emptyStructure⟩, fun a => by
-    ext _ f <;> exact Empty.elim f⟩
-
-instance (priority := 100) strongHomClassEmpty {F M N} [FunLike F M N] :
-    StrongHomClass Language.empty F M N :=
-  ⟨fun _ _ f => Empty.elim f, fun _ _ r => Empty.elim r⟩
-
-/-- Makes a `Language.empty.Hom` out of any function. -/
+/-- Makes a `Language.empty.Hom` out of any function.
+This is only needed because there is no instance of `FunLike (M → N) M N`, and thus no instance of
+`Language.empty.HomClass M N`. -/
 @[simps]
 def _root_.Function.emptyHom (f : M → N) : M →[Language.empty] N where toFun := f
 
-/-- Makes a `Language.empty.Embedding` out of any function. -/
---@[simps] Porting note: commented out and lemmas added manually
-def _root_.Embedding.empty (f : M ↪ N) : M ↪[Language.empty] N where toEmbedding := f
-
-@[simp]
-theorem toFun_embedding_empty (f : M ↪ N) : (Embedding.empty f : M → N) = f :=
-  rfl
-
-@[simp]
-theorem toEmbedding_embedding_empty (f : M ↪ N) : (Embedding.empty f).toEmbedding = f :=
-  rfl
-
-/-- Makes a `Language.empty.Equiv` out of any function. -/
---@[simps] Porting note: commented out and lemmas added manually
-def _root_.Equiv.empty (f : M ≃ N) : M ≃[Language.empty] N where toEquiv := f
-
-@[simp]
-theorem toFun_equiv_empty (f : M ≃ N) : (Equiv.empty f : M → N) = f :=
-  rfl
-
-@[simp]
-theorem toEquiv_equiv_empty (f : M ≃ N) : (Equiv.empty f).toEquiv = f :=
-  rfl
-
 end Empty
 
 end Language

Mathlib/ModelTheory/Satisfiability.lean

@@ -578,8 +578,9 @@ theorem empty_theory_categorical (T : Language.empty.Theory) : κ.Categorical T
 
 theorem empty_infinite_Theory_isComplete : Language.empty.infiniteTheory.IsComplete :=
   (empty_theory_categorical.{0} ℵ₀ _).isComplete ℵ₀ _ le_rfl (by simp)
-    ⟨Theory.Model.bundled ((model_infiniteTheory_iff Language.empty).2
-      (inferInstanceAs (Infinite ℕ)))⟩ fun M =>
-    (model_infiniteTheory_iff Language.empty).1 M.is_model
+    ⟨by
+      haveI : Language.empty.Structure ℕ := emptyStructure
+      exact ((model_infiniteTheory_iff Language.empty).2 (inferInstanceAs (Infinite ℕ))).bundled⟩
+    fun M => (model_infiniteTheory_iff Language.empty).1 M.is_model
 
 end Cardinal