fix: Iso.hom_inv_id, remove show/simp, change for lint

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -195,7 +195,7 @@ theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
     -- 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
+    simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id] at key
     exact key
   · -- SURJECTIVITY (proved 2026-06-13)
     intro h
@@ -246,7 +246,6 @@ lemma isSolid_of_isLimit_gen
   constructor
   · 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; coerce, then congr_arg avoids ← assoc one-occurrence problem
     have hfg' : sol ≫ f = sol ≫ g := hfg
     have key := congr_arg (· ≫ c.π.app j) hfg'
@@ -267,7 +266,7 @@ lemma isSolid_of_isLimit_gen
                   change 𝟙 _ ≫ g_j k = g_j j ≫ F.map φ
                   simp only [Category.id_comp]; exact (compat φ).symm } }
     refine ⟨hc.lift g_cone, ?_⟩
-    show sol ≫ hc.lift g_cone = h_map
+    change sol ≫ hc.lift g_cone = h_map
     apply hc.hom_ext; intro j
     have hfac : hc.lift g_cone ≫ c.π.app j = g_j j := hc.fac g_cone j
     rw [Category.assoc, hfac]; exact hg_j' j
@@ -298,7 +297,8 @@ theorem profiniteSolid_obj_isSolid (S : Profinite.{u}) :
   change (E.coneAt S).pt.IsSolid
   apply isSolid_of_isLimit_gen R (E.coneAt S) h_pwise
   intro f
-  simp only [Functor.comp_obj, StructuredArrow.proj_obj]
+  -- Use exact with definitional equality rather than simp;
+  -- (F ⩙ G).obj j and StructuredArrow.proj .obj j unfold definitionally
   exact finFree_isSolid R f.right
 
 end CondensedMod