refine deprecation fix: faithful binders + keep one-liners

- CoherenceSpace.symmetric: back to strict-implicit ⦃x y⦄ (matches the old
  `Symmetric` def exactly), so ⟨symmetric⟩ and `symmetric h` compile unchanged
- ChainI: project the class hypotheses directly with dot-notation
  (IR.irrefl _ hR, TR.trans _ _ _ …) instead of `letI := _; exact Class.method`,
  restoring the original succinct one-liners

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: gotrevor

Foundation/Semantics/CoherenceSpace/Basic.lean

@@ -18,7 +18,7 @@ class CoherenceSpace (α : Type*) where
   /-- A coherence relation -/
   Coherence : α → α → Prop
   reflexive : ∀ x, Coherence x x
-  symmetric : ∀ x y, Coherence x y → Coherence y x
+  symmetric : ∀ ⦃x y⦄, Coherence x y → Coherence y x
 
 namespace CoherenceSpace
 
@@ -28,11 +28,11 @@ variable {α : Type*} [CoherenceSpace α]
 
 instance : Std.Refl (α := α) Coherence := ⟨reflexive⟩
 
-instance : Std.Symm (α := α) Coherence := ⟨fun x y ↦ symmetric x y⟩
+instance : Std.Symm (α := α) Coherence := ⟨symmetric⟩
 
 @[simp, refl, grind .] protected lemma Coherence.refl (x : α) : x ⁐ x := reflexive x
 
-lemma Coherence.symm {x y : α} : x ⁐ y → y ⁐ x := fun h ↦ symmetric x y h
+lemma Coherence.symm {x y : α} : x ⁐ y → y ⁐ x := fun h ↦ symmetric h
 
 @[grind =] lemma Coherence.symm_iff {x y : α} : x ⁐ y ↔ y ⁐ x := ⟨symm, symm⟩
 

Foundation/Vorspiel/List/ChainI.lean

@@ -54,22 +54,12 @@ lemma not_mem_of_rel (IR : Std.Irrefl R) (TR : IsTrans α R) {a b x : α} {l : L
   |      [] => simp
   | a' :: l =>
     rintro (_ | _)
-    case singleton =>
-      simp
-      intro hR
-      rintro rfl
-      letI := IR
-      exact Std.Irrefl.irrefl _ hR
+    case singleton => simp; intro hR; rintro rfl; exact IR.irrefl _ hR
     case cons a' Raa' h =>
     intro Rxa
-    have : x ≠ a := by
-      rintro rfl
-      letI := IR
-      exact Std.Irrefl.irrefl _ Rxa
+    have : x ≠ a := by rintro rfl; exact IR.irrefl _ Rxa
     have : x ∉ l :=
-      have : R x a' := by
-        letI := TR
-        exact IsTrans.trans _ _ _ Rxa Raa'
+      have : R x a' := TR.trans _ _ _ Rxa Raa'
       not_mem_of_rel IR TR h this
     simp_all