mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app i))

Tactic:
]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app i))
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ c.π.app i ≫ F.map β = c.π.app i ≫ F.map β

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun
      s.1.topologicalSpace ≤
    instTopologicalSpaceCarrier R (ofCone c).pt

Tactic:
]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun
      s.1.topologicalSpace ≤
    instTopologicalSpaceCarrier R (ofCone c).pt
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous
    (⇑(hom (c.π.app i)) ∘ (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun)

Tactic:
]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous
    (⇑(hom (c.π.app i)) ∘ (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app i))

Tactic:
]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app i))
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ F.map γ = F.map (rightToMax i₀ j) ≫ F.map γ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
⊢ 𝟙 (F.obj i₀) = 𝟙 (F.obj i₀)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j

Tactic:
]

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this : TopologicalSpace ↑X := ⊤
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this : TopologicalSpace ↑X := ⊤
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this✝ : TopologicalSpace ↑X := ⊤
this : ContinuousAdd ↑X
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this✝

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this✝ : TopologicalSpace ↑X := ⊤
this : ContinuousAdd ↑X
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this✝
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
s : Cocone F
j : J
⊢ F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j) = F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (of R ↑X).topologicalSpace ≤ (of R ↑Y).topologicalSpace

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (of R ↑X).topologicalSpace ≤ (of R ↑Y).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ TopologicalSpace.coinduced LinearMap.id.toFun ((𝟭 (TopModuleCat R)).obj X).topologicalSpace ≤
    ((forget₂ (TopModuleCat R) (ModuleCat R) ⋙ indiscrete R).obj X).topologicalSpace

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ TopologicalSpace.coinduced LinearMap.id.toFun ((𝟭 (TopModuleCat R)).obj X).topologicalSpace ≤
    ((forget₂ (TopModuleCat R) (ModuleCat R) ⋙ indiscrete R).obj X).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun (freeObj R X).topologicalSpace ≤
    (freeObj R Y).topologicalSpace

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun (freeObj R X).topologicalSpace ≤
    (freeObj R Y).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ (freeObj R X).topologicalSpace ≤ TopologicalSpace.induced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun τ

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ (freeObj R X).topologicalSpace ≤ TopologicalSpace.induced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun τ
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    τ

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    τ
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ F.map β ≫ c.ι.app i = F.map β ≫ c.ι.app i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) (TopologicalSpace.coinduced (TopCat.Hom.hom f).toFun X.str)

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) (TopologicalSpace.coinduced (TopCat.Hom.hom f).toFun X.str)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced ((Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun ∘ fun x ↦ Finsupp.single x 1) X.str ≤
    TopologicalSpace.coinduced ((fun x ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) X.str

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced ((Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun ∘ fun x ↦ Finsupp.single x 1) X.str ≤
    TopologicalSpace.coinduced ((fun x ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) X.str
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
X : C
inst✝ : IsFinitelyPresentable X
⊢ IsFinitelyPresentable X

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
X : C
inst✝ : IsFinitelyPresentable X
⊢ IsFinitelyPresentable X
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).topologicalSpace ≤
    TopologicalSpace.induced ((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).topologicalSpace ≤
    TopologicalSpace.induced ((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat).obj X).str ≤
    TopologicalSpace.induced
      (((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun ∘ fun x ↦
        Finsupp.single x 1)
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat).obj X).str ≤
    TopologicalSpace.induced
      (((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun ∘ fun x ↦
        Finsupp.single x 1)
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : IsCardinalPresentable X κ
⊢ IsCardinalPresentable X κ'

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : IsCardinalPresentable X κ
⊢ IsCardinalPresentable X κ'
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
e✝ : X ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : IsCardinalPresentable X✝ κ
⊢ IsCardinalPresentable Y✝ κ

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
e✝ : X ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : IsCardinalPresentable X✝ κ
⊢ IsCardinalPresentable Y✝ κ
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∀ {J_1 : Type w} [inst : SmallCategory J_1] [FinCategory J_1] (F : J_1 ⥤ J), Nonempty (Cocone F)

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∀ {J_1 : Type w} [inst : SmallCategory J_1] [FinCategory J_1] (F : J_1 ⥤ J), Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ IsFiltered J

Tactic:
by
  rw [IsFiltered.iff_cocone_nonempty.{w}]
  intro A _ _ F
  have hA : HasCardinalLT (Arrow A) κ := by
    refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
    simp only [hasCardinalLT_aleph0_iff]
    infer_instance
  exact ⟨cocone F hA⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
⊢ Nonempty (Cocone F)

Tactic:
]

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
⊢ Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h : Function.Surjective fun i ↦ ⟨f i, ⋯⟩
hs : ∀ (j : κ.ord.ToType), ∃ k, j < f k
⊢ Order.cof κ.ord.ToType ≤ Cardinal.mk ι

Tactic:
]

Goal state after:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h : Function.Surjective fun i ↦ ⟨f i, ⋯⟩
hs : ∀ (j : κ.ord.ToType), ∃ k, j < f k
⊢ Order.cof κ.ord.ToType ≤ Cardinal.mk ι
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
⊢ f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
]

Goal state after:
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ x ⊗ₜ[R] ∑ a, Pi.single a (m a) = x ⊗ₜ[R] m

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ x ⊗ₜ[R] ∑ a, Pi.single a (m a) = x ⊗ₜ[R] m
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ x ⊗ₜ[R] Pi.single i m j = x ⊗ₜ[R] Pi.single i m j

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j ↦ x ⊗ₜ[R] Pi.single i m j
⊢ ((piRightInv R S N M) fun j ↦ x ⊗ₜ[R] Pi.single i m j) = x ⊗ₜ[R] Pi.single i m

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j ↦ x ⊗ₜ[R] Pi.single i m j
⊢ ((piRightInv R S N M) fun j ↦ x ⊗ₜ[R] Pi.single i m j) = x ⊗ₜ[R] Pi.single i m