Merge branch 'ec-formula' into partial-type

Author: NoneMore

Mathlib/ModelTheory/Semantics.lean

@@ -915,31 +915,21 @@ theorem realize_exClosure_of_realize_equivSentence [DecidableEq α] [L[[α]].Str
     (h : (Formula.equivSentence φ).Realize M) : φ.exClosure.Realize M := by
   rw [Formula.realize_exClosure]
   exists fun a => (L.con (a : α) : M)
-  apply (BoundedFormula.realize_restrictFreeVar'
-    (s := (φ.freeVarFinset : Set α)) Set.Subset.rfl
-    (v := fun a => (L.con a : M))).2
-  exact (φ.realize_equivSentence M).1 h
+  simpa [Formula.Realize, BoundedFormula.realize_restrictFreeVar] using h
 
 theorem exists_realize_equivSentence_of_realize_exClosure [DecidableEq α] [Nonempty M]
-    {φ : L.Formula α} (h : φ.exClosure.Realize (M := M)) :
+    {φ : L.Formula α} (h : φ.exClosure.Realize M) :
     ∃ v : α → M,
       @Sentence.Realize _ M (@Language.withConstantsStructure L M _ α (constantsOn.structure v))
         (Formula.equivSentence φ) := by
   classical
-  obtain ⟨v, hv⟩ := (φ.realize_exClosure (M := M)).1 h
-  let v' : α → M := fun a =>
-    if hmem : a ∈ φ.freeVarFinset then v ⟨a, hmem⟩ else Classical.choice inferInstance
+  obtain ⟨v, hv⟩ := (Formula.realize_exClosure φ).1 h
+  let v' := fun a =>if hmem : a ∈ φ.freeVarFinset
+    then v ⟨a, hmem⟩ else Classical.choice inferInstance
   exists v'
-  have hvEq : v' ∘ (↑) = v := by aesop
-  have hv' : Formula.Realize (φ.restrictFreeVar id) (v' ∘ (↑)) := by
-    simp_all only [realize_exClosure]
-  have hφ : φ.Realize v' := by
-    apply
-      (BoundedFormula.realize_restrictFreeVar' (s := (φ.freeVarFinset : Set α))
-        Set.Subset.rfl).1
-    simpa [Set.inclusion_eq_id] using hv'
-  exact
-    (Formula.realize_equivSentence_symm M (Formula.equivSentence φ) v').1 (by simpa)
+  simpa [Formula.realize_equivSentence, Formula.Realize] using
+    (BoundedFormula.realize_restrictFreeVar v'
+      (by aesop)).1 hv
 
 end Formula