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 : TopCat
f : X ⟶ Y
τ : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R)
h :
  Membership.mem (γ := Set (TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v))))
    {t : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R) |
      ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R) ∧
        ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R) ∧
          TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ t}
    τ
hτ₁ : ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R)
hτ₂ : ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R)
hτ₃ : TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ τ
hxy :
  (↑(toModuleCat (freeObj R Y)) : Type (max u v)) = Finsupp.{v, u} (↑Y : Type v) R →
    Eq (α := (↑X : Type v) → (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
      (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
        (AddHom.toFun
          (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
        fun (x : (↑X : Type v)) ↦ Finsupp.single x 1)
      ((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun)
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced
      (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
        (AddHom.toFun
          (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
        fun (x : (↑X : Type v)) ↦ Finsupp.single x 1)
      X.str)
    (TopologicalSpace.coinduced ((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) X.str)

Tactic:
congr! 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R)
h :
  Membership.mem (γ := Set (TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v))))
    {t : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R) |
      ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R) ∧
        ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R) ∧
          TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ t}
    τ
hτ₁ : ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R)
hτ₂ : ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R)
hτ₃ : TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ τ
e_2 : (↑(toModuleCat (freeObj R Y)) : Type (max u v)) = Finsupp.{v, u} (↑Y : Type v) R
hxy :
  ∀ (x : (↑X : Type v)),
    Eq (α := (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
      (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
        (AddHom.toFun
          (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
        (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) x)
      (((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) x)
⊢ Eq (α := (↑X : Type v) → (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      fun (x : (↑X : Type v)) ↦ Finsupp.single x 1)
    ((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun)

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R)
h :
  Membership.mem (γ := Set (TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v))))
    {t : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R) |
      ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R) ∧
        ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R) ∧
          TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ t}
    τ
hτ₁ : ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R)
hτ₂ : ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R)
hτ₃ : TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ τ
e_2 : (↑(toModuleCat (freeObj R Y)) : Type (max u v)) = Finsupp.{v, u} (↑Y : Type v) R
x : (↑X : Type v)
⊢ Eq (α := (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) x)
    (((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) x)

Tactic:
simp [coe_freeObj]

Premises used: TopModuleCat.coe_freeObj
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
v : Finsupp.{v, u} (↑X : Type v) R
⊢ Eq (α := (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeObj R Y))
    ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R f) :
          (a : (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeObj R X)) →
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeObj R Y))
        v :
      (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeObj R Y))
    (Finsupp.mapDomain (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)) v : Finsupp.{v, u} (↑Y : Type v) R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : TopCat
h :
  ∀ (x : (↑(toModuleCat (freeObj R M)) : Type (max u v))),
    Eq (α := (↑(toModuleCat (freeObj R M)) : Type (max u v)))
      ((@hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat R) ↦
                (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
              (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
              (fun (X Y : TopModuleCat R) ↦
                (ContinuousLinearMap.funLike :
                  FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                    (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
              _ _ _ (freeMap R (𝟙 M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
            (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
          x :
        (↑(toModuleCat (freeObj R M)) : Type (max u v)))
      ((@hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat R) ↦
                (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
              (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
              (fun (X Y : TopModuleCat R) ↦
                (ContinuousLinearMap.funLike :
                  FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                    (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
              _ _ _ (𝟙 (freeObj R M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
            (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
          x :
        (↑(toModuleCat (freeObj R M)) : Type (max u v)))
⊢ Eq (α := Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) (freeMap R (𝟙 M)) (𝟙 (freeObj R M))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : TopCat
x : (↑(toModuleCat (freeObj R M)) : Type (max u v))
⊢ Eq (α := (↑(toModuleCat (freeObj R M)) : Type (max u v)))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat R) ↦ (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
            (fun (X Y : TopModuleCat R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                  (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
            _ _ _ (freeMap R (𝟙 M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
          (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R M)) : Type (max u v)))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat R) ↦ (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
            (fun (X Y : TopModuleCat R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                  (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
            _ _ _ (𝟙 (freeObj R M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
          (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R M)) : Type (max u v)))

Tactic:
DFunLike.congr_fun (Finsupp.lmapDomain_id _ _) x

Premises used: Finsupp.lmapDomain_id, DFunLike.congr_fun
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : TopCat
x : (↑(toModuleCat (freeObj R M)) : Type (max u v))
⊢ Eq (α := (↑(toModuleCat (freeObj R M)) : Type (max u v)))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat R) ↦ (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
            (fun (X Y : TopModuleCat R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                  (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
            _ _ _ (freeMap R (𝟙 M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
          (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R M)) : Type (max u v)))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat R) ↦ (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
            (fun (X Y : TopModuleCat R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                  (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
            _ _ _ (𝟙 (freeObj R M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
          (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R M)) : Type (max u v)))

Tactic:
exact DFunLike.congr_fun (Finsupp.lmapDomain_id _ _) x

Premises used: Finsupp.lmapDomain_id, DFunLike.congr_fun
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : (↑(toModuleCat (freeObj R X)) : Type (max u v))),
    Eq (α := (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
              (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
              fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R (f ≫ g)) :
            (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
          x :
        (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
              (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
              fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R f ≫ freeMap R g) :
            (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
          x :
        (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
⊢ Eq (α := Quiver.Hom (V := TopModuleCat R) (freeObj R X) (freeObj R Z)) (freeMap R (f ≫ g)) (freeMap R f ≫ freeMap R g)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑(toModuleCat (freeObj R X)) : Type (max u v))
⊢ Eq (α := (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R (f ≫ g)) :
          (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R f ≫ freeMap R g) :
          (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R Z)) : Type (max u v)))

Tactic:
DFunLike.congr_fun (Finsupp.lmapDomain_comp _ _ f.hom g.hom) _

Premises used: DFunLike.congr_fun, Finsupp.lmapDomain_comp, TopCat.Hom.hom, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑(toModuleCat (freeObj R X)) : Type (max u v))
⊢ Eq (α := (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R (f ≫ g)) :
          (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) (freeMap R f ≫ freeMap R g) :
          (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R Z)) : Type (max u v)))

Tactic:
exact DFunLike.congr_fun (Finsupp.lmapDomain_comp _ _ f.hom g.hom) _

Premises used: DFunLike.congr_fun, Finsupp.lmapDomain_comp, TopCat.Hom.hom, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
rw :
  LE.le (α :=
    TopologicalSpace
      (↑(toModuleCat
            (Functor.obj
              (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                  (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                  fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                  C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier) ⋙
                free R)
              X)) :
        Type (max u v)))
    (topologicalSpace
      (Functor.obj
        (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier) ⋙
          free R)
        X))
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
          ((Finsupp.lift (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) R
                (↑X.toModuleCat : Type (max u v)) :
              (a : (↑X.toModuleCat : Type (max u v)) → (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v))) →
                ((↑X.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                  (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v)))
            id)))
      (Functor.obj (𝟭 (TopModuleCat R)) X).topologicalSpace)
⊢ Continuous (X :=
    (↑(toModuleCat
          (Functor.obj
            (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier) ⋙
              free R)
            X)) :
      Type (max u v)))
    (Y := (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)))
    (AddHom.toFun
      (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
        ((Finsupp.lift (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) R
              (↑X.toModuleCat : Type (max u v)) :
            (a : (↑X.toModuleCat : Type (max u v)) → (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v))) →
              ((↑X.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v)))
          id)))

Tactic:
rw [continuous_iff_le_induced]

Premises used: continuous_iff_le_induced
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
⊢ LE.le (α :=
    TopologicalSpace
      (↑(toModuleCat
            (Functor.obj
              (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                  (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                  fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                  C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier) ⋙
                free R)
              X)) :
        Type (max u v)))
    (topologicalSpace
      (Functor.obj
        (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier) ⋙
          free R)
        X))
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
          ((Finsupp.lift (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) R
                (↑X.toModuleCat : Type (max u v)) :
              (a : (↑X.toModuleCat : Type (max u v)) → (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v))) →
                ((↑X.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                  (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v)))
            id)))
      (Functor.obj (𝟭 (TopModuleCat R)) X).topologicalSpace)

Tactic:
sInf_le ⟨continuousSMul_induced (Finsupp.lift _ R X id),
        continuousAdd_induced (Finsupp.lift _ R X id), ?_⟩

Premises used: Set.Mem, setOf, id, TopModuleCat.toModuleCat, continuousSMul_induced, continuousAdd_induced, sInf_le, And.intro, ModuleCat.carrier, OrderDual, DFunLike.coe, Finsupp.lift
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
⊢ LE.le (α :=
    TopologicalSpace
      (↑(Functor.obj
            (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
              (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
              fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
              C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
            X) :
        Type (max v u)))
    (Functor.obj
        (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
          (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC := fun (X : TopModuleCat R) ↦
          (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
          C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
        X).str
    (TopologicalSpace.induced id
      (Functor.obj
          (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
          X).str)

Tactic:
induced_id.symm.le

Premises used: induced_id, Eq.le, Eq.symm