awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : I → TopModuleCat R
f_1 : (i : I) → Quiver.Hom.{?u.284171, max u (?u.284171 + 1)} M (X_1 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))
X Y : J
f : X ⟶ Y
x : (↑(Functor.obj (Functor.obj (Functor.const J) (induced c.π.app)) X).toModuleCat : Type u_3)
⊢ Eq (α := (↑(F.obj Y).toModuleCat : Type u_3))
    ((hom (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)) (X := Functor.obj (Functor.obj (Functor.const J) (induced c.π.app)) X) (Y :=
            F.obj Y)
            (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (induced c.π.app)) f ≫ fromInduced c.π.app Y) :
          (a : (↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat : Type u_3)) →
            (↑(F.obj Y).toModuleCat : Type u_3))
        x :
      (↑(F.obj Y).toModuleCat : Type u_3))
    ((hom (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)) (fromInduced c.π.app X ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat : Type u_3)) →
            (↑(F.obj Y).toModuleCat : Type u_3))
        x :
      (↑(F.obj Y).toModuleCat : Type u_3))

Tactic:
congr($(c.π.naturality f).hom x)

Premises used: CategoryTheory.Limits.Cone.π, congrArg, id, CategoryTheory.NatTrans.naturality, ModuleCat.Hom.hom, DFunLike.coe
-- 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_1 : I → TopModuleCat R
f_1 : (i : I) → Quiver.Hom.{?u.284171, max u (?u.284171 + 1)} M (X_1 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))
X Y : J
f : X ⟶ Y
x : (↑(Functor.obj (Functor.obj (Functor.const J) (induced c.π.app)) X).toModuleCat : Type u_3)
⊢ Eq (α := (↑(F.obj Y).toModuleCat : Type u_3))
    ((hom (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)) (X := Functor.obj (Functor.obj (Functor.const J) (induced c.π.app)) X) (Y :=
            F.obj Y)
            (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (induced c.π.app)) f ≫ fromInduced c.π.app Y) :
          (a : (↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat : Type u_3)) →
            (↑(F.obj Y).toModuleCat : Type u_3))
        x :
      (↑(F.obj Y).toModuleCat : Type u_3))
    ((hom (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)) (fromInduced c.π.app X ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat : Type u_3)) →
            (↑(F.obj Y).toModuleCat : Type u_3))
        x :
      (↑(F.obj Y).toModuleCat : Type u_3))

Tactic:
exact congr($(c.π.naturality f).hom x)
-- 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
rw :
  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)) ≤
    instTopologicalSpaceCarrier R (ofCone c).pt
⊢ Continuous (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))

Tactic:
rw [continuous_iff_coinduced_le]

Premises used: continuous_iff_coinduced_le
-- 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
⊢ 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)) ≤
    instTopologicalSpaceCarrier R (ofCone c).pt

Tactic:
le_iInf fun i ↦ ?_

Premises used: iInf, Set.Mem, setOf, le_iInf, OrderDual
-- 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
refine :
  ∀ (i : J),
    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
⊢ 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)) ≤
    instTopologicalSpaceCarrier R (ofCone c).pt

Tactic:
refine le_iInf fun i ↦ ?_

Premises used: le_iInf
-- 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
change :
  Continuous (X := (↑s.pt.toModuleCat : Type u_3)) (Y := (↑(F.obj i).toModuleCat : Type u_3))
    (⇑(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) ≫
            c.π.app i)) :
      (a : (↑((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).pt : Type u_3)) →
        (↑((F ⋙ forget₂ (TopModuleCat R) (ModuleCat R)).obj i) : Type u_3))
⊢ 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))

Tactic:
change Continuous (X := s.pt) (Y := F.obj i)
      (hc.lift ((forget₂ _ (ModuleCat R)).mapCone s) ≫ c.π.app i).hom

Premises used: CategoryTheory.Limits.Cone.π, Continuous, ModuleCat, CategoryTheory.forget₂, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.mapCone, ModuleCat.Hom.hom, DFunLike.coe, CategoryTheory.NatTrans.app, CategoryTheory.Limits.IsLimit.lift
-- 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
x : (↑s.pt.toModuleCat : Type u_3)
⊢ Eq (α := (↑(F.obj i).toModuleCat : Type u_3))
    (((hom (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)) (X := s.pt)
              (ofHom
                    {
                      toLinearMap :=
                        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)),
                      cont := ⋯ } ≫
                  (ofCone c).π.app i :
                s.pt ⟶ F.obj i) :
            (↑s.pt.toModuleCat : Type u_3) →L[R] (↑(F.obj i).toModuleCat : Type u_3)) :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
        x :
      (↑(F.obj i).toModuleCat : Type u_3))
    ((hom (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)) (s.π.app i) :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
        x :
      (↑(F.obj i).toModuleCat : Type u_3))

Tactic:
congr($(hc.fac ((forget₂ _ _).mapCone s) i).hom x)

Premises used: ModuleCat, congrArg, id, TopModuleCat, CategoryTheory.forget₂, CategoryTheory.Functor.mapCone, ModuleCat.Hom.hom, DFunLike.coe, CategoryTheory.Limits.IsLimit.fac
-- 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
x : (↑s.pt.toModuleCat : Type u_3)
⊢ Eq (α := (↑(F.obj i).toModuleCat : Type u_3))
    (((hom (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)) (X := s.pt)
              (ofHom
                    {
                      toLinearMap :=
                        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)),
                      cont := ⋯ } ≫
                  (ofCone c).π.app i :
                s.pt ⟶ F.obj i) :
            (↑s.pt.toModuleCat : Type u_3) →L[R] (↑(F.obj i).toModuleCat : Type u_3)) :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
        x :
      (↑(F.obj i).toModuleCat : Type u_3))
    ((hom (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)) (s.π.app i) :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
        x :
      (↑(F.obj i).toModuleCat : Type u_3))

Tactic:
exact congr($(hc.fac ((forget₂ _ _).mapCone s) i).hom x)
-- 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
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
x : (↑s.pt.toModuleCat : Type u_3)
⊢ Eq (α := (↑(ofCone c).pt.toModuleCat : Type u_3))
    ((hom (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)) m :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(ofCone c).pt.toModuleCat : Type u_3))
        x :
      (↑(ofCone c).pt.toModuleCat : Type u_3))
    (((hom (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)) (X := s.pt) (Y := (ofCone c).pt)
              (ofHom
                  {
                    toLinearMap :=
                      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)),
                    cont := ⋯ } :
                Quiver.Hom (V := TopModuleCat.{u_3, u} R) (of R (↑s.1.1 : Type u_3))
                  (of R (↑(ofCone c).pt.toModuleCat : Type u_3))) :
            (↑s.pt.toModuleCat : Type u_3) →L[R] (↑(ofCone c).pt.toModuleCat : Type u_3)) :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(ofCone c).pt.toModuleCat : Type u_3))
        x :
      (↑(ofCone c).pt.toModuleCat : Type u_3))

Tactic:
congr($(hc.uniq ((forget₂ _ _).mapCone s) ((forget₂ _ _).map m) fun j ↦ ?_).hom x)

Premises used: ModuleCat, congrArg, id, CategoryTheory.Functor.map, CategoryTheory.Limits.IsLimit.uniq, TopModuleCat, CategoryTheory.forget₂, CategoryTheory.Functor.mapCone, ModuleCat.Hom.hom, DFunLike.coe
-- 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.332254, max u (?u.332254 + 1)} M (X i).toModuleCat
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{v, u} R
inst_3 :
  HasLimit
    (F ⋙
      forget₂ (TopModuleCat.{v, u} R) (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)) (ModuleCat.{v, u} R) (FD := fun (x1 x2 : ModuleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CD := ModuleCat.carrier))
⊢ HasLimit F

Tactic:
⟨_, isLimit (limit.isLimit _)⟩

Premises used: TopModuleCat.isLimit, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk