-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
refine :
  IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology LightProfinite) (Type u))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (op (LightProfinite.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit
        (constantSheafAdj (coherentTopology LightProfinite) (Type u)
          (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
      (obj
        (sheafCompose (coherentTopology LightProfinite)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
⊢ IsIso (C := LightCondSet) (X :=
    obj (C := LightCondMod R)
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (obj (Functor.const LightProfiniteᵒᵖ)
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (op (LightProfinite.of PUnit.{u + 1}))))))
    (Y :=
    obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))
    (CategoryStruct.comp (Y :=
        obj
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
              (CC := ModuleCat.carrier) ⋙
            constantSheaf (coherentTopology LightProfinite) (Type u))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (op (LightProfinite.of PUnit.{u + 1}))))
        (NatTrans.app
          (Iso.hom
            (constantCommuteCompose (coherentTopology LightProfinite)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier))))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (op (LightProfinite.of PUnit.{u + 1}))))
        (NatTrans.app
          (Adjunction.counit
            (constantSheafAdj (coherentTopology LightProfinite) (Type u)
              (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
          (obj
            (sheafCompose (coherentTopology LightProfinite)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier)))
            (obj (functor R) M))) :
      obj
          (constantSheaf (coherentTopology LightProfinite) (ModuleCat R) ⋙
            sheafCompose (coherentTopology LightProfinite)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier)))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (op (LightProfinite.of PUnit.{u + 1}))) ⟶
        obj (𝟭 (Sheaf (coherentTopology LightProfinite) (Type u)))
          (obj
            (sheafCompose (coherentTopology LightProfinite)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := ModuleCat.carrier)))
            (obj (functor R) M)))

Tactic:
refine IsIso.comp_isIso' inferInstance ?_

Premises used: inferInstance, CategoryTheory.IsIso.comp_isIso'