-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
⊢ IsIso (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}))))))
    (CategoryTheory.Functor.map
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (NatTrans.app
        (Adjunction.counit
          (constantSheafAdj (coherentTopology LightProfinite) (ModuleCat R)
            (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
        (obj (functor R) M)))
have rw : 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: rw [← constantSheafAdj_counit_w]