doc: fix the docs on ModelTheory/* (#3968)

Mathlib/ModelTheory/Basic.lean

@@ -29,16 +29,10 @@ structures.
 * A `FirstOrder.Language.Embedding`, denoted `M ↪[L] N`, is an embedding from the `L`-structure `M`
   to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves
   the interpretations of relations in both directions.
-* A `FirstOrder.Language.ElementaryEmbedding`, denoted `M ↪ₑ[L] N`, is an embedding from the
-  `L`-structure `M` to the `L`-structure `N` that commutes with the realizations of all formulas.
 * A `FirstOrder.Language.Equiv`, denoted `M ≃[L] N`, is an equivalence from the `L`-structure `M`
   to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves
   the interpretations of relations in both directions.
 
-## TODO
-
-Use `[Countable L.symbols]` instead of `[L.countable]`.
-
 ## References
 For the Flypitch project:
 - [J. Han, F. van Doorn, *A formal proof of the independence of the continuum hypothesis*]
@@ -980,12 +974,12 @@ instance (priority := 100) strongHomClassEmpty {F M N} [FunLike F M fun _ => N]
   ⟨fun _ _ f => Empty.elim f, fun _ _ r => Empty.elim r⟩
 #align first_order.language.strong_hom_class_empty FirstOrder.Language.strongHomClassEmpty
 
-/-- Makes a `Language.empty.hom` out of any function. -/
+/-- Makes a `Language.empty.Hom` out of any function. -/
 @[simps]
 def _root_.Function.emptyHom (f : M → N) : M →[Language.empty] N where toFun := f
 #align function.empty_hom Function.emptyHom
 
-/-- Makes a `Language.empty.embedding` out of any function. -/
+/-- 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
 #align embedding.empty Embedding.empty
@@ -998,7 +992,7 @@ theorem toFun_embedding_empty (f : M ↪ N) : (Embedding.empty f : M → N) = f
 theorem toEmbedding_embedding_empty (f : M ↪ N) : (Embedding.empty f).toEmbedding = f :=
   rfl
 
-/-- Makes a `Language.empty.equiv` out of any function. -/
+/-- 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
 #align equiv.empty Equiv.empty

Mathlib/ModelTheory/Bundled.lean

@@ -16,8 +16,8 @@ import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 This file bundles types together with their first-order structure.
 
 ## Main Definitions
-* `FirstOrder.language.Theory.ModelType` is the type of nonempty models of a particular theory.
-* `FirstOrder.language.equivSetoid` is the isomorphism equivalence relation on bundled structures.
+* `FirstOrder.Language.Theory.ModelType` is the type of nonempty models of a particular theory.
+* `FirstOrder.Language.equivSetoid` is the isomorphism equivalence relation on bundled structures.
 
 ## TODO
 * Define category structures on bundled structures and models.

Mathlib/ModelTheory/ElementaryMaps.lean

@@ -415,7 +415,7 @@ theorem isElementary (S : L.ElementarySubstructure M) : (S : L.Substructure M).I
   S.is_elementary'
 #align first_order.language.elementary_substructure.is_elementary FirstOrder.Language.ElementarySubstructure.isElementary
 
-/-- The natural embedding of an `L.substructure` of `M` into `M`. -/
+/-- The natural embedding of an `L.Substructure` of `M` into `M`. -/
 def subtype (S : L.ElementarySubstructure M) : S ↪ₑ[L] M where
   toFun := (↑)
   map_formula' := S.isElementary

Mathlib/ModelTheory/FinitelyGenerated.lean

@@ -16,10 +16,10 @@ This file defines what it means for a first-order (sub)structure to be finitely
 generated, similarly to other finitely-generated objects in the algebra library.
 
 ## Main Definitions
-* `first_order.language.substructure.FG` indicates that a substructure is finitely generated.
-* `first_order.language.Structure.FG` indicates that a structure is finitely generated.
-* `first_order.language.substructure.CG` indicates that a substructure is countably generated.
-* `first_order.language.Structure.CG` indicates that a structure is countably generated.
+* `FirstOrder.Language.Substructure.FG` indicates that a substructure is finitely generated.
+* `FirstOrder.Language.Structure.FG` indicates that a structure is finitely generated.
+* `FirstOrder.Language.Substructure.CG` indicates that a substructure is countably generated.
+* `FirstOrder.Language.Structure.CG` indicates that a structure is countably generated.
 
 
 ## TODO
@@ -212,7 +212,7 @@ theorem fg_def : FG L M ↔ (⊤ : L.Substructure M).FG :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 #align first_order.language.Structure.fg_def FirstOrder.Language.Structure.fg_def
 
-/-- An equivalent expression of `Structure.fg` in terms of `set.finite` instead of `finset`. -/
+/-- An equivalent expression of `Structure.fg` in terms of `Set.Finite` instead of `Finset`. -/
 theorem fg_iff : FG L M ↔ ∃ S : Set M, S.Finite ∧ closure L S = (⊤ : L.Substructure M) := by
   rw [fg_def, Substructure.fg_def]
 #align first_order.language.Structure.fg_iff FirstOrder.Language.Structure.fg_iff

Mathlib/ModelTheory/LanguageMap.lean

@@ -55,6 +55,7 @@ structure LHom where
 #align first_order.language.Lhom FirstOrder.Language.LHom
 
 -- mathport name: «expr →ᴸ »
+@[inherit_doc FirstOrder.Language.LHom]
 infixl:10 " →ᴸ " => LHom
 
 -- \^L
@@ -453,6 +454,7 @@ def withConstants : Language.{max u w', v} :=
 #align first_order.language.with_constants FirstOrder.Language.withConstants
 
 -- mathport name: language.with_constants
+@[inherit_doc FirstOrder.Language.withConstants]
 scoped[FirstOrder] notation:95 L "[[" α "]]" => Language.withConstants L α
 
 @[simp]

Mathlib/ModelTheory/Order.lean

@@ -28,7 +28,7 @@ particularly useful example in model theory.
 
 ## Main Results
 * `PartialOrder`s model the theory of partial orders, `LinearOrder`s model the theory of
-linear orders, and dense linear orders without endpoints model `Theory.DLO`.
+linear orders, and dense linear orders without endpoints model `Language.dlo`.
 
 -/
 

Mathlib/ModelTheory/Semantics.lean

@@ -19,27 +19,27 @@ in a style inspired by the [Flypitch project](https://flypitch.github.io/).
 ## Main Definitions
 * `FirstOrder.Language.Term.realize` is defined so that `t.realize v` is the term `t` evaluated at
 variables `v`.
-* `FirstOrder.Language.BoundedFormula.Realize` is defined so that `φ.realize v xs` is the bounded
+* `FirstOrder.Language.BoundedFormula.Realize` is defined so that `φ.Realize v xs` is the bounded
 formula `φ` evaluated at tuples of variables `v` and `xs`.
-* `FirstOrder.Language.Formula.Realize` is defined so that `φ.realize v` is the formula `φ`
+* `FirstOrder.Language.Formula.Realize` is defined so that `φ.Realize v` is the formula `φ`
 evaluated at variables `v`.
-* `FirstOrder.Language.Sentence.Realize` is defined so that `φ.realize M` is the sentence `φ`
+* `FirstOrder.Language.Sentence.Realize` is defined so that `φ.Realize M` is the sentence `φ`
 evaluated in the structure `M`. Also denoted `M ⊨ φ`.
-* `FirstOrder.Language.Theory.Model` is defined so that `T.model M` is true if and only if every
+* `FirstOrder.Language.Theory.Model` is defined so that `T.Model M` is true if and only if every
 sentence of `T` is realized in `M`. Also denoted `T ⊨ φ`.
 
 ## Main Results
 * `FirstOrder.Language.BoundedFormula.realize_toPrenex` shows that the prenex normal form of a
 formula has the same realization as the original formula.
-* Several results in this file show that syntactic constructions such as `relabel`, `castLe`,
-`lift_at`, `subst`, and the actions of language maps commute with realization of terms, formulas,
+* Several results in this file show that syntactic constructions such as `relabel`, `castLE`,
+`liftAt`, `subst`, and the actions of language maps commute with realization of terms, formulas,
 sentences, and theories.
 
 ## Implementation Notes
-* Formulas use a modified version of de Bruijn variables. Specifically, a `L.boundedFormula α n`
+* Formulas use a modified version of de Bruijn variables. Specifically, a `L.BoundedFormula α n`
 is a formula with some variables indexed by a type `α`, which cannot be quantified over, and some
-indexed by `Fin n`, which can. For any `φ : L.boundedFormula α (n + 1)`, we define the formula
-`∀' φ : L.boundedFormula α n` by universally quantifying over the variable indexed by
+indexed by `Fin n`, which can. For any `φ : L.BoundedFormula α (n + 1)`, we define the formula
+`∀' φ : L.BoundedFormula α n` by universally quantifying over the variable indexed by
 `n : Fin (n + 1)`.
 
 ## References

Mathlib/ModelTheory/Substructures.lean

@@ -26,7 +26,7 @@ the least substructure of `M` containing `s`.
 substructure `s` under the homomorphism `f`, as a substructure.
 * `FirstOrder.Language.Substructure.map` is defined so that `s.map f` is the image of the
 substructure `s` under the homomorphism `f`, as a substructure.
-* `FirstOrder.Language.Hom.range` is defined so that `f.map` is the range of the
+* `FirstOrder.Language.Hom.range` is defined so that `f.range` is the range of the
 the homomorphism `f`, as a substructure.
 * `FirstOrder.Language.Hom.domRestrict` and `FirstOrder.Language.Hom.codRestrict` restrict
 the domain and codomain respectively of first-order homomorphisms to substructures.
@@ -663,7 +663,7 @@ instance inducedStructure {S : L.Substructure M} : L.Structure S where
 set_option linter.uppercaseLean3 false in
 #align first_order.language.substructure.induced_Structure FirstOrder.Language.Substructure.inducedStructure
 
-/-- The natural embedding of an `L.substructure` of `M` into `M`. -/
+/-- The natural embedding of an `L.Substructure` of `M` into `M`. -/
 def subtype (S : L.Substructure M) : S ↪[L] M where
   toFun := (↑)
   inj' := Subtype.coe_injective

Mathlib/ModelTheory/Syntax.lean

@@ -21,7 +21,7 @@ This file defines first-order terms, formulas, sentences, and theories in a styl
 ## Main Definitions
 * A `FirstOrder.Language.Term` is defined so that `L.Term α` is the type of `L`-terms with free
   variables indexed by `α`.
-* A `FirstOrder.Language.Formula` is defined so that `L.formula α` is the type of `L`-formulas with
+* A `FirstOrder.Language.Formula` is defined so that `L.Formula α` is the type of `L`-formulas with
   free variables indexed by `α`.
 * A `FirstOrder.Language.Sentence` is a formula with no free variables.
 * A `FirstOrder.Language.Theory` is a set of sentences.
@@ -41,10 +41,10 @@ variables with given terms.
 constants in the language and having extra variables indexed by the same type.
 
 ## Implementation Notes
-* Formulas use a modified version of de Bruijn variables. Specifically, a `L.boundedFormula α n`
+* Formulas use a modified version of de Bruijn variables. Specifically, a `L.BoundedFormula α n`
 is a formula with some variables indexed by a type `α`, which cannot be quantified over, and some
-indexed by `Fin n`, which can. For any `φ : L.boundedFormula α (n + 1)`, we define the formula
-`∀' φ : L.boundedFormula α n` by universally quantifying over the variable indexed by
+indexed by `Fin n`, which can. For any `φ : L.BoundedFormula α (n + 1)`, we define the formula
+`∀' φ : L.BoundedFormula α n` by universally quantifying over the variable indexed by
 `n : Fin (n + 1)`.
 
 ## References
@@ -792,7 +792,7 @@ theorem IsPrenex.liftAt {k m : ℕ} (h : IsPrenex φ) : (φ.liftAt k m).IsPrenex
 
 --Porting note: universes in different order
 /-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
-  If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.to_prenex_imp_right ψ`
+  If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.toPrenexImpRight ψ`
   is a prenex normal form for `φ.imp ψ`. -/
 def toPrenexImpRight : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
   | n, φ, BoundedFormula.ex ψ => ((φ.liftAt 1 n).toPrenexImpRight ψ).ex
@@ -822,7 +822,7 @@ theorem isPrenex_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ
 
 --Porting note: universes in different order
 /-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
-  If `φ` and `ψ` are in prenex normal form, then `φ.to_prenex_imp ψ`
+  If `φ` and `ψ` are in prenex normal form, then `φ.toPrenexImp ψ`
   is a prenex normal form for `φ.imp ψ`. -/
 def toPrenexImp : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
   | n, BoundedFormula.ex φ, ψ => (φ.toPrenexImp (ψ.liftAt 1 n)).all