-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → Quiver.Hom.{?u.292990, max u (?u.292990 + 1)} M (X i).toModuleCat
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cone
    (F ⋙
      forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
        (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
        (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦
        (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD := ModuleCat.carrier))
hc : IsLimit c
s : Cone F
i : J
rw :
  Continuous (X := (↑(toModuleCat s.1) : Type u_3)) (Y := (↑(F.obj i).toModuleCat : Type u_3))
    (Function.comp (β := (↑(ofCone c).pt.toModuleCat : Type u_3))
        (⇑(hom (FC := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CC :=
              ModuleCat.carrier) (c.π.app i)) :
          (a : (↑c.1 : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
        (AddHom.toFun
          (LinearMap.toAddHom.{u, u, u_3, u_3} (R := R) (S := R) (σ := RingHom.id R)
            (ModuleCat.Hom.hom
              (hc.lift
                (Functor.mapCone
                  (forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
                    (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC :=
                    fun (X : TopModuleCat.{u_3, u} R) ↦ (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD :=
                    fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD :=
                    ModuleCat.carrier))
                  s))))) :
      (↑s.1.1 : Type u_3) → (↑(F.obj i).toModuleCat : Type u_3))
⊢ TopologicalSpace.coinduced (X := (↑s.1.1 : Type u_3))
      (AddHom.toFun
          (LinearMap.toAddHom.{u, u, u_3, u_3} (R := R) (S := R) (σ := RingHom.id R)
            (ModuleCat.Hom.hom
              (hc.lift
                (Functor.mapCone
                  (forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
                    (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC :=
                    fun (X : TopModuleCat.{u_3, u} R) ↦ (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD :=
                    fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD :=
                    ModuleCat.carrier))
                  s)))) :
        (↑s.1.1 : Type u_3) → (↑(ofCone c).pt.toModuleCat : Type u_3))
      (topologicalSpace s.1 : TopologicalSpace (↑(toModuleCat s.1) : Type u_3)) ≤
    TopologicalSpace.induced
      (⇑(hom (FC := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CC :=
            ModuleCat.carrier) (c.π.app i)) :
        (a : (↑c.1 : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
      (F.obj i).topologicalSpace

Tactic:
rw [coinduced_le_iff_le_induced, induced_compose, ← continuous_iff_le_induced]

Premises used: induced_compose, continuous_iff_le_induced, coinduced_le_iff_le_induced