Trigger CI for leanprover-community/batteries#813

leanprover-community · Dec 23, 2024 · 88ce072 · 88ce072
2 parents a1bda00 + 85bb89c
commit 88ce072
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
@@ -568,6 +568,12 @@ theorem realize_graph {f : L.Functions n} {x : Fin n → M} {y : M} :
   simp only [Formula.graph, Term.realize, realize_equal, Fin.cons_zero, Fin.cons_succ]
   rw [eq_comm]
 
+theorem boundedFormula_realize_eq_realize (φ : L.Formula α) (x : α → M) (y : Fin 0 → M) :
+    BoundedFormula.Realize φ x y ↔ φ.Realize x := by
+  rw [Formula.Realize, iff_iff_eq]
+  congr
+  ext i; exact Fin.elim0 i
+
 end Formula
 
 @[simp]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d3a45c11f470e814978c1e939a60509e3420c0b5",
+   "rev": "8510de1dc4a6a573fc9e6c0980315fc1088da4db",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "union-darray",