-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
⊢ IsIso (C := CondensedSet) (X :=
    obj (C := CondensedMod R)
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (obj (Functor.const CompHausᵒᵖ)
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))))
    (Y :=
    obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))
    (CategoryStruct.comp (Y :=
        obj
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
              (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
            constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))
        (NatTrans.app
          (Iso.hom
            (constantCommuteCompose (coherentTopology CompHaus)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier))))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))
        (NatTrans.app
          (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
          (obj
            (sheafCompose (coherentTopology CompHaus)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
            (obj (functor R) M))) :
      obj
          (constantSheaf (coherentTopology CompHaus) (ModuleCat R) ⋙
            sheafCompose (coherentTopology CompHaus)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))) ⟶
        obj (𝟭 (Sheaf (coherentTopology CompHaus) (Type (u + 1))))
          (obj
            (sheafCompose (coherentTopology CompHaus)
              (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
            (obj (functor R) M)))
have refine : IsIso (X :=
  obj
    (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
      constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
    ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op (CompHaus.of PUnit.{u + 1}))))
  (NatTrans.app
    (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M)))
Tactic: refine IsIso.comp_isIso' inferInstance ?_