fix: port to Lean v4.33.1 (toolchain, manifest, tactic adaptations)

ModalLogicArchive/Logic/Semantics.lean

@@ -216,7 +216,8 @@ instance empty' (𝓜 : M) : 𝓜 ⊧* (∅ : Set F) := ⟨by simp⟩
     𝓜 ⊧* Set.range φ ↔ ∀ i, 𝓜 ⊧ φ i := by simp [modelsSet_iff]
 
 @[simp] lemma setOf_iff {P : F → Prop} {𝓜 : M} :
-    𝓜 ⊧* setOf P ↔ ∀ φ, P φ → 𝓜 ⊧ φ := by simp [modelsSet_iff]
+    𝓜 ⊧* setOf P ↔ ∀ φ, P φ → 𝓜 ⊧ φ := by
+  rw [modelsSet_iff]; exact ⟨fun h φ hP => h hP, fun h φ hP => h φ hP⟩
 
 end ModelsSet
 

ModalLogicArchive/Modal/LogicSymbol.lean

@@ -344,7 +344,7 @@ prefix:90 "□'" => List.LO.box
 
 @[simp, grind =] lemma boxItr_nil : (□^[n]'([] : List F)) = [] := by rfl
 
-@[simp, grind =] lemma boxItr_single : (□^[n]'[φ]) = [□^[n]φ] := by dsimp [boxItr];
+@[simp, grind =] lemma boxItr_single : (□^[n]'[φ]) = [□^[n]φ] := by simp [boxItr];
 
 @[simp, grind =] lemma eq_boxItr_conn : (□^[n]'(ψ :: s)) = (□^[n]ψ) :: (□^[n]'s) := by induction s <;> simp_all [boxItr];
 @[simp, grind =] lemma eq_box_conn : (□' (ψ :: s)) = (□ψ) :: □'s := eq_boxItr_conn (n := 1)
@@ -427,7 +427,7 @@ prefix:90 "◇'⁻¹" => List.LO.predia
 @[simp, grind =] lemma diaItr_nil : (◇^[n]'([] : List F)) = [] := by rfl
 @[simp, grind =] lemma prediaItr_nil : (◇⁻¹^[n]'([] : List F)) = [] := by rfl
 
-@[simp, grind =] lemma diaItr_single : (◇^[n]'[φ]) = [◇^[n]φ] := by dsimp [diaItr];
+@[simp, grind =] lemma diaItr_single : (◇^[n]'[φ]) = [◇^[n]φ] := by simp [diaItr];
 
 @[simp, grind =] lemma eq_diaItr_conn : (◇^[n]'(ψ :: s)) = (◇^[n]ψ) :: (◇^[n]'s) := by induction s <;> simp_all [diaItr];
 @[simp, grind =] lemma eq_dia_conn : (◇' (ψ :: s)) = (◇ψ) :: ◇'s := eq_diaItr_conn (n := 1)

ModalLogicArchive/Vorspiel/AdjunctiveSet.lean

@@ -24,6 +24,7 @@ class AdjunctiveSet (β : outParam Type*) (α : Type*) extends Membership β α,
 attribute [simp] AdjunctiveSet.not_mem_empty AdjunctiveSet.mem_cons_iff
 
 instance Set.adjunctiveSet : AdjunctiveSet α (Set α) where
+  toHasSubset := ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩
   subset_iff := iff_of_eq Set.subset_def
   not_mem_empty := by simp
   mem_cons_iff := by simp [Adjoin.adjoin]
@@ -39,6 +40,7 @@ instance Multiset.adjunctiveSet : AdjunctiveSet α (Multiset α) where
   mem_cons_iff := by simp [Adjoin.adjoin]
 
 instance Finset.adjunctiveSet [DecidableEq α] : AdjunctiveSet α (Finset α) where
+  toHasSubset := ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩
   subset_iff := Finset.subset_iff
   not_mem_empty := by simp
   mem_cons_iff := by simp [Adjoin.adjoin]

Neighborhood/Semantics/AxiomN.lean

@@ -52,6 +52,16 @@ instance {P : MaximalConsistentSet L → Set (Proofset L)} [L.HasAxiomN] :
   apply iff_of_true _ (Set.mem_univ Ω)
   exact Or.inl ⟨⊤, MaximalConsistentSet.mem_of_prove (by simp), by simp⟩
 
+/-- Direct instance on the abbrev head: under Lean v4.33, instance search no longer unfolds
+`intermediateRelativeMaximalCanonicalModel` (an abbrev of `relativeBasicCanonicalModel`) to match
+the general instance above. -/
+instance [L.HasAxiomN] :
+    (intermediateRelativeMaximalCanonicalModel L).ContainsUnit := by
+  constructor
+  ext Ω
+  apply iff_of_true _ (Set.mem_univ Ω)
+  exact Or.inl ⟨⊤, MaximalConsistentSet.mem_of_prove (by simp), by simp⟩
+
 end
 
 end

Neighborhood/Semantics/Completeness.lean

@@ -260,13 +260,9 @@ abbrev minimalRelativeMaximalCanonicalModel (L : Logic α) [L.Cl] [L.HasRE] [Non
   relativeBasicCanonicalModel L (fun _ _ => False)
 
 lemma minimalRelativeMaximalCanonicalModel.iff_minimal :
-  Ω ∈ (minimalRelativeMaximalCanonicalModel L).box X ↔ Ω ∈ (basicCanonicalModel L).box X := by
-  rw [relativeBasicCanonicalModel.iff_mem_box]
-  constructor
-  · rintro (h | ⟨_, h⟩)
-    · exact h
-    · exact h.elim
-  · exact Or.inl
+  Ω ∈ (minimalRelativeMaximalCanonicalModel L).box X ↔ Ω ∈ (basicCanonicalModel L).box X :=
+  (relativeBasicCanonicalModel.iff_mem_box (P := fun _ _ => False)).trans
+    ⟨fun h => h.elim id (fun ⟨_, h'⟩ => h'.elim), fun h => Or.inl h⟩
 
 /-- `relativeBasicCanonicalModel` with every non-proofset as an extra neighborhood. -/
 abbrev maximalRelativeMaximalCanonicalModel (L : Logic α) [L.Cl] [L.HasRE] [Nonempty (MaximalConsistentSet L)] :

Neighborhood/Semantics/Filtration.lean

@@ -385,7 +385,9 @@ lemma iff_mem_B :
       apply minimalFiltration.iff_mem_B.mpr;
       use φ;
     . right;
-      suffices (∃ Y, 【M (□φ)】 = (minimalFiltration M T).B Y) ∧ W ∈ 【M (□φ)】 by simpa;
+      suffices (∃ Y, 【M (□φ)】 = (minimalFiltration M T).B Y) ∧ W ∈ 【M (□φ)】 by
+        rw [if_pos this.1];
+        exact this.2;
       constructor;
       . use (【M.truthset φ】);
         rw [Filtration.box_in_out hφ]
@@ -575,7 +577,12 @@ def quasiFilteringTransitiveFiltration (M : Model κ α) [M.IsMonotonic] [M.IsTr
               (∀ ξ, □ξ ∈ T → 【M (□ξ)】 ∈ Ys → W ∈ 【M (□ξ)】 → A ∈ 【M (□ξ)】) ↔
               (∀ ξ, □ξ ∈ T → ∀ Yi ∈ Ys, Yi = 【M (□ξ)】 → W ∈ 【M (□ξ)】 → A ∈ Yi) by
               simp [Ξ, Us];
-              tauto;
+              constructor;
+              . rintro h i hi;
+                rcases Finset.mem_filter.mp hi with ⟨hiYs, ψ, hψ, rfl, hW⟩;
+                exact h ψ hψ hiYs hW;
+              . rintro h a ha hYs hW;
+                exact h _ (Finset.mem_filter.mpr ⟨hYs, a, ha, rfl, hW⟩);
             constructor;
             . rintro h _ _ _ _ rfl;
               apply h <;> assumption;
@@ -588,7 +595,12 @@ def quasiFilteringTransitiveFiltration (M : Model κ α) [M.IsMonotonic] [M.IsTr
               (∀ ψ, □ψ ∈ T → 【M ψ】 ∈ Ys → W ∈ 【M (□ψ)】 → A ∈ 【M ψ】) ↔
               (∀ ψ, □ψ ∈ T → ∀ Yi ∈ Ys, Yi = 【M ψ】 → W ∈ 【M (□ψ)】 → A ∈ Yi) by
               simp [Ψ, Vs];
-              tauto;
+              constructor;
+              . rintro h i hi;
+                rcases Finset.mem_filter.mp hi with ⟨hiYs, ψ, hψ, rfl, hW⟩;
+                exact h ψ hψ hiYs hW;
+              . rintro h a ha hYs hW;
+                exact h _ (Finset.mem_filter.mpr ⟨hYs, a, ha, rfl, hW⟩);
             constructor;
             . rintro h _ _ _ _ rfl;
               apply h <;> assumption;
@@ -692,10 +704,18 @@ def quasiFilteringTransitiveFiltration (M : Model κ α) [M.IsMonotonic] [M.IsTr
           rw [eYVU, this.1, this.2];
           exact Finset.union_empty _;
         constructor;
-        . suffices ∀ Yi ∈ Ys, ∀ ψ, □ψ ∈ T → Yi = 【M ψ】 → ⟦w⟧ ∉ 【M (□ψ)】 by simpa [Vs];
+        . suffices ∀ Yi ∈ Ys, ∀ ψ, □ψ ∈ T → Yi = 【M ψ】 → ⟦w⟧ ∉ 【M (□ψ)】 by
+            simp only [Vs, Finset.eq_empty_iff_forall_notMem];
+            rintro Yi hi;
+            rcases Finset.mem_filter.mp hi with ⟨hYi, ψ, hψ, rfl, hw⟩;
+            exact this _ hYi ψ hψ rfl hw;
           rintro Yi hYi ψ hψ rfl hw;
           exact hΨ ⟨⟨ψ, hψ, ⟨_, hYi, rfl⟩, hw⟩⟩;
-        . suffices ∀ Yi ∈ Ys, ∀ ξ, □ξ ∈ T → Yi = 【M (□ξ)】 → ⟦w⟧ ∉ 【M (□ξ)】 by simpa [Us];
+        . suffices ∀ Yi ∈ Ys, ∀ ξ, □ξ ∈ T → Yi = 【M (□ξ)】 → ⟦w⟧ ∉ 【M (□ξ)】 by
+            simp only [Us, Finset.eq_empty_iff_forall_notMem];
+            rintro Yi hi;
+            rcases Finset.mem_filter.mp hi with ⟨hYi, ξ, hξ, rfl, hw⟩;
+            exact this _ hYi ξ hξ rfl hw;
           rintro Yi hYi ξ hξ rfl hw;
           exact hΞ ⟨⟨ξ, hξ, ⟨_, hYi, rfl⟩, hw⟩⟩;
     . intro h;