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 : I → TopModuleCat R
f : (i : I) → Quiver.Hom.{?u.342320, max u (?u.342320 + 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))
inst_4 :
  PreservesLimit
    (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))
    (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
      ModuleCat.carrier))
⊢ PreservesLimit 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)) TopCat (FD := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CD :=
      TopCat.carrier))

Tactic:
preservesLimit_of_preserves_limit_cone (isLimit (limit.isLimit _))
    (TopCat.isLimitConeOfForget (F := F ⋙ forget₂ _ TopCat)
      ((forget _).mapCone (getLimitCone (F ⋙ forget₂ _ (ModuleCat.{v} R))).1 :)
      (isLimitOfPreserves (forget (ModuleCat R)) (limit.isLimit _)))

Premises used: ModuleCat, CategoryTheory.Functor.comp, CategoryTheory.Limits.getLimitCone, TopModuleCat.isLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.forget₂, CategoryTheory.forget, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Functor.mapCone, TopCat.isLimitConeOfForget, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.LimitCone.cone
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
⊢ Functor.IsRightAdjoint
    (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)) (ModuleCat.{u_1, u} R) (FD := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
      (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))

Tactic:
⟨_, ⟨withModuleTopologyAdj R⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, TopModuleCat.withModuleTopologyAdj
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
⊢ Functor.IsLeftAdjoint (C := ModuleCat.{u_1, u} R) (D := TopModuleCat.{u_1, u} R) (withModuleTopology R)

Tactic:
⟨_, ⟨withModuleTopologyAdj R⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, TopModuleCat.withModuleTopologyAdj
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : ModuleCat.{v, u} R
this : TopologicalSpace (↑X : Type v) := ⊤
rw : TopologicalSpace.coinduced (fun (p : (↑X : Type v) × (↑X : Type v)) ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this
⊢ Continuous (Y := (↑X : Type v)) fun (p : (↑X : Type v) × (↑X : Type v)) ↦ p.1 + p.2

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
X : ModuleCat.{v, u} R
this : TopologicalSpace (↑X : Type v) := ⊤
⊢ TopologicalSpace.coinduced (fun (p : (↑X : Type v) × (↑X : Type v)) ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : ModuleCat.{v, u} R
this : TopologicalSpace (↑X : Type v) := ⊤
⊢ TopologicalSpace.coinduced (fun (p : (↑X : Type v) × (↑X : Type v)) ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : ModuleCat.{v, u} R
this_1 : TopologicalSpace (↑X : Type v) := ⊤
this : ContinuousAdd.{v} (↑X : Type v)
rw : TopologicalSpace.coinduced (fun (p : Prod.{u, v} R (↑X : Type v)) ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this_1
⊢ Continuous (Y := (↑X : Type v)) fun (p : Prod.{u, v} R (↑X : Type v)) ↦ p.1 • p.2

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
X : ModuleCat.{v, u} R
this_1 : TopologicalSpace (↑X : Type v) := ⊤
this : ContinuousAdd.{v} (↑X : Type v)
⊢ TopologicalSpace.coinduced (fun (p : Prod.{u, v} R (↑X : Type v)) ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this_1

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : ModuleCat.{v, u} R
this_1 : TopologicalSpace (↑X : Type v) := ⊤
this : ContinuousAdd.{v} (↑X : Type v)
⊢ TopologicalSpace.coinduced (fun (p : Prod.{u, v} R (↑X : Type v)) ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this_1

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
this_1 : TopologicalSpace (↑X : Type v) := ⊤
this : TopologicalSpace (↑Y : Type v) := ⊤
rw :
  TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (topologicalSpace (of R (↑X : Type v))) ≤
    topologicalSpace (of R (↑Y : Type v))
⊢ Continuous (ModuleCat.Hom.hom f).toFun

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
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
this_1 : TopologicalSpace (↑X : Type v) := ⊤
this : TopologicalSpace (↑Y : Type v) := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (topologicalSpace (of R (↑X : Type v))) ≤
    topologicalSpace (of R (↑Y : Type v))

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
this_1 : TopologicalSpace (↑X : Type v) := ⊤
this : TopologicalSpace (↑Y : Type v) := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (topologicalSpace (of R (↑X : Type v))) ≤
    topologicalSpace (of R (↑Y : Type v))

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat.{v, u} R
rw :
  TopologicalSpace.coinduced (AddHom.toFun (LinearMap.toAddHom.{u, u, v, v} (R := R) LinearMap.id))
      (Functor.obj (𝟭 (TopModuleCat.{v, u} R)) X).topologicalSpace ≤
    topologicalSpace
      (Functor.obj
        (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) ⋙
          indiscrete R)
        X)
⊢ Continuous.{v, v} (X := (↑(Functor.obj (𝟭 (TopModuleCat.{v, u} R)) X).toModuleCat : Type v))
    (AddHom.toFun (LinearMap.toAddHom.{u, u, v, v} (R := R) LinearMap.id))

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
X : TopModuleCat.{v, u} R
⊢ TopologicalSpace.coinduced (AddHom.toFun (LinearMap.toAddHom.{u, u, v, v} (R := R) LinearMap.id))
      (Functor.obj (𝟭 (TopModuleCat.{v, u} R)) X).topologicalSpace ≤
    topologicalSpace
      (Functor.obj
        (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) ⋙
          indiscrete R)
        X)

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat.{v, u} R
⊢ TopologicalSpace.coinduced (AddHom.toFun (LinearMap.toAddHom.{u, u, v, v} (R := R) LinearMap.id))
      (Functor.obj (𝟭 (TopModuleCat.{v, u} R)) X).topologicalSpace ≤
    topologicalSpace
      (Functor.obj
        (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) ⋙
          indiscrete R)
        X)

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
⊢ Functor.IsLeftAdjoint
    (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))

Tactic:
⟨_, ⟨indiscreteAdj R⟩⟩

Premises used: Nonempty.intro, TopModuleCat.indiscreteAdj, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
⊢ Functor.IsRightAdjoint (C := TopModuleCat.{v, u} R) (indiscrete R)

Tactic:
⟨_, ⟨indiscreteAdj R⟩⟩

Premises used: Nonempty.intro, TopModuleCat.indiscreteAdj, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopCat
⊢ (↑(toModuleCat (freeObj R X)) : Type (max u v)) = Finsupp.{v, u} (↑X : Type v) R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
rw :
  LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced (X := (↑(toModuleCat (freeObj R X)) : Type (max u v)))
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      (topologicalSpace (freeObj R X)))
    (topologicalSpace (freeObj R Y))
⊢ Continuous (X := (↑(toModuleCat (freeObj R X)) : Type (max u v))) (Y :=
    (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (AddHom.toFun
      (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))

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
X Y : TopCat
f : X ⟶ Y
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced (X := (↑(toModuleCat (freeObj R X)) : Type (max u v)))
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      (topologicalSpace (freeObj R X)))
    (topologicalSpace (freeObj R Y))

Tactic:
le_sInf fun (τ : TopologicalSpace (_ →₀ R)) ⟨hτ₁, hτ₂, hτ₃⟩ ↦ ?_

Premises used: Set.Mem, TopModuleCat.freeObj, setOf, Finsupp.lmapDomain, LinearMap.toAddHom, LE.le, TopModuleCat.topologicalSpace, TopologicalSpace.coinduced, _private.0.TopModuleCat.freeMap.match_1, TopCat.Hom.hom, le_sInf, OrderDual, DFunLike.coe, AddHom.toFun
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
refine :
  ∀ (τ : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R)),
    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 ≤ τ),
        TopologicalSpace.coinduced (X := (↑(toModuleCat (freeObj R X)) : Type (max u v)))
            (AddHom.toFun
              (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
            (topologicalSpace (freeObj R X)) ≤
          τ
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced (X := (↑(toModuleCat (freeObj R X)) : Type (max u v)))
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      (topologicalSpace (freeObj R X)))
    (topologicalSpace (freeObj R Y))

Tactic:
refine le_sInf fun (τ : TopologicalSpace (_ →₀ R)) ⟨hτ₁, hτ₂, hτ₃⟩ ↦ ?_
-- 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 ≤ τ
rw :
  LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R X)) : Type (max u v))) (topologicalSpace (freeObj R X))
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      τ)
⊢ TopologicalSpace.coinduced (X := (↑(toModuleCat (freeObj R X)) : Type (max u v)))
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      (topologicalSpace (freeObj R X)) ≤
    τ

Tactic:
rw [coinduced_le_iff_le_induced]

Premises used: coinduced_le_iff_le_induced
-- 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 ≤ τ
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R X)) : Type (max u v))) (topologicalSpace (freeObj R X))
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      τ)

Tactic:
sInf_le ⟨continuousSMul_induced (Finsupp.lmapDomain _ _ f.hom),
      continuousAdd_induced (Finsupp.lmapDomain _ _ f.hom), ?_⟩

Premises used: Set.Mem, setOf, Finsupp.lmapDomain, continuousSMul_induced, continuousAdd_induced, TopCat.Hom.hom, sInf_le, And.intro, OrderDual, DFunLike.coe
-- 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 ≤ τ
refine :
  LE.le (α := TopologicalSpace (Finsupp.{v, u} (↑X : Type v) R))
    (TopologicalSpace.coinduced (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) X.str)
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      τ)
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R X)) : Type (max u v))) (topologicalSpace (freeObj R X))
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      τ)

Tactic:
refine sInf_le ⟨continuousSMul_induced (Finsupp.lmapDomain _ _ f.hom),
      continuousAdd_induced (Finsupp.lmapDomain _ _ f.hom), ?_⟩
-- 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 ≤ τ
rw :
  TopologicalSpace.coinduced (X := 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)))))
      (TopologicalSpace.coinduced (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) X.str) ≤
    τ
⊢ LE.le (α := TopologicalSpace (Finsupp.{v, u} (↑X : Type v) R))
    (TopologicalSpace.coinduced (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) X.str)
    (TopologicalSpace.induced
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      τ)

Tactic:
rw [← coinduced_le_iff_le_induced]

Premises used: coinduced_le_iff_le_induced
-- 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 ≤ τ
grw :
  LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced (X := 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)))))
      (TopologicalSpace.coinduced (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) X.str))
    (TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1)
      (TopologicalSpace.coinduced (TopCat.Hom.hom f).toFun X.str))
⊢ TopologicalSpace.coinduced (X := 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)))))
      (TopologicalSpace.coinduced (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) X.str) ≤
    τ

Tactic:
grw [← hτ₃, ← coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2)]

Premises used: ContinuousMap.continuous_toFun, TopCat.Hom.hom, Iff.mp, continuous_iff_coinduced_le, coinduced_mono
-- 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 ≤ τ
rw :
  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)
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced (X := 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)))))
      (TopologicalSpace.coinduced (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) X.str))
    (TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1)
      (TopologicalSpace.coinduced (TopCat.Hom.hom f).toFun X.str))

Tactic:
rw [coinduced_compose, coinduced_compose]

Premises used: coinduced_compose