refactor(Vorspiel): rename clashing Matrix.map/forall_iff/exists_iff to vec* (Mathlib co-import)

Foundation/FirstOrder/Basic/BinderNotation.lean

@@ -45,14 +45,14 @@ lemma eval_nestFormulae {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L
 
 @[simp] lemma eval_nestFormulae₁ {φ : Semiformula L ξ 1} {ψ : Semiformula L ξ (m + 1)} :
     Eval e f (φ.nestFormulae ![ψ]) ↔ ∀ x : M, Eval (x :> e) f ψ → Eval ![x] f φ := by
-  simp [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq]
+  simp [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq]
 
 @[simp] lemma eval_nestFormulae₂ {φ : Semiformula L ξ 2} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} :
     Eval e f (φ.nestFormulae ![ψ₁, ψ₂]) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![x₁, x₂] f φ := by
   suffices
     (∀ x₁ x₂, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval ![x₁, x₂] f φ) ↔
     ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![x₁, x₂] f φ by
-    simpa [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_two]
+    simpa [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_two]
   grind
 
 @[simp] lemma eval_nestFormulae₃ {φ : Semiformula L ξ 3} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} :
@@ -61,7 +61,7 @@ lemma eval_nestFormulae {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L
   suffices
     (∀ x₁ x₂ x₃, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval (x₃ :> e) f ψ₃ → Eval ![x₁, x₂, x₃] f φ) ↔
     ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → ∀ x₃, Eval (x₃ :> e) f ψ₃ → Eval ![x₁, x₂, x₃] f φ by
-    simpa [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
+    simpa [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
   grind
 
 @[simp] lemma eval_nestFormulae₄ {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} :
@@ -83,7 +83,7 @@ lemma eval_nestFormulae {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L
       ∀ x₃, Eval (x₃ :> e) f ψ₃ →
       ∀ x₄, Eval (x₄ :> e) f ψ₄ →
       Eval ![x₁, x₂, x₃, x₄] f φ) by
-    simpa [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
+    simpa [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
   grind
 
 lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semiformula L ξ (m + 1)} :
@@ -96,14 +96,14 @@ lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semi
 
 @[simp] lemma eval_nestFormulaeFunc₁ {φ : Semiformula L ξ 2} {ψ : Semiformula L ξ (m + 1)} :
     Eval (z :> e) f (φ.nestFormulaeFunc ![ψ]) ↔ ∀ x, Eval (x :> e) f ψ → Eval ![z, x] f φ := by
-  simp [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq]
+  simp [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq]
 
 @[simp] lemma eval_nestFormulaeFunc₂ {φ : Semiformula L ξ 3} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} :
     Eval (z :> e) f (φ.nestFormulaeFunc ![ψ₁, ψ₂]) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![z, x₁, x₂] f φ := by
   suffices
     (∀ x₁ x₂, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval ![z, x₁, x₂] f φ) ↔
     ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![z, x₁, x₂] f φ by
-    simpa [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_two]
+    simpa [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_two]
   grind
 
 @[simp] lemma eval_nestFormulaeFunc₃ {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} :
@@ -112,7 +112,7 @@ lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semi
   suffices
     (∀ x₁ x₂ x₃, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval (x₃ :> e) f ψ₃ → Eval ![z, x₁, x₂, x₃] f φ) ↔
     ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → ∀ x₃, Eval (x₃ :> e) f ψ₃ → Eval ![z, x₁, x₂, x₃] f φ by
-    simpa [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
+    simpa [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
   grind
 
 @[simp] lemma eval_nestFormulaeFunc₄ {φ : Semiformula L ξ 5} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} :
@@ -134,7 +134,7 @@ lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semi
       ∀ x₃, Eval (x₃ :> e) f ψ₃ →
       ∀ x₄, Eval (x₄ :> e) f ψ₄ →
       Eval ![z, x₁, x₂, x₃, x₄] f φ) by
-    simpa [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
+    simpa [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ]
   grind
 
 end Semiformula

Foundation/FirstOrder/Basic/Semantics/Semantics.lean

@@ -278,25 +278,25 @@ lemma eval_nrel' {r : L.Rel k} {v} :
     Eval b f (∀⁰* φ) ↔ ∀ e', Eval e' f φ :=
   match k with
   |     0 => by simp [eq_finZeroElim]
-  | k + 1 => by simpa [allClosure_succ, eval_allClosure (k := k), Matrix.forall_iff] using forall_comm
+  | k + 1 => by simpa [allClosure_succ, eval_allClosure (k := k), Matrix.vecForall_iff] using forall_comm
 
 @[simp] lemma eval_exsClosure {b} {φ : Semiformula L ξ k} :
     Eval b f (∃⁰* φ) ↔ ∃ e', Eval e' f φ :=
   match k with
   |     0 => by simp [eq_finZeroElim]
-  | k + 1 => by simpa [exsClosure_succ, eval_exsClosure (k := k), Matrix.exists_iff] using exists_comm
+  | k + 1 => by simpa [exsClosure_succ, eval_exsClosure (k := k), Matrix.vecExists_iff] using exists_comm
 
 @[simp] lemma eval_allItr {b} {φ : Semiformula L ξ (n + k)} :
     Eval b f (∀⁰^[k] φ) ↔ ∀ e', Eval (Matrix.appendr e' b) f φ :=
   match k with
   |     0 => by simp [Matrix.empty_eq]
-  | k + 1 => by simpa [allItr_succ, eval_allItr (k := k), Matrix.forall_iff] using forall_comm
+  | k + 1 => by simpa [allItr_succ, eval_allItr (k := k), Matrix.vecForall_iff] using forall_comm
 
 @[simp] lemma eval_exsItr {b} {φ : Semiformula L ξ (n + k)} :
     Eval b f (∃⁰^[k] φ) ↔ ∃ e', Eval (Matrix.appendr e' b) f φ :=
   match k with
   |     0 => by simp [Matrix.empty_eq]
-  | k + 1 => by simpa [exsItr_succ, eval_exsItr (k := k), Matrix.exists_iff] using exists_comm
+  | k + 1 => by simpa [exsItr_succ, eval_exsItr (k := k), Matrix.vecExists_iff] using exists_comm
 
 section rew
 

Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean

@@ -129,7 +129,7 @@ theorem bold_sigma_one_complete {n} {φ : ArithmeticSemisentence n} (hp : Hierar
       apply ball_intro
       intro i hi
       suffices T.internalize V ⊢ (toNumVec (i :> w) ⤔ ⌜φ⌝) by
-        simpa [Semiformula.substs_substs, Matrix.map_map_comp']
+        simpa [Semiformula.substs_substs, Matrix.vecMap_vecMap_comp']
       exact ih (h i hi)
     exact ball_replace T ((toNumVec w).q ⤔ ⌜φ⌝) _ _ ⨀ (eq_comm <| term_complete T t w) ⨀ this
   case hExs =>
@@ -139,7 +139,7 @@ theorem bold_sigma_one_complete {n} {φ : ArithmeticSemisentence n} (hp : Hierar
     suffices T.internalize V ⊢ ∃⁰ ((toNumVec w).q ⤔ ⌜φ⌝) by simpa
     apply TProof.exs! (𝕹 i)
     suffices T.internalize V ⊢ (toNumVec (i :> w) ⤔ ⌜φ⌝) by
-      simpa [Semiformula.substs_substs, Matrix.map_map_comp']
+      simpa [Semiformula.substs_substs, Matrix.vecMap_vecMap_comp']
     exact ih hφ
 
 theorem sigma_one_provable_of_models {σ : ArithmeticSentence} (hσ : Hierarchy 𝚺 1 σ) :

Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Typed.lean

@@ -310,11 +310,11 @@ noncomputable def substItrDisj (w : SemitermVec V ℒₒᵣ m n) (φ : Semiformu
 
 @[simp] lemma substItrConj_free (w : SemitermVec V ℒₒᵣ m 1) (φ : Semiformula V ℒₒᵣ (m + 1)) (z : V) :
     (φ.substItrConj w z).free = φ.shift.substItrConj (Semiterm.free⨟ w) z := by
-  unfold free; simp [Matrix.map_map_comp']; rfl
+  unfold free; simp [Matrix.vecMap_vecMap_comp']; rfl
 
 @[simp] lemma substItrDisj_free (w : SemitermVec V ℒₒᵣ m 1) (φ : Semiformula V ℒₒᵣ (m + 1)) (z : V) :
     (φ.substItrDisj w z).free = φ.shift.substItrDisj (Semiterm.free⨟ w) z := by
-  unfold free; simp [Matrix.map_map_comp']; rfl
+  unfold free; simp [Matrix.vecMap_vecMap_comp']; rfl
 
 end Semiformula
 

Foundation/Vorspiel/Matrix.lean

@@ -232,11 +232,15 @@ def appendr {n m} (v : Fin n → α) (w : Fin m → α) : Fin (m + n) → α :=
 
 @[simp] lemma appendr_cons {m n} (x : α) (v : Fin n → α) (w : Fin m → α) : appendr (x :> v) w = x :> appendr v w := by funext i; simp [appendr]
 
-lemma forall_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :
+-- Renamed from `Matrix.forall_iff` to `Matrix.vecForall_iff` to avoid clashing with
+-- Mathlib's `Matrix.forall_iff` (Mathlib.Data.Matrix.Reflection), which otherwise makes
+-- Foundation unimportable alongside that module.
+lemma vecForall_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :
     (∀ v, φ v) ↔ (∀ a, ∀ v, φ (a :> v)) :=
   ⟨fun h a v ↦ h (a :> v), fun h v ↦ by simpa [eq_vecCons v] using h (v 0) (v ∘ Fin.succ)⟩
 
-lemma exists_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :
+-- Renamed from `Matrix.exists_iff` to `Matrix.vecExists_iff`; see `vecForall_iff` above.
+lemma vecExists_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :
     (∃ v, φ v) ↔ (∃ a, ∃ v, φ (a :> v)) :=
   ⟨by rintro ⟨v, hv⟩; exact ⟨v 0, v ∘ Fin.succ, by simpa [eq_vecCons] using hv⟩,
    by rintro ⟨a, v, hv⟩; exact ⟨_, hv⟩⟩
@@ -245,33 +249,36 @@ def foldr (f : α → β → β) (init : β) : {k : ℕ} → (Fin k → α) →
   |     0, _ => init
   | _ + 1, v => f (vecHead v) (Matrix.foldr f init (vecTail v))
 
-def map (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v
+-- Renamed from `Matrix.map` to `Matrix.vecMap` to avoid clashing with Mathlib's
+-- `Matrix.map`: both auto-generate `Matrix.map.eq_1`, which makes Foundation
+-- unimportable alongside Mathlib matrix/analysis theory (e.g. Bochner integration).
+def vecMap (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v
 
-section map
+section vecMap
 
-postfix:max "⨟" => map
+postfix:max "⨟" => vecMap
 
 variable (f : α → β)
 
-@[simp] lemma map_nil (v : Fin 0 → α) : f⨟ v = ![] := empty_eq (f⨟ v)
+@[simp] lemma vecMap_nil (v : Fin 0 → α) : f⨟ v = ![] := empty_eq (f⨟ v)
 
-@[simp] lemma map_cons (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v := by
+@[simp] lemma vecMap_cons (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v := by
   ext i
-  cases i using Fin.cases <;> simp [map]
+  cases i using Fin.cases <;> simp [vecMap]
 
-@[simp] lemma map_cons' (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v) := by
+@[simp] lemma vecMap_cons' (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v) := by
   ext i
-  cases i using Fin.cases <;> { simp [map]; rfl }
+  cases i using Fin.cases <;> { simp [vecMap]; rfl }
 
-@[simp] lemma map_app (v : Fin k → α) (i : Fin k) : (f⨟ v) i = f (v i) := rfl
+@[simp] lemma vecMap_app (v : Fin k → α) (i : Fin k) : (f⨟ v) i = f (v i) := rfl
 
-lemma map_map_comp (g : β → γ) (f : α → β) (v : Fin k → α) :
+lemma vecMap_vecMap_comp (g : β → γ) (f : α → β) (v : Fin k → α) :
     g⨟ (f⨟ v) = (g ∘ f)⨟ v := by ext x; simp
 
-lemma map_map_comp' (g : β → γ) (f : α → β) (v : Fin k → α) :
+lemma vecMap_vecMap_comp' (g : β → γ) (f : α → β) (v : Fin k → α) :
     g⨟ (f⨟ v) = (fun x ↦ g (f x))⨟ v := by ext x; simp
 
-end map
+end vecMap
 section foldr
 
 variable (f : α → β → β) (init : β)