doc(FirstOrder): Fix some typos and add a few docstrings

Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean

@@ -31,12 +31,12 @@ lemma succ_induction {P : V → Prop}
   InductionScheme.succ_induction (C := Semiformula.Open) (by
     rcases hP with ⟨φ, hp, hhp⟩
     haveI : Inhabited V := Classical.inhabited_of_nonempty'
-    refine ⟨φ.enumarateFVar, Rew.rewriteMap φ.idxOfFVar ▹ φ, by simp [hp], ?_⟩
+    refine ⟨φ.enumerateFVar, Rew.rewriteMap φ.idxOfFVar ▹ φ, by simp [hp], ?_⟩
     intro x
     simp only [hhp, Nat.succ_eq_add_one, Nat.reduceAdd, Semiformula.eval_rewriteMap]
     exact Semiformula.eval_iff_of_funEqOn φ (by
       intro z hz
-      simp [Semiformula.enumarateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hz)]))
+      simp [Semiformula.enumerateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hz)]))
     zero succ
 
 lemma least_number {P : V → Prop}

Foundation/FirstOrder/Arithmetic/Schemata.lean

@@ -141,7 +141,7 @@ lemma succ_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P)
   InductionScheme.succ_induction (P := P) (C := Hierarchy Γ m) (by
     rcases hP with ⟨φ, hp⟩
     haveI : Inhabited V := Classical.inhabited_of_nonempty'
-    exact ⟨φ.val.enumarateFVar, (Rew.rewriteMap φ.val.idxOfFVar) ▹ φ.val, by simp,
+    exact ⟨φ.val.enumerateFVar, (Rew.rewriteMap φ.val.idxOfFVar) ▹ φ.val, by simp,
       by intro x; simp [Semiformula.eval_rewriteMap, hp.df.iff]⟩)
     zero succ
 

Foundation/FirstOrder/Basic/Semantics/Semantics.lean

@@ -453,10 +453,10 @@ lemma eval_toEmpty [DecidableEq ξ] {n} {φ : Semiformula L ξ n} (hp : φ.freeV
   haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
   simp [Semiformula.univCl, ←eval_toEmpty (f := default)]
 
-@[simp] lemma eval_enumarateFVar_idxOfFVar_eq_id [DecidableEq M] [Inhabited M] (φ : Semiformula L M n) (v) :
-    φ.Eval v (fun x ↦ φ.enumarateFVar (φ.idxOfFVar x)) ↔ φ.Eval v id :=
+@[simp] lemma eval_enumerateFVar_idxOfFVar_eq_id [DecidableEq M] [Inhabited M] (φ : Semiformula L M n) (v) :
+    φ.Eval v (fun x ↦ φ.enumerateFVar (φ.idxOfFVar x)) ↔ φ.Eval v id :=
   Semiformula.eval_iff_of_funEqOn _ <| by
-    intro x hx; simp [Semiformula.enumarateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hx)]
+    intro x hx; simp [Semiformula.enumerateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hx)]
 
 end rew
 

Foundation/FirstOrder/Basic/Syntax/Formula.lean

@@ -541,7 +541,7 @@ def lMap (Φ : L₁ →ᵥ L₂) {n} : Semiformula L₁ ξ n →ˡᶜ Semiformul
     (Semiformula.lMap Φ φ).freeVariables = φ.freeVariables := by
   induction φ using Semiformula.rec' <;> try simp [lMap_rel, lMap_nrel, freeVariables_rel, freeVariables_nrel, *]
 
-section enumarateFVar
+section enumerateFVar
 
 def fvarList {n : ℕ} : Semiformula L ξ n → List ξ
   |        ⊤ => []
@@ -555,18 +555,18 @@ def fvarList {n : ℕ} : Semiformula L ξ n → List ξ
 
 def idxOfFVar [DecidableEq ξ] (φ : Semiformula L ξ n) : ξ → ℕ := φ.fvarList.idxOf
 
-def enumarateFVar [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ :=
+def enumerateFVar [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ :=
   fun i ↦ if hi : i < φ.fvarList.length then φ.fvarList.get ⟨i, hi⟩ else default
 
-lemma enumarateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) :
-    enumarateFVar φ (idxOfFVar φ x) = x := by
-  simpa [enumarateFVar, idxOfFVar]
+lemma enumerateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) :
+    enumerateFVar φ (idxOfFVar φ x) = x := by
+  simpa [enumerateFVar, idxOfFVar]
   using fun h ↦ False.elim <| not_le.mpr (List.idxOf_lt_length_iff.mpr hx) h
 
 lemma mem_fvarList_iff_fvar? [DecidableEq ξ] {φ : Semiformula L ξ n} : x ∈ φ.fvarList ↔ φ.FVar? x := by
   induction φ using rec' <;> simp [fvarList, Semiterm.mem_fvarList_iff_fvar?, *]
 
-end enumarateFVar
+end enumerateFVar
 
 end Semiformula
 

Foundation/FirstOrder/SetTheory/Recursion.lean

@@ -116,7 +116,7 @@ lemma attempt_function_restrict_eq_of_lt
   intro γ hγβ y
   have hγα : γ ∈ α.val := by aesop
   have : IsOrdinal γ := of_mem hγβ
-  have hγsusbetβ : γ ⊆ β.val := by grind
+  have hγsubsetβ : γ ⊆ β.val := by grind
   simp_all [mem_restrict_iff]
 
 /-- Any two attempt functions agree on overlapping inputs. -/

Foundation/FirstOrder/SetTheory/Z.lean

@@ -282,7 +282,7 @@ instance power.definable : ℒₛₑₜ-function₁[V] power := power.defined.to
 
 lemma separation_exists_eval (x : V) (φ : SetTheorySemiformula V 1) : ∃ y : V, ∀ z : V, z ∈ y ↔ z ∈ x ∧ φ.Eval ![z] id := by
   -- have : Inhabited V := inhabited_of_nonempty inferInstance
-  let f := φ.enumarateFVar
+  let f := φ.enumerateFVar
   let ψ := (Rew.rewriteMap φ.idxOfFVar) ▹ φ
   have := by simpa [models_iff, Semiformula.eval_univCl, Axiom.separationSchema] using Theory.models V 𝗭 (Zermelo.axiom_of_separation ψ)
   simpa [ψ, f, Semiformula.eval_rewriteMap, Matrix.constant_eq_singleton] using this f x

Foundation/FirstOrder/SetTheory/ZF.lean

@@ -16,7 +16,7 @@ lemma replacement_exists_eval (φ : SetTheorySemiformula V 2) (X : V) (h : (∀
     ∃ Y : V, ∀ y : V, y ∈ Y ↔ ∃ x ∈ X, φ.Eval ![x, y] id := by
   /- `φ` can have finitely many free variables of type `V`, these are interpreted by `id : V → V` as finitely many parameters in `V`.
   `f` enumerates the parameters of `φ`. -/
-  let f := φ.enumarateFVar
+  let f := φ.enumerateFVar
   /- While `φ` has free variables of type `V`, `ψ` has free variables of type `ℕ`.
   Since `f` enumerates the parameters, it is intended to be the valuation of the free variables of `ψ`. -/
   let ψ := (Rew.rewriteMap φ.idxOfFVar) ▹ φ

Foundation/Syntax/Predicate/Rew.lean

@@ -26,7 +26,9 @@ namespace FirstOrder
 
 /--
 A structure for maps which rewrite the semiterms occurring in a term.
+
 toFun - A function from `Semiterm L ξ₁ n₁` to `Semiterm L ξ₂ n₂`.
+
 func'' - A proof that `toFun` respects the function symbols of `L`.
 -/
 structure Rew (L : Language) (ξ₁ : Type*) (n₁ : ℕ) (ξ₂ : Type*) (n₂ : ℕ) where
@@ -95,7 +97,7 @@ def rewriteMap (e : ξ₁ → ξ₂) : Rew L ξ₁ n ξ₂ n := rewrite (fun m =
 def map (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) : Rew L ξ₁ n₁ ξ₂ n₂ :=
   bind (fun n => #(b n)) (fun m => &(e m))
 
-/-- `LO.FirstOrder.Rew.subst v` is a substitution of the bounded variables occurring in a term by `v : Fin n → Semiterm L ξ n'`. -/
+/-- `LO.FirstOrder.Rew.subst v` is a substitution of the bound variables occurring in a term by `v : Fin n → Semiterm L ξ n'`. -/
 def subst {n'} (v : Fin n → Semiterm L ξ n') : Rew L ξ n ξ n' :=
   bind v fvar
 
@@ -119,6 +121,8 @@ def cast {n n' : ℕ} (h : n = n') : Rew L ξ n ξ n' :=
 def castLE {n n' : ℕ} (h : n ≤ n') : Rew L ξ n ξ n' :=
   map (Fin.castLE h) id
 
+/-- `LO.FirstOrder.Rew.embSubsts v` is a substitution of the bound variables occurring in a term with no free variables by `v : Fin n → Semiterm L ξ n'`.
+This closely resembles `LO.FirstOrder.Rew.subst`, however the term is required to have free variables of type `Empty`. -/
 def embSubsts (v : Fin k → Semiterm L ξ n) : Rew L Empty k ξ n := Rew.bind v Empty.elim
 
 protected def q (ω : Rew L ξ₁ n₁ ξ₂ n₂) : Rew L ξ₁ (n₁ + 1) ξ₂ (n₂ + 1) :=

Foundation/Syntax/Predicate/Term.lean

@@ -232,12 +232,12 @@ def fvarList : Semiterm L ξ n → List ξ
 
 def idxOfFVar [DecidableEq ξ] (t : Semiterm L ξ n) : ξ → ℕ := t.fvarList.idxOf
 
-def enumarateFVar [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ :=
+def enumerateFVar [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ :=
   fun i ↦ if hi : i < t.fvarList.length then t.fvarList.get ⟨i, hi⟩ else default
 
-lemma enumarateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) :
-    enumarateFVar t (idxOfFVar t x) = x := by
-  simpa [enumarateFVar, idxOfFVar]
+lemma enumerateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) :
+    enumerateFVar t (idxOfFVar t x) = x := by
+  simpa [enumerateFVar, idxOfFVar]
   using fun h ↦ False.elim <| not_le.mpr (List.idxOf_lt_length_iff.mpr $ hx) h
 
 lemma mem_fvarList_iff_fvar? [DecidableEq ξ] {t : Semiterm L ξ n} : x ∈ t.fvarList ↔ t.FVar? x:= by

Foundation/Vorspiel/List/Basic.lean

@@ -152,7 +152,7 @@ lemma remove_cons_subset_cons_remove (a b) (l : List α) :
   simp only [mem_remove_iff, mem_cons, ne_eq, and_imp]
   rintro (rfl | hx) nex <;> simp [*]
 
-lemma remove_map_substet_map_remove [DecidableEq β] (f : α → β) (l : List α) (a) :
+lemma remove_map_subset_map_remove [DecidableEq β] (f : α → β) (l : List α) (a) :
     (l.map f).remove (f a) ⊆ (l.remove a).map f := by
   simp only [subset_def, mem_remove_iff, mem_map, ne_eq, and_imp, forall_exists_index,
     forall_apply_eq_imp_iff₂]