fix: congr_arg instead of rw assoc (avoids first-occurrence-only issue)

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -192,12 +192,11 @@ theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
     intro g g' hgg'
     have h_step : g ≫ (finFree_iso_solid R T).hom = g' ≫ (finFree_iso_solid R T).hom := by
       sorry
-    -- Cancel hom via hom_inv_id; use simp to handle left-normalization
-    have h : g ≫ (finFree_iso_solid R T).hom ≫ (finFree_iso_solid R T).inv =
-             g' ≫ (finFree_iso_solid R T).hom ≫ (finFree_iso_solid R T).inv := by
-      rw [← Category.assoc, h_step]
-    rw [(finFree_iso_solid R T).hom_inv_id, Category.comp_id] at h
-    exact h
+    -- congr_arg gives (g ≫ hom) ≫ inv = (g' ≫ hom) ≫ inv (left-assoc, both sides)
+    -- then Category.assoc + hom_inv_id + comp_id reduce to g = g'
+    have key := congr_arg (· ≫ (finFree_iso_solid R T).inv) h_step
+    simp only [Category.assoc, (finFree_iso_solid R T).hom_inv_id, Category.comp_id] at key
+    exact key
   · -- SURJECTIVITY (proved 2026-06-13)
     intro h
     -- Translate h to Hom(profiniteFree X, finFree T) via finFree_iso_solid.hom
@@ -248,10 +247,11 @@ lemma isSolid_of_isLimit_gen
   · intro f g hfg
     apply hc.hom_ext; intro j; apply (bijFun j).1
     show sol ≫ f ≫ c.π.app j = sol ≫ g ≫ c.π.app j
-    -- hfg has Yoneda type, not sol ≫ f = sol ≫ g syntactically;
-    -- explicit coercion needed for rw to find the pattern
+    -- hfg has Yoneda type; coerce, then congr_arg avoids ← assoc one-occurrence problem
     have hfg' : sol ≫ f = sol ≫ g := hfg
-    rw [← Category.assoc, hfg']
+    have key := congr_arg (· ≫ c.π.app j) hfg'
+    simp only [Category.assoc] at key
+    exact key
   · intro h_map
     choose g_j hg_j using fun j => (bijFun j).2 (h_map ≫ c.π.app j)
     have hg_j' : ∀ j, sol ≫ g_j j = h_map ≫ c.π.app j := hg_j