awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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
⊢ 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))
have 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
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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
have 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
Tactic: refine le_iInf fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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
⊢ 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
have rw : Continuous (X := (↑(toModuleCat s.1) : Type u_3)) (Y := (↑(F.obj i).toModuleCat : Type u_3))
  (Function.comp (β := (↑(ofCone c).pt.toModuleCat : Type u_3))
      (⇑(hom (FC := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CC :=
            ModuleCat.carrier) (c.π.app i)) :
        (a : (↑c.1 : Type u_3)) → (↑(F.obj i).toModuleCat : Type u_3))
      (AddHom.toFun
        (LinearMap.toAddHom.{u, u, u_3, u_3} (R := R) (S := R) (σ := RingHom.id R)
          (ModuleCat.Hom.hom
            (hc.lift
              (Functor.mapCone
                (forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
                  (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC :=
                  fun (X : TopModuleCat.{u_3, u} R) ↦ (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD :=
                  fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD :=
                  ModuleCat.carrier))
                s))))) :
    (↑s.1.1 : Type u_3) → (↑(F.obj i).toModuleCat : Type u_3))
Tactic: rw [coinduced_le_iff_le_induced, induced_compose, ← continuous_iff_le_induced]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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
⊢ 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))
have 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))
Tactic: change Continuous (X := s.pt) (Y := F.obj i)
      (hc.lift ((forget₂ _ (ModuleCat R)).mapCone s) ≫ c.π.app i).hom
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : ModuleCat.{v, u} R
this : TopologicalSpace (↑X : Type v) := ⊤
⊢ Continuous (Y := (↑X : Type v)) fun (p : (↑X : Type v) × (↑X : Type v)) ↦ p.1 + p.2
have rw : TopologicalSpace.coinduced (fun (p : (↑X : Type v) × (↑X : Type v)) ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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)
⊢ Continuous (Y := (↑X : Type v)) fun (p : Prod.{u, v} R (↑X : Type v)) ↦ p.1 • p.2
have rw : TopologicalSpace.coinduced (fun (p : Prod.{u, v} R (↑X : Type v)) ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this_1
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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) := ⊤
⊢ Continuous (ModuleCat.Hom.hom f).toFun
have rw : TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (topologicalSpace (of R (↑X : Type v))) ≤
  topologicalSpace (of R (↑Y : Type v))
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat.{v, u} R
⊢ 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))
have 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)
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ 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)))))
have 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))
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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))
have 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)) ≤
        τ
Tactic: refine le_sInf fun (τ : TopologicalSpace (_ →₀ R)) ⟨hτ₁, hτ₂, hτ₃⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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 ≤ τ
⊢ 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)) ≤
    τ
have 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)))))
    τ)
Tactic: rw [coinduced_le_iff_le_induced]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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)))))
      τ)
have 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)))))
    τ)
Tactic: refine sInf_le ⟨continuousSMul_induced (Finsupp.lmapDomain _ _ f.hom),
      continuousAdd_induced (Finsupp.lmapDomain _ _ f.hom), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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 (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)))))
      τ)
have 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) ≤
  τ
Tactic: rw [← coinduced_le_iff_le_induced]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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 ≤ τ
⊢ 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) ≤
    τ
have 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))
Tactic: grw [← hτ₃, ← coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2)]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
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 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))
have 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)
Tactic: rw [coinduced_compose, coinduced_compose]