bump to nightly-2023-04-13-00

mathlib commit leanprover-community/mathlib@039ef89

Mathbin/ModelTheory/Bundled.lean

@@ -152,7 +152,7 @@ def reduct {L' : Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelCat) : T
   carrier := M
   struc := φ.reduct M
   nonempty' := M.nonempty'
-  is_model := (@Lhom.onTheory_model L L' M (φ.reduct M) _ φ _ T).1 M.is_model
+  is_model := (@LHom.onTheory_model L L' M (φ.reduct M) _ φ _ T).1 M.is_model
 #align first_order.language.Theory.Model.reduct FirstOrder.Language.Theory.ModelCat.reduct
 
 /-- When `φ` is injective, `default_expansion` expands a model of `T` to a model of `φ.on_Theory T`
@@ -167,16 +167,16 @@ noncomputable def defaultExpansion {L' : Language} {φ : L →ᴸ L'} (h : φ.In
   struc := φ.defaultExpansion M
   nonempty' := M.nonempty'
   is_model :=
-    (@Lhom.onTheory_model L L' M _ (φ.defaultExpansion M) φ (h.isExpansionOn_default M) T).2
+    (@LHom.onTheory_model L L' M _ (φ.defaultExpansion M) φ (h.isExpansionOn_default M) T).2
       M.is_model
 #align first_order.language.Theory.Model.default_expansion FirstOrder.Language.Theory.ModelCat.defaultExpansion
 
 instance leftStructure {L' : Language} {T : (L.Sum L').Theory} (M : T.ModelCat) : L.Structure M :=
-  (Lhom.sumInl : L →ᴸ L.Sum L').reduct M
+  (LHom.sumInl : L →ᴸ L.Sum L').reduct M
 #align first_order.language.Theory.Model.left_Structure FirstOrder.Language.Theory.ModelCat.leftStructure
 
 instance rightStructure {L' : Language} {T : (L.Sum L').Theory} (M : T.ModelCat) : L'.Structure M :=
-  (Lhom.sumInr : L' →ᴸ L.Sum L').reduct M
+  (LHom.sumInr : L' →ᴸ L.Sum L').reduct M
 #align first_order.language.Theory.Model.right_Structure FirstOrder.Language.Theory.ModelCat.rightStructure
 
 /-- A model of a theory is also a model of any subtheory. -/

Mathbin/ModelTheory/Order.lean

@@ -90,7 +90,7 @@ variable (L)
 /-- The language homomorphism sending the unique symbol `≤` of `language.order` to `≤` in an ordered
  language. -/
 def orderLhom : Language.order →ᴸ L :=
-  Lhom.mk₂ Empty.elim Empty.elim Empty.elim Empty.elim fun _ => leSymb
+  LHom.mk₂ Empty.elim Empty.elim Empty.elim Empty.elim fun _ => leSymb
 #align first_order.language.order_Lhom FirstOrder.Language.orderLhom
 
 end IsOrdered
@@ -105,8 +105,8 @@ theorem orderLhom_leSymb [L.IsOrdered] :
 #align first_order.language.order_Lhom_le_symb FirstOrder.Language.orderLhom_leSymb
 
 @[simp]
-theorem orderLhom_order : orderLhom Language.order = Lhom.id Language.order :=
-  Lhom.funext (Subsingleton.elim _ _) (Subsingleton.elim _ _)
+theorem orderLhom_order : orderLhom Language.order = LHom.id Language.order :=
+  LHom.funext (Subsingleton.elim _ _) (Subsingleton.elim _ _)
 #align first_order.language.order_Lhom_order FirstOrder.Language.orderLhom_order
 
 instance : IsOrdered (L.Sum Language.order) :=
@@ -160,14 +160,14 @@ variable (L M)
 
 /-- A structure is ordered if its language has a `≤` symbol whose interpretation is -/
 abbrev OrderedStructure [IsOrdered L] [LE M] [L.Structure M] : Prop :=
-  Lhom.IsExpansionOn (orderLhom L) M
+  LHom.IsExpansionOn (orderLhom L) M
 #align first_order.language.ordered_structure FirstOrder.Language.OrderedStructure
 
 variable {L M}
 
 @[simp]
 theorem orderedStructure_iff [IsOrdered L] [LE M] [L.Structure M] :
-    L.OrderedStructure M ↔ Lhom.IsExpansionOn (orderLhom L) M :=
+    L.OrderedStructure M ↔ LHom.IsExpansionOn (orderLhom L) M :=
   Iff.rfl
 #align first_order.language.ordered_structure_iff FirstOrder.Language.orderedStructure_iff
 

Mathbin/ModelTheory/Semantics.lean

@@ -209,7 +209,7 @@ theorem realize_onTerm [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M]
   induction' t with _ n f ts ih
   · rfl
   · simp only [term.realize, Lhom.on_term, Lhom.map_on_function, ih]
-#align first_order.language.Lhom.realize_on_term FirstOrder.Language.Lhom.realize_onTerm
+#align first_order.language.Lhom.realize_on_term FirstOrder.Language.LHom.realize_onTerm
 
 end Lhom
 
@@ -605,7 +605,7 @@ theorem realize_onBoundedFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpan
     rfl
   · simp only [on_bounded_formula, ih1, ih2, realize_imp]
   · simp only [on_bounded_formula, ih3, realize_all]
-#align first_order.language.Lhom.realize_on_bounded_formula FirstOrder.Language.Lhom.realize_onBoundedFormula
+#align first_order.language.Lhom.realize_on_bounded_formula FirstOrder.Language.LHom.realize_onBoundedFormula
 
 end Lhom
 
@@ -713,18 +713,18 @@ theorem realize_graph {f : L.Functions n} {x : Fin n → M} {y : M} :
 end Formula
 
 @[simp]
-theorem Lhom.realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α)
+theorem LHom.realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α)
     {v : α → M} : (φ.onFormula ψ).realize v ↔ ψ.realize v :=
   φ.realize_onBoundedFormula ψ
-#align first_order.language.Lhom.realize_on_formula FirstOrder.Language.Lhom.realize_onFormula
+#align first_order.language.Lhom.realize_on_formula FirstOrder.Language.LHom.realize_onFormula
 
 @[simp]
-theorem Lhom.setOf_realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M]
+theorem LHom.setOf_realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M]
     (ψ : L.Formula α) : (setOf (φ.onFormula ψ).realize : Set (α → M)) = setOf ψ.realize :=
   by
   ext
   simp
-#align first_order.language.Lhom.set_of_realize_on_formula FirstOrder.Language.Lhom.setOf_realize_onFormula
+#align first_order.language.Lhom.set_of_realize_on_formula FirstOrder.Language.LHom.setOf_realize_onFormula
 
 variable (M)
 
@@ -775,10 +775,10 @@ theorem realize_equivSentence_symm (φ : L[[α]].Sentence) (v : α → M) :
 end Formula
 
 @[simp]
-theorem Lhom.realize_onSentence [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M]
+theorem LHom.realize_onSentence [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M]
     (ψ : L.Sentence) : M ⊨ φ.onSentence ψ ↔ M ⊨ ψ :=
   φ.realize_onFormula ψ
-#align first_order.language.Lhom.realize_on_sentence FirstOrder.Language.Lhom.realize_onSentence
+#align first_order.language.Lhom.realize_on_sentence FirstOrder.Language.LHom.realize_onSentence
 
 variable (L)
 
@@ -839,9 +839,9 @@ theorem Theory.realize_sentence_of_mem [M ⊨ T] {φ : L.Sentence} (h : φ ∈ T
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 @[simp]
-theorem Lhom.onTheory_model [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory) :
+theorem LHom.onTheory_model [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory) :
     M ⊨ φ.onTheory T ↔ M ⊨ T := by simp [Theory.model_iff, Lhom.on_Theory]
-#align first_order.language.Lhom.on_Theory_model FirstOrder.Language.Lhom.onTheory_model
+#align first_order.language.Lhom.on_Theory_model FirstOrder.Language.LHom.onTheory_model
 
 variable {M} {T}
 

Mathbin/ModelTheory/Skolem.lean

@@ -85,7 +85,7 @@ noncomputable instance skolem₁Structure : L.skolem₁.Structure M :=
 namespace Substructure
 
 theorem skolem₁_reduct_isElementary (S : (L.Sum L.skolem₁).Substructure M) :
-    (Lhom.sumInl.substructureReduct S).IsElementary :=
+    (LHom.sumInl.substructureReduct S).IsElementary :=
   by
   apply (Lhom.sum_inl.substructure_reduct S).is_elementary_of_exists
   intro n φ x a h
@@ -98,7 +98,7 @@ theorem skolem₁_reduct_isElementary (S : (L.Sum L.skolem₁).Substructure M) :
 /-- Any `L.sum L.skolem₁`-substructure is an elementary `L`-substructure. -/
 noncomputable def elementarySkolem₁Reduct (S : (L.Sum L.skolem₁).Substructure M) :
     L.ElementarySubstructure M :=
-  ⟨Lhom.sumInl.substructureReduct S, S.skolem₁_reduct_isElementary⟩
+  ⟨LHom.sumInl.substructureReduct S, S.skolem₁_reduct_isElementary⟩
 #align first_order.language.substructure.elementary_skolem₁_reduct FirstOrder.Language.Substructure.elementarySkolem₁Reduct
 
 theorem coeSort_elementarySkolem₁Reduct (S : (L.Sum L.skolem₁).Substructure M) :

Mathbin/ModelTheory/Substructures.lean

@@ -724,18 +724,18 @@ def substructureReduct : L'.Substructure M ↪o L.Substructure M
     simp only [SetLike.coe_set_eq] at h
     exact h
   map_rel_iff' S T := Iff.rfl
-#align first_order.language.Lhom.substructure_reduct FirstOrder.Language.Lhom.substructureReduct
+#align first_order.language.Lhom.substructure_reduct FirstOrder.Language.LHom.substructureReduct
 
 @[simp]
 theorem mem_substructureReduct {x : M} {S : L'.Substructure M} :
     x ∈ φ.substructureReduct S ↔ x ∈ S :=
   Iff.rfl
-#align first_order.language.Lhom.mem_substructure_reduct FirstOrder.Language.Lhom.mem_substructureReduct
+#align first_order.language.Lhom.mem_substructure_reduct FirstOrder.Language.LHom.mem_substructureReduct
 
 @[simp]
 theorem coe_substructureReduct {S : L'.Substructure M} : (φ.substructureReduct S : Set M) = ↑S :=
   rfl
-#align first_order.language.Lhom.coe_substructure_reduct FirstOrder.Language.Lhom.coe_substructureReduct
+#align first_order.language.Lhom.coe_substructure_reduct FirstOrder.Language.LHom.coe_substructureReduct
 
 end Lhom
 

Mathbin/ModelTheory/Syntax.lean

@@ -311,28 +311,28 @@ scoped[FirstOrder] prefix:arg "&" => FirstOrder.Language.Term.var ∘ Sum.inr
 
 namespace Lhom
 
-/- warning: first_order.language.Lhom.on_term -> FirstOrder.Language.Lhom.onTerm is a dubious translation:
+/- warning: first_order.language.Lhom.on_term -> FirstOrder.Language.LHom.onTerm is a dubious translation:
 lean 3 declaration is
-  forall {L : FirstOrder.Language.{u1, u2}} {L' : FirstOrder.Language.{u4, u5}} {α : Type.{u3}}, (FirstOrder.Language.Lhom.{u1, u2, u4, u5} L L') -> (FirstOrder.Language.Term.{u1, u2, u3} L α) -> (FirstOrder.Language.Term.{u4, u5, u3} L' α)
+  forall {L : FirstOrder.Language.{u1, u2}} {L' : FirstOrder.Language.{u4, u5}} {α : Type.{u3}}, (FirstOrder.Language.LHom.{u1, u2, u4, u5} L L') -> (FirstOrder.Language.Term.{u1, u2, u3} L α) -> (FirstOrder.Language.Term.{u4, u5, u3} L' α)
 but is expected to have type
-  forall {L : FirstOrder.Language.{u1, u5}} {L' : FirstOrder.Language.{u3, u4}} {α : Type.{u2}}, (FirstOrder.Language.Lhom.{u1, u5, u3, u4} L L') -> (FirstOrder.Language.Term.{u1, u5, u2} L α) -> (FirstOrder.Language.Term.{u3, u4, u2} L' α)
-Case conversion may be inaccurate. Consider using '#align first_order.language.Lhom.on_term FirstOrder.Language.Lhom.onTermₓ'. -/
+  forall {L : FirstOrder.Language.{u1, u5}} {L' : FirstOrder.Language.{u3, u4}} {α : Type.{u2}}, (FirstOrder.Language.LHom.{u1, u5, u3, u4} L L') -> (FirstOrder.Language.Term.{u1, u5, u2} L α) -> (FirstOrder.Language.Term.{u3, u4, u2} L' α)
+Case conversion may be inaccurate. Consider using '#align first_order.language.Lhom.on_term FirstOrder.Language.LHom.onTermₓ'. -/
 /-- Maps a term's symbols along a language map. -/
 @[simp]
 def onTerm (φ : L →ᴸ L') : L.term α → L'.term α
   | var i => var i
   | func f ts => func (φ.onFunction f) fun i => on_term (ts i)
-#align first_order.language.Lhom.on_term FirstOrder.Language.Lhom.onTerm
+#align first_order.language.Lhom.on_term FirstOrder.Language.LHom.onTerm
 
 @[simp]
-theorem id_onTerm : ((Lhom.id L).onTerm : L.term α → L.term α) = id :=
+theorem id_onTerm : ((LHom.id L).onTerm : L.term α → L.term α) = id :=
   by
   ext t
   induction' t with _ _ _ _ ih
   · rfl
   · simp_rw [on_term, ih]
     rfl
-#align first_order.language.Lhom.id_on_term FirstOrder.Language.Lhom.id_onTerm
+#align first_order.language.Lhom.id_on_term FirstOrder.Language.LHom.id_onTerm
 
 @[simp]
 theorem comp_onTerm {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
@@ -343,7 +343,7 @@ theorem comp_onTerm {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
   · rfl
   · simp_rw [on_term, ih]
     rfl
-#align first_order.language.Lhom.comp_on_term FirstOrder.Language.Lhom.comp_onTerm
+#align first_order.language.Lhom.comp_on_term FirstOrder.Language.LHom.comp_onTerm
 
 end Lhom
 
@@ -980,12 +980,12 @@ namespace Lhom
 
 open BoundedFormula
 
-/- warning: first_order.language.Lhom.on_bounded_formula -> FirstOrder.Language.Lhom.onBoundedFormula is a dubious translation:
+/- warning: first_order.language.Lhom.on_bounded_formula -> FirstOrder.Language.LHom.onBoundedFormula is a dubious translation:
 lean 3 declaration is
-  forall {L : FirstOrder.Language.{u1, u2}} {L' : FirstOrder.Language.{u4, u5}} {α : Type.{u3}}, (FirstOrder.Language.Lhom.{u1, u2, u4, u5} L L') -> (forall {k : Nat}, (FirstOrder.Language.BoundedFormula.{u1, u2, u3} L α k) -> (FirstOrder.Language.BoundedFormula.{u4, u5, u3} L' α k))
+  forall {L : FirstOrder.Language.{u1, u2}} {L' : FirstOrder.Language.{u4, u5}} {α : Type.{u3}}, (FirstOrder.Language.LHom.{u1, u2, u4, u5} L L') -> (forall {k : Nat}, (FirstOrder.Language.BoundedFormula.{u1, u2, u3} L α k) -> (FirstOrder.Language.BoundedFormula.{u4, u5, u3} L' α k))
 but is expected to have type
-  forall {L : FirstOrder.Language.{u1, u5}} {L' : FirstOrder.Language.{u3, u4}} {α : Type.{u2}}, (FirstOrder.Language.Lhom.{u1, u5, u3, u4} L L') -> (forall {k : Nat}, (FirstOrder.Language.BoundedFormula.{u1, u5, u2} L α k) -> (FirstOrder.Language.BoundedFormula.{u3, u4, u2} L' α k))
-Case conversion may be inaccurate. Consider using '#align first_order.language.Lhom.on_bounded_formula FirstOrder.Language.Lhom.onBoundedFormulaₓ'. -/
+  forall {L : FirstOrder.Language.{u1, u5}} {L' : FirstOrder.Language.{u3, u4}} {α : Type.{u2}}, (FirstOrder.Language.LHom.{u1, u5, u3, u4} L L') -> (forall {k : Nat}, (FirstOrder.Language.BoundedFormula.{u1, u5, u2} L α k) -> (FirstOrder.Language.BoundedFormula.{u3, u4, u2} L' α k))
+Case conversion may be inaccurate. Consider using '#align first_order.language.Lhom.on_bounded_formula FirstOrder.Language.LHom.onBoundedFormulaₓ'. -/
 /-- Maps a bounded formula's symbols along a language map. -/
 @[simp]
 def onBoundedFormula (g : L →ᴸ L') : ∀ {k : ℕ}, L.BoundedFormula α k → L'.BoundedFormula α k
@@ -994,11 +994,11 @@ def onBoundedFormula (g : L →ᴸ L') : ∀ {k : ℕ}, L.BoundedFormula α k 
   | k, Rel R ts => (g.onRelation R).BoundedFormula (g.onTerm ∘ ts)
   | k, imp f₁ f₂ => (on_bounded_formula f₁).imp (on_bounded_formula f₂)
   | k, all f => (on_bounded_formula f).all
-#align first_order.language.Lhom.on_bounded_formula FirstOrder.Language.Lhom.onBoundedFormula
+#align first_order.language.Lhom.on_bounded_formula FirstOrder.Language.LHom.onBoundedFormula
 
 @[simp]
 theorem id_onBoundedFormula :
-    ((Lhom.id L).onBoundedFormula : L.BoundedFormula α n → L.BoundedFormula α n) = id :=
+    ((LHom.id L).onBoundedFormula : L.BoundedFormula α n → L.BoundedFormula α n) = id :=
   by
   ext f
   induction' f with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
@@ -1008,7 +1008,7 @@ theorem id_onBoundedFormula :
     rfl
   · rw [on_bounded_formula, ih1, ih2, id.def, id.def, id.def]
   · rw [on_bounded_formula, ih3, id.def, id.def]
-#align first_order.language.Lhom.id_on_bounded_formula FirstOrder.Language.Lhom.id_onBoundedFormula
+#align first_order.language.Lhom.id_on_bounded_formula FirstOrder.Language.LHom.id_onBoundedFormula
 
 @[simp]
 theorem comp_onBoundedFormula {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
@@ -1024,28 +1024,28 @@ theorem comp_onBoundedFormula {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →
     rfl
   · simp only [on_bounded_formula, Function.comp_apply, ih1, ih2, eq_self_iff_true, and_self_iff]
   · simp only [ih3, on_bounded_formula, Function.comp_apply]
-#align first_order.language.Lhom.comp_on_bounded_formula FirstOrder.Language.Lhom.comp_onBoundedFormula
+#align first_order.language.Lhom.comp_on_bounded_formula FirstOrder.Language.LHom.comp_onBoundedFormula
 
 /-- Maps a formula's symbols along a language map. -/
 def onFormula (g : L →ᴸ L') : L.Formula α → L'.Formula α :=
   g.onBoundedFormula
-#align first_order.language.Lhom.on_formula FirstOrder.Language.Lhom.onFormula
+#align first_order.language.Lhom.on_formula FirstOrder.Language.LHom.onFormula
 
 /-- Maps a sentence's symbols along a language map. -/
 def onSentence (g : L →ᴸ L') : L.Sentence → L'.Sentence :=
   g.onFormula
-#align first_order.language.Lhom.on_sentence FirstOrder.Language.Lhom.onSentence
+#align first_order.language.Lhom.on_sentence FirstOrder.Language.LHom.onSentence
 
 /-- Maps a theory's symbols along a language map. -/
 def onTheory (g : L →ᴸ L') (T : L.Theory) : L'.Theory :=
   g.onSentence '' T
-#align first_order.language.Lhom.on_Theory FirstOrder.Language.Lhom.onTheory
+#align first_order.language.Lhom.on_Theory FirstOrder.Language.LHom.onTheory
 
 @[simp]
 theorem mem_onTheory {g : L →ᴸ L'} {T : L.Theory} {φ : L'.Sentence} :
     φ ∈ g.onTheory T ↔ ∃ φ₀, φ₀ ∈ T ∧ g.onSentence φ₀ = φ :=
   Set.mem_image _ _ _
-#align first_order.language.Lhom.mem_on_Theory FirstOrder.Language.Lhom.mem_onTheory
+#align first_order.language.Lhom.mem_on_Theory FirstOrder.Language.LHom.mem_onTheory
 
 end Lhom
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "3416b87ec8cbacb1e962544fa82526682f49c6a1",
+    "rev": "f749c4dbe76ae8aa697a9043bad05b0f4de3f188",
     "name": "lean3port",
-    "inputRev?": "3416b87ec8cbacb1e962544fa82526682f49c6a1"}},
+    "inputRev?": "f749c4dbe76ae8aa697a9043bad05b0f4de3f188"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "72a49e2ccfc57378887e7de57b73c480817044d3",
+    "rev": "28d9dc68d7bd1304ee2bebc14a12f7fb341d9bed",
     "name": "mathlib",
-    "inputRev?": "72a49e2ccfc57378887e7de57b73c480817044d3"}},
+    "inputRev?": "28d9dc68d7bd1304ee2bebc14a12f7fb341d9bed"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-04-12-22"
+def tag : String := "nightly-2023-04-13-00"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3416b87ec8cbacb1e962544fa82526682f49c6a1"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f749c4dbe76ae8aa697a9043bad05b0f4de3f188"
 
 @[default_target]
 lean_lib Mathbin where