fix(Condensed/Solid): resolve Yoneda-obj type coercion in surjectivity proofs

Root cause: after `rw [isIso_iff_bijective]; intro h`, h has Yoneda-obj type
`(yoneda.obj M).obj (op X)` rather than morphism type `X ⟶ M`. This blocked
composition `h ≫ iso.hom` and broke subsequent `rw` steps.

Fixes:
- `profiniteSolid_fintype_isSolid` surjectivity: bind h via transparent let hm,
  then use congrArg (· ≫ rest) hmid to avoid right-assoc subterm-matching issue
- `finFree_isSolid` surjectivity: bind h via transparent let hh before h ≫ e.inv
- Remove unused `Category.assoc` simp arguments (linter)
- Fix 100-char line length violation

The surj_factor sorry and sol_leftCancel axiom remain as documented.

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -220,34 +220,34 @@ theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
     have key := congrArg (· ≫ (finFree_iso_solid R T).inv) h_step
     simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id] at key
     exact key
-  · -- SURJECTIVITY (proved 2026-06-13)
+  · -- SURJECTIVITY (proved 2026-06-14, congrArg approach)
     intro h
-    -- Translate h to Hom(profiniteFree X, finFree T) via finFree_iso_solid.hom
-    -- Use let (not have) so h' is transparent and h' = h ≫ iso.hom is rfl
+    -- h has Yoneda-obj type after intro; bind as morphism via transparent let
+    let hm : (profiniteFree R).obj X ⟶
+             (profiniteSolid R).obj (FintypeCat.toProfinite.obj T) := h
+    -- h': image of hm under iso_T.hom (transparent let, so h' = hm ≫ iso_T.hom by rfl)
     let h' : (profiniteFree R).obj X ⟶ (finFree R).obj T :=
-      h ≫ (finFree_iso_solid R T).hom
+      hm ≫ (finFree_iso_solid R T).hom
     obtain ⟨U₀, q₀, h₀, hfact⟩ := surj_factor R T X h'
     refine ⟨(profiniteSolid R).map q₀ ≫ (finFree_iso_solid R U₀).hom ≫
             h₀ ≫ (finFree_iso_solid R T).inv, ?_⟩
     have hmid := sol_map_counit R U₀ X q₀
-    -- Prove the key equation using calc to handle associativity cleanly
-    have eq1 : (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
-        (finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv = h :=
-      calc (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
-               (finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv
-          = ((profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
-             (finFree_iso_solid R U₀).hom) ≫ h₀ ≫ (finFree_iso_solid R T).inv := by
-               simp only [Category.assoc]
-        _ = (profiniteFree R).map q₀ ≫ h₀ ≫ (finFree_iso_solid R T).inv := by
-               rw [hmid]
-        _ = ((profiniteFree R).map q₀ ≫ h₀) ≫ (finFree_iso_solid R T).inv := by
-               rw [← Category.assoc]
-        _ = h' ≫ (finFree_iso_solid R T).inv := by
-               rw [← hfact]
-        _ = h := by
-               rw [show h' = h ≫ (finFree_iso_solid R T).hom from rfl,
-                   Category.assoc, (finFree_iso_solid R T).hom_inv_id, Category.comp_id]
-    exact eq1
+    -- Step 1: sol ≫ solid.map q₀ ≫ iso_U₀.hom ≫ h₀ ≫ iso_T.inv
+    --         = profiniteFree.map q₀ ≫ h₀ ≫ iso_T.inv  (via congrArg + hmid)
+    have step1 : (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
+        (finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv =
+        (profiniteFree R).map q₀ ≫ h₀ ≫ (finFree_iso_solid R T).inv := by
+      have key := congrArg (· ≫ h₀ ≫ (finFree_iso_solid R T).inv) hmid
+      exact key
+    -- Step 2: profiniteFree.map q₀ ≫ h₀ ≫ iso_T.inv = h
+    -- (hfact: h' = map q₀ ≫ h₀; h' = hm ≫ iso_T.hom; hm := h; iso cancel)
+    have step2 : (profiniteFree R).map q₀ ≫ h₀ ≫ (finFree_iso_solid R T).inv = h := by
+      have key2 := congrArg (· ≫ (finFree_iso_solid R T).inv) hfact.symm
+      simp only [Category.assoc] at key2
+      -- key2: map q₀ ≫ h₀ ≫ iso_T.inv = h' ≫ iso_T.inv; expand h' to trigger hom_inv_id
+      rw [key2, show h' = hm ≫ (finFree_iso_solid R T).hom from rfl,
+          Category.assoc, (finFree_iso_solid R T).hom_inv_id, Category.comp_id]
+    exact step1.trans step2
 
 /-! ### Limits of solid modules are solid -/
 
@@ -270,7 +270,6 @@ lemma isSolid_of_isLimit_gen
     apply hc.hom_ext; intro j; apply (bijFun j).1
     have hfg' : sol ≫ f = sol ≫ g := hfg
     have key := congrArg (· ≫ 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)
@@ -317,15 +316,15 @@ theorem finFree_isSolid (T : FintypeCat.{u}) : ((finFree R).obj T).IsSolid := by
     have key2 := congrArg (· ≫ e.hom) hfinv
     simp only [Category.assoc, e.inv_hom_id, Category.comp_id] at key2
     exact key2
-  · -- SURJECTIVITY: translate via e.inv, then lift back with e.hom
+  · -- SURJECTIVITY: h has Yoneda-obj type; let-bind as morphism first
     intro h
-    obtain ⟨f', hf'⟩ := hM.2 (h ≫ e.inv)
+    let hh : (profiniteFree R).obj X ⟶ (finFree R).obj T := h
+    obtain ⟨f', hf'⟩ := hM.2 (hh ≫ e.inv)
     refine ⟨f' ≫ e.hom, ?_⟩
-    have hf'' : (profiniteSolidification R).app X ≫ f' = h ≫ e.inv := hf'
+    have hf'' : (profiniteSolidification R).app X ≫ f' = hh ≫ e.inv := hf'
     have key3 := congrArg (· ≫ e.hom) hf''
     simp only [Category.assoc, e.inv_hom_id, Category.comp_id] at key3
-    -- show converts Yoneda goal to direct form so exact key3 matches
-    show (profiniteSolidification R).app X ≫ (f' ≫ e.hom) = h
+    change (profiniteSolidification R).app X ≫ (f' ≫ e.hom) = h
     exact key3
 
 /-! ### General solidness of `profiniteSolid R` -/