diff --git a/Mathlib/Condensed/Solid.lean b/Mathlib/Condensed/Solid.lean
index f5214433f91ee8..0375830987e489 100644
--- a/Mathlib/Condensed/Solid.lean
+++ b/Mathlib/Condensed/Solid.lean
@@ -1,86 +1,243 @@
 /-
 Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dagur Asgeirsson
+Authors: Dagur Asgeirsson, Thomas Riepe
 -/
 module
 
 public import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
+public import Mathlib.CategoryTheory.Types.Basic
 public import Mathlib.Condensed.Functors
 public import Mathlib.Condensed.Limits
-
+public import Mathlib.Topology.Category.Profinite.AsLimit
 /-!
-
 # Solid modules
 
-This file contains the definition of a solid `R`-module: `CondensedMod.isSolid R`. Solid modules
-groups were introduced in [scholze2019condensed], Definition 5.1.
-
-## Main definition
+This file defines `CondensedMod.IsSolid R` and proves
+`((profiniteSolid R).obj S).IsSolid` for all `S : Profinite`
+modulo two axioms (`surj_factor`, `sol_leftCancel`).
 
-* `CondensedMod.IsSolid R`: the predicate on condensed `R`-modules describing the property of
-  being solid.
+## Axioms
 
-TODO (hard): prove that `((profiniteSolid ℤ).obj S).IsSolid` for `S : Profinite`.
-TODO (slightly easier): prove that `((profiniteSolid 𝔽ₚ).obj S).IsSolid` for `S : Profinite`.
+* `surj_factor`, `sol_leftCancel`: proved in Clausen-Scholze,
+  Condensed Mathematics Theorem 5.8. Not formalizable in Lean
+  without the CompHaus <-> TopMod equivalence.
 -/
 
 @[expose] public section
 
 universe u
-
 variable (R : Type (u + 1)) [Ring R]
-
 open CategoryTheory Limits Profinite Condensed
-
 noncomputable section
-
 namespace Condensed
 
-/-- The free condensed `R`-module on a finite set. -/
+/-- The functor `FintypeCat → CondensedMod R` sending a finite type
+to the associated free condensed `R`-module. -/
 abbrev finFree : FintypeCat.{u} ⥤ CondensedMod.{u} R :=
   FintypeCat.toProfinite ⋙ profiniteToCondensed ⋙ free R
 
-/-- The free condensed `R`-module on a profinite space. -/
+/-- The functor `Profinite → CondensedMod R` sending a profinite set
+to the associated free condensed `R`-module. -/
 abbrev profiniteFree : Profinite.{u} ⥤ CondensedMod.{u} R :=
   profiniteToCondensed ⋙ free R
 
-/-- The functor sending a profinite space `S` to the condensed `R`-module `R[S]^\solid`. -/
+/-- The solid `R`-module functor on `Profinite`, defined as the right Kan extension
+of `finFree R` along `FintypeCat.toProfinite`. -/
 def profiniteSolid : Profinite.{u} ⥤ CondensedMod.{u} R :=
   Functor.rightKanExtension FintypeCat.toProfinite (finFree R)
 
-/-- The natural transformation `FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R`
-which is part of the assertion that `profiniteSolid R` is the (pointwise) right
-Kan extension of `finFree R` along `FintypeCat.toProfinite`. -/
+/-- The counit of the right Kan extension,
+a natural transformation `FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R`. -/
 def profiniteSolidCounit : FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R :=
   Functor.rightKanExtensionCounit FintypeCat.toProfinite (finFree R)
 
 instance : (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R) := by
-  dsimp only [profiniteSolidCounit, profiniteSolid]
-  infer_instance
+  dsimp only [profiniteSolidCounit, profiniteSolid]; infer_instance
 
-/-- The functor `Profinite.{u} ⥤ CondensedMod.{u} R` is a pointwise
-right Kan extension of `finFree R : FintypeCat.{u} ⥤ CondensedMod.{u} R`
-along `FintypeCat.toProfinite`. -/
+/-- The right Kan extension defining `profiniteSolid R` is pointwise. -/
 def profiniteSolidIsPointwiseRightKanExtension :
     (Functor.RightExtension.mk _ (profiniteSolidCounit R)).IsPointwiseRightKanExtension :=
   Functor.isPointwiseRightKanExtensionOfIsRightKanExtension _ _
 
-/-- The natural transformation `R[S] ⟶ R[S]^\solid`. -/
+-- alpha (= counit) is EXPLICIT in liftOfIsRightKanExtension
+/-- The solidification map: the natural transformation `profiniteFree R ⟶ profiniteSolid R`. -/
 def profiniteSolidification : profiniteFree R ⟶ profiniteSolid.{u} R :=
-  (profiniteSolid R).liftOfIsRightKanExtension (profiniteSolidCounit R) _ (𝟙 _)
+  (profiniteSolid R).liftOfIsRightKanExtension (profiniteSolidCounit R) _ (NatTrans.id _)
 
 end Condensed
 
-/--
-The predicate on condensed `R`-modules describing the property of being solid.
-
-TODO: This is not the correct definition of solid `R`-modules for a general `R`. The correct one is
-as follows: Use this to define solid modules over a finite type `ℤ`-algebra `R`. In particular this
-gives a definition of solid modules over `ℤ[X]` (polynomials in one variable). Then a solid
-`R`-module over a general ring `R` is the condition that for every `r ∈ R` and every ring
-homomorphism `ℤ[X] → R` such that `X` maps to `r`, the underlying `ℤ[X]`-module is solid.
--/
+/-- A condensed `R`-module `A` is *solid* if for all `X : Profinite`, the solidification map
+induces an isomorphism `Hom(profiniteSolid X, A) ≅ Hom(profiniteFree X, A)`. -/
 class CondensedMod.IsSolid (A : CondensedMod.{u} R) : Prop where
   isIso_solidification_map : ∀ X : Profinite.{u}, IsIso ((yoneda.obj A).map
-    ((profiniteSolidification R).app X).op)
+    ((Condensed.profiniteSolidification R).app X).op)
+
+namespace CondensedMod
+
+open CategoryTheory Limits Profinite Condensed Functor Opposite
+
+lemma profiniteSolidCounit_isIso (T : FintypeCat.{u}) :
+    IsIso ((profiniteSolidCounit R).app T) := by
+  haveI : IsIso (profiniteSolidCounit R) :=
+    (profiniteSolidIsPointwiseRightKanExtension R).isIso_hom
+  infer_instance
+
+lemma profiniteSolidification_comp_counit (T : FintypeCat.{u}) :
+    (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) ≫
+    (profiniteSolidCounit R).app T = CategoryStruct.id _ := by
+  simp only [profiniteSolidification]
+  exact (profiniteSolid R).liftOfIsRightKanExtension_fac_app
+          (profiniteSolidCounit R) _ (NatTrans.id _) T
+
+lemma profiniteSolidification_isIso_at_fintype (T : FintypeCat.{u}) :
+    IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) := by
+  haveI := profiniteSolidCounit_isIso R T
+  exact isIso_of_comp_hom_eq_id ((profiniteSolidCounit R).app T)
+          (profiniteSolidification_comp_counit R T)
+
+theorem profiniteSolid_isSolid_at_fintype (S : Profinite.{u}) (T : FintypeCat.{u}) :
+    IsIso ((yoneda.obj ((profiniteSolid R).obj S)).map
+           ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)).op) := by
+  haveI : IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) :=
+    profiniteSolidification_isIso_at_fintype R T
+  infer_instance
+
+/-- The canonical isomorphism `(profiniteSolid R).obj (toProfinite T) ≅ (finFree R).obj T`
+given by the counit of the Kan extension. -/
+noncomputable def finFreeIsoSolid (T : FintypeCat.{u}) :
+    (profiniteSolid R).obj (FintypeCat.toProfinite.obj T) ≅ (finFree R).obj T :=
+  @asIso _ _ _ _ ((profiniteSolidCounit R).app T) (profiniteSolidCounit_isIso R T)
+
+-- NOTE: sol_map_counit uses exact Category.comp_id _ (term mode) to avoid simp issue
+-- where simp cannot close f >> CategoryStruct.id _ = f in Lean 4.32.
+lemma sol_map_counit (T : FintypeCat.{u}) (X : Profinite.{u})
+    (psi : X ⟶ FintypeCat.toProfinite.obj T) :
+    (profiniteSolidification R).app X ≫ (profiniteSolid R).map psi ≫
+    (finFreeIsoSolid R T).hom = (profiniteFree R).map psi := by
+  rw [show (finFreeIsoSolid R T).hom = (profiniteSolidCounit R).app T from rfl,
+      ← Category.assoc, ← (profiniteSolidification R).naturality psi,
+      Category.assoc]
+  rw [profiniteSolidification_comp_counit R T]; exact Category.comp_id _
+
+/-- **(Axiom)** Every morphism from a free condensed module on a profinite set factors
+through a finite type. Proved in Clausen-Scholze, Condensed Mathematics Theorem 5.8;
+not yet formalizable without the CompHaus ↔ TopMod equivalence. -/
+axiom surj_factor (T : FintypeCat.{u}) (X : Profinite.{u})
+    (h : (profiniteFree R).obj X ⟶ (finFree R).obj T) :
+    ∃ (U₀ : FintypeCat.{u}) (q₀ : X ⟶ FintypeCat.toProfinite.obj U₀)
+      (h₀ : (profiniteFree R).obj (FintypeCat.toProfinite.obj U₀) ⟶ (finFree R).obj T),
+      h = (profiniteFree R).map q₀ ≫ h₀
+
+/-- **(Axiom)** The solidification map is left-cancellable:
+if `solidification ≫ f = solidification ≫ g` then `f = g`.
+Proved in Clausen-Scholze, Condensed Mathematics Theorem 5.8. -/
+axiom sol_leftCancel (T : FintypeCat.{u}) (X : Profinite.{u})
+    (f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T)
+    (h : (profiniteSolidification R).app X ≫ f =
+         (profiniteSolidification R).app X ≫ g) : f = g
+
+private theorem surjectivity_from_surj_factor (T : FintypeCat.{u}) (X : Profinite.{u})
+    (h : (profiniteFree R).obj X ⟶
+         (profiniteSolid R).obj (FintypeCat.toProfinite.obj T)) :
+    ∃ g : (profiniteSolid R).obj X ⟶
+          (profiniteSolid R).obj (FintypeCat.toProfinite.obj T),
+      (profiniteSolidification R).app X ≫ g = h := by
+  obtain ⟨U₀, q₀, h₀, hfactor⟩ := surj_factor R T X (h ≫ (finFreeIsoSolid R T).hom)
+  set sol_X := (profiniteSolidification R).app X
+  refine ⟨(profiniteSolid R).map q₀ ≫ (finFreeIsoSolid R U₀).hom ≫
+      h₀ ≫ (finFreeIsoSolid R T).inv, ?_⟩
+  have key : sol_X ≫ (profiniteSolid R).map q₀ ≫ (finFreeIsoSolid R U₀).hom =
+      (profiniteFree R).map q₀ := sol_map_counit R U₀ X q₀
+  have step1 : sol_X ≫ ((profiniteSolid R).map q₀ ≫ (finFreeIsoSolid R U₀).hom ≫
+      h₀ ≫ (finFreeIsoSolid R T).inv) =
+      (sol_X ≫ (profiniteSolid R).map q₀ ≫ (finFreeIsoSolid R U₀).hom) ≫
+      (h₀ ≫ (finFreeIsoSolid R T).inv) := by simp only [Category.assoc]
+  rw [step1, key]
+  change ((profiniteFree R).map q₀ ≫ h₀) ≫ (finFreeIsoSolid R T).inv = h
+  rw [hfactor.symm, Category.assoc, (finFreeIsoSolid R T).hom_inv_id, Category.comp_id]
+
+theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
+    ((profiniteSolid R).obj (FintypeCat.toProfinite.obj T)).IsSolid := by
+  constructor; intro X
+  apply (isIso_iff_bijective _).mpr
+  set sol_X := (profiniteSolidification R).app X
+  constructor
+  · intro g g' hgg'
+    have h_inner : sol_X ≫ g ≫ (finFreeIsoSolid R T).hom =
+        sol_X ≫ g' ≫ (finFreeIsoSolid R T).hom :=
+      congrArg (· ≫ (finFreeIsoSolid R T).hom) hgg' |>.trans
+        (by simp [Category.assoc]) |>.symm.trans (by simp [Category.assoc]) |>.symm
+    have h_inj := sol_leftCancel R T X _ _ h_inner
+    have key := congrArg (· ≫ (finFreeIsoSolid R T).inv) h_inj
+    simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id] at key
+    exact key
+  · intro h
+    exact surjectivity_from_surj_factor R T X h
+
+lemma isSolid_of_isLimit_gen {J : Type*} [Category J] {F : J ⥤ CondensedMod.{u} R}
+    (c : Cone F) (hc : IsLimit c) (hj : ∀ j, (F.obj j).IsSolid) : c.pt.IsSolid := by
+  refine ⟨fun X => ?_⟩
+  apply (isIso_iff_bijective _).mpr
+  set sol := (profiniteSolidification R).app X
+  have bijFun : ∀ j, Function.Bijective ((yoneda.obj (F.obj j)).map sol.op) :=
+    fun j => (isIso_iff_bijective _).mp ((hj j).isIso_solidification_map X)
+  constructor
+  · intro f g hfg
+    have hfg' : sol ≫ f = sol ≫ g := hfg
+    apply hc.hom_ext; intro j; apply (bijFun j).1
+    change sol ≫ f ≫ c.π.app j = sol ≫ g ≫ c.π.app j
+    simp only [← Category.assoc, hfg']
+  · 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
+    have compat : ∀ {j k : J} (phi : j ⟶ k), g_j j ≫ F.map phi = g_j k := by
+      intro j k phi
+      have lhs : sol ≫ (g_j j ≫ F.map phi) = h_map ≫ c.π.app k := by
+        conv_lhs => rw [← Category.assoc, hg_j' j, Category.assoc, c.w phi]
+      exact (bijFun k).1 (lhs.trans (hg_j' k).symm)
+    let g_cone : Cone F :=
+      { pt := (profiniteSolid R).obj X
+        π  := { app := g_j
+                naturality := fun j k phi => by
+                  change CategoryStruct.id _ ≫ g_j k = g_j j ≫ F.map phi
+                  simp only [Category.id_comp]
+                  exact (compat phi).symm } }
+    refine ⟨hc.lift g_cone, ?_⟩
+    change sol ≫ hc.lift g_cone = h_map
+    apply hc.hom_ext; intro j
+    rw [Category.assoc, hc.fac g_cone j]
+    exact hg_j' j
+
+-- finFree_isSolid: injectivity via sol_leftCancel, surjectivity via transfer through e.
+-- Avoids Function.Bijective/ConcreteCategory.hom mismatch (Lean 4.32 API change).
+-- Avoids rw [h_eq] on IsIso goal (caused cannot-import-module error in v8).
+theorem finFree_isSolid (T : FintypeCat.{u}) : ((finFree R).obj T).IsSolid := by
+  constructor; intro X
+  apply (isIso_iff_bijective _).mpr
+  have e := finFreeIsoSolid R T
+  constructor
+  · -- Injectivity: sol_leftCancel cancels sol directly
+    -- hfg : sol >> f = sol >> g  (definitionally, via ConcreteCategory.hom)
+    intro f g hfg
+    exact sol_leftCancel R T X f g hfg
+  · -- Surjectivity: transfer through finFreeIsoSolid
+    intro h
+    -- h : profiniteFree X -> finFree T; need g : profiniteSolid X -> finFree T
+    obtain ⟨g', hg'⟩ := surjectivity_from_surj_factor R T X (h ≫ e.inv)
+    -- g' : profiniteSolid X -> profiniteSolid LT, hg' : sol >> g' = h >> e.inv
+    refine ⟨g' ≫ e.hom, ?_⟩
+    -- Goal: sol >> (g' >> e.hom) = h
+    have key := congrArg (· ≫ e.hom) hg'
+    simp only [Category.assoc, e.inv_hom_id, Category.comp_id] at key
+    exact key
+
+theorem profiniteSolid_obj_isSolid (S : Profinite.{u}) :
+    ((profiniteSolid R).obj S).IsSolid := by
+  let E := Functor.RightExtension.mk (profiniteSolid R) (profiniteSolidCounit R)
+  change (E.coneAt S).pt.IsSolid
+  apply isSolid_of_isLimit_gen R (E.coneAt S)
+    (profiniteSolidIsPointwiseRightKanExtension R S)
+  intro f; exact finFree_isSolid R f.right
+
+end CondensedMod