Use a type synonym for withConstants structures

Author: NoneMore

Mathlib/ModelTheory/ElementaryMaps.lean

@@ -196,14 +196,17 @@ theorem comp_assoc (f : M ↪ₑ[L] N) (g : N ↪ₑ[L] P) (h : P ↪ₑ[L] Q) :
 
 /-- Lifts an elementary embedding to the expanded language with constants -/
 def liftWithConstants (f : M ↪ₑ[L] N) (A : Set M) :
-    @ElementaryEmbedding (L[[A]]) M N _ (f.toEmbedding.withConstantsStructure A) := by
-  letI : L[[A]].Structure N := f.toEmbedding.withConstantsStructure A
+    M ↪ₑ[L[[A]]] (f.toEmbedding.withConstants A) := by
   refine ⟨f, ?_⟩
   intro n φ x
-  have h : Sum.elim (fun a ↦ ↑(L.con a)) (f ∘ x) = f ∘ Sum.elim (fun a : ↑A ↦ ↑(L.con a)) x :=
+  have h :
+    (Sum.elim (fun a ↦ ↑(L.con a)) (⇑f ∘ x) :
+      ↑A ⊕ Fin n → f.toEmbedding.withConstants A) =
+    f ∘ Sum.elim (fun a ↦ ↑(L.con a)) x :=
     (Sum.comp_elim _ _ _).symm
   have h' : (default : Fin 0 → N) = f ∘ (default : Fin 0 → M) := List.ofFn_inj.mp rfl
-  simp [Formula.Realize, h', ← BoundedFormula.realize_constantsVarsEquiv, h]
+  simp only [Formula.Realize, h', ← BoundedFormula.realize_constantsVarsEquiv, h]
+  exact f.map_boundedFormula _ _ _
 
 end ElementaryEmbedding
 

Mathlib/ModelTheory/LanguageMap.lean

@@ -502,15 +502,23 @@ instance map_constants_inclusion_isExpansionOn :
 
 variable {L} (A) {N : Type w'} [L.Structure N] (f : M ↪[L] N)
 
-/-- Lifts a structure to the expanded language with respect to an embedding. -/
-def Embedding.withConstantsStructure : L[[A]].Structure N :=
-  letI : (constantsOn A).Structure N := constantsOn.structure fun a => f a
-  L.withConstantsStructure A
+/-- Type synonym for `N` used to equip it with an `L[[A]]`-structure where the new constants on `A`
+are interpreted via the embedding `f`. -/
+@[nolint unusedArguments]
+def Embedding.withConstants (f : M ↪[L] N) (A : Set M) : Type w' := N
+
+instance : L.Structure (f.withConstants A) := by
+  dsimp [Embedding.withConstants]
+  infer_instance
+
+instance (f : M ↪[L] N) : (constantsOn A).Structure (f.withConstants A) :=
+  constantsOn.structure fun a => f a
+
+instance : L[[A]].Structure (f.withConstants A) := L.withConstantsStructure A
 
 /-- Lifts an embedding to the expanded language with constants. -/
 def Embedding.liftWithConstants :
-    @Embedding (L[[A]]) M N _ (f.withConstantsStructure A) := by
-  letI : L[[A]].Structure N := f.withConstantsStructure A
+    M ↪[L[[A]]] f.withConstants A := by
   refine ⟨f.toEmbedding, ?_, ?_⟩
   · intro n g x
     cases g with