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
X Y : TopModuleCat.{u_1, u} R
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1)
x : (↑Y.toModuleCat : Type u_1)
⊢ Eq (α := (↑Y.toModuleCat : Type u_1))
    (((@hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
              (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
              (fun (X Y : TopModuleCat.{u_1, u} R) ↦
                (ContinuousLinearMap.funLike :
                  FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                    (↑Y.toModuleCat : Type u_1)))
              _ _ _
              (CategoryStruct.comp (Y := X)
                  (ofHom (↑e.symm : (↑Y.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1)) :
                    Quiver.Hom (V := TopModuleCat.{u_1, u} R) (of R (↑Y.1 : Type u_1)) (of R (↑X.1 : Type u_1)))
                  (ofHom (↑e : (↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1))) :
                Y ⟶ Y) :
            (↑Y.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) :
          (a : (↑Y.toModuleCat : Type u_1)) → (↑Y.toModuleCat : Type u_1))
        x :
      (↑Y.toModuleCat : Type u_1))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
            (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
            (fun (X Y : TopModuleCat.{u_1, u} R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                  (↑Y.toModuleCat : Type u_1)))
            _ _ _ (𝟙 Y : Y ⟶ Y) :
          (a : (↑Y.toModuleCat : Type u_1)) → (↑Y.toModuleCat : Type u_1))
        x :
      (↑Y.toModuleCat : Type u_1))

Tactic:
e.apply_symm_apply _

Premises used: ContinuousLinearEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1)
x : (↑Y.toModuleCat : Type u_1)
⊢ Eq (α := (↑Y.toModuleCat : Type u_1))
    (((@hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
              (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
              (fun (X Y : TopModuleCat.{u_1, u} R) ↦
                (ContinuousLinearMap.funLike :
                  FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                    (↑Y.toModuleCat : Type u_1)))
              _ _ _
              (CategoryStruct.comp (Y := X)
                  (ofHom (↑e.symm : (↑Y.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1)) :
                    Quiver.Hom (V := TopModuleCat.{u_1, u} R) (of R (↑Y.1 : Type u_1)) (of R (↑X.1 : Type u_1)))
                  (ofHom (↑e : (↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1))) :
                Y ⟶ Y) :
            (↑Y.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) :
          (a : (↑Y.toModuleCat : Type u_1)) → (↑Y.toModuleCat : Type u_1))
        x :
      (↑Y.toModuleCat : Type u_1))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
            (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
            (fun (X Y : TopModuleCat.{u_1, u} R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                  (↑Y.toModuleCat : Type u_1)))
            _ _ _ (𝟙 Y : Y ⟶ Y) :
          (a : (↑Y.toModuleCat : Type u_1)) → (↑Y.toModuleCat : Type u_1))
        x :
      (↑Y.toModuleCat : Type u_1))

Tactic:
exact e.apply_symm_apply _

Premises used: ContinuousLinearEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
⊢ Eq.{u_1 + 1} (α := (↑M₁.toModuleCat : Type u_1) →L[R] (↑M₂.toModuleCat : Type u_1)) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
m : (↑M₁.toModuleCat : Type u_1)
⊢ Eq (α := (↑M₂.toModuleCat : Type u_1))
    ((Hom.hom 0 : (a : (↑M₁.toModuleCat : Type u_1)) → (↑M₂.toModuleCat : Type u_1)) m : (↑M₂.toModuleCat : Type u_1))
    (0 : (↑M₂.toModuleCat : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
φ₁ φ₂ : M₁ ⟶ M₂
⊢ Hom.hom (φ₁ + φ₂) = Hom.hom φ₁ + Hom.hom φ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
φ : M₁ ⟶ M₂
⊢ Hom.hom (-φ) = -Hom.hom φ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
φ₁ φ₂ : M₁ ⟶ M₂
⊢ Hom.hom (φ₁ - φ₂) = Hom.hom φ₁ - Hom.hom φ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
n : ℕ
φ : M₁ ⟶ M₂
⊢ Hom.hom (n • φ) = n • Hom.hom φ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M₁ M₂ : TopModuleCat.{u_1, u} R
n : ℤ
φ : M₁ ⟶ M₂
⊢ Hom.hom (n • φ) = n • Hom.hom φ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
S : Type u_1
inst : CommRing S
inst_1 : TopologicalSpace S
M₁ M₂ : TopModuleCat.{u_2, u_1} S
s : S
φ : M₁ ⟶ M₂
⊢ Hom.hom (s • φ) = s • Hom.hom φ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : TopModuleCat.{u_1, u} R
⊢ IsTopologicalAddGroup.{u_1} (↑M.toModuleCat : Type u_1)

Tactic:
M.3

Premises used: TopModuleCat.isTopologicalAddGroup
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
f : X ⟶ Y
hf :
  IsIso (X :=
    Functor.obj
      (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
        (CD := TopCat.carrier))
      X)
    (CategoryTheory.Functor.map
      (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
        (CD := TopCat.carrier))
      f)
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1) :=
  let __spread.0 := Hom.hom f;
  let __spread.1 :
    (↑(Functor.obj
            (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
              (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC :=
              fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
              C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
            X) :
        Type u_1) ≃ₜ
      (↑(Functor.obj
            (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
              (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC :=
              fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
              C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
            Y) :
        Type u_1) :=
    TopCat.homeoOfIso
      (asIso
        (CategoryTheory.Functor.map
          (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
            (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
            (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
            (CD := TopCat.carrier))
          f));
  { toLinearMap := (↑__spread.0 : (↑X.toModuleCat : Type u_1) →ₗ[R] (↑Y.toModuleCat : Type u_1)),
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
change : IsIso (ofIso e).hom
⊢ IsIso f

Tactic:
change IsIso (ofIso e).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.Iso.hom, TopModuleCat.ofIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
f : X ⟶ Y
hf :
  IsIso (X :=
    Functor.obj
      (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
        (CD := TopCat.carrier))
      X)
    (CategoryTheory.Functor.map
      (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
        (CD := TopCat.carrier))
      f)
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1) :=
  let __spread.0 := Hom.hom f;
  let __spread.1 :
    (↑(Functor.obj
            (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
              (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC :=
              fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
              C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
            X) :
        Type u_1) ≃ₜ
      (↑(Functor.obj
            (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
              (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC :=
              fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
              C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
            Y) :
        Type u_1) :=
    TopCat.homeoOfIso
      (asIso
        (CategoryTheory.Functor.map
          (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
            (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
            (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
            (CD := TopCat.carrier))
          f));
  { toLinearMap := (↑__spread.0 : (↑X.toModuleCat : Type u_1) →ₗ[R] (↑Y.toModuleCat : Type u_1)),
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso (ofIso e).hom

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
f : X ⟶ Y
⊢ TopCat.Hom.hom
      (CategoryTheory.Functor.map
        (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
          (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
          (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
          (CD := TopCat.carrier))
        f) =
    (↑(Hom.hom f) :
      C((↑((forget₂ (TopModuleCat R) TopCat).obj X) : Type u_1),
        (↑((forget₂ (TopModuleCat R) TopCat).obj Y) : Type u_1)))

Tactic:
rfl

Premises used: toContinuousMap, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat.{u_1, u} R
⊢ (↑(Functor.obj
          (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
            (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
            (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
            (CD := TopCat.carrier))
          X) :
      Type u_1) =
    (↑X.toModuleCat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- 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.207351, max u (?u.207351 + 1)} (X_1 i).toModuleCat M
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cocone
    (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
h :
  ∀ (x : (↑(F.obj X).toModuleCat : Type u_3)),
    Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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)) (F.map f ≫ toCoinduced c.ι.app Y) :
            (a : (↑(F.obj X).toModuleCat : Type u_3)) →
              (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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)) (Y :=
              Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y)
              (toCoinduced c.ι.app X ≫
                CategoryTheory.Functor.map (Functor.obj (Functor.const J) (coinduced c.ι.app)) f) :
            (a : (↑(F.obj X).toModuleCat : Type u_3)) →
              (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y).toModuleCat : Type u_3))
⊢ F.map f ≫ toCoinduced c.ι.app Y =
    toCoinduced c.ι.app X ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (coinduced c.ι.app)) f

Tactic:
ext 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_1 : I → TopModuleCat R
f_1 : (i : I) → Quiver.Hom.{?u.207351, max u (?u.207351 + 1)} (X_1 i).toModuleCat M
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cocone
    (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 : (↑(F.obj X).toModuleCat : Type u_3)
⊢ Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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)) (F.map f ≫ toCoinduced c.ι.app Y) :
          (a : (↑(F.obj X).toModuleCat : Type u_3)) →
            (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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)) (Y := Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y)
            (toCoinduced c.ι.app X ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (coinduced c.ι.app)) f) :
          (a : (↑(F.obj X).toModuleCat : Type u_3)) →
            (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y).toModuleCat : Type u_3))

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

Premises used: congrArg, id, CategoryTheory.Limits.Cocone.ι, 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.207351, max u (?u.207351 + 1)} (X_1 i).toModuleCat M
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cocone
    (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 : (↑(F.obj X).toModuleCat : Type u_3)
⊢ Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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)) (F.map f ≫ toCoinduced c.ι.app Y) :
          (a : (↑(F.obj X).toModuleCat : Type u_3)) →
            (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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)) (Y := Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y)
            (toCoinduced c.ι.app X ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (coinduced c.ι.app)) f) :
          (a : (↑(F.obj X).toModuleCat : Type u_3)) →
            (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) 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.264306, max u (?u.264306 + 1)} (X i).toModuleCat M
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
inst_3 :
  HasColimit
    (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))
⊢ HasColimit F

Tactic:
⟨_, isColimit (colimit.isColimit _)⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, TopModuleCat.isColimit
-- 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
h :
  ∀ (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))
⊢ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (induced c.π.app)) f ≫ fromInduced c.π.app Y =
    fromInduced c.π.app X ≫ F.map f

Tactic:
ext x