mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
x✝ : ↥(Submodule.comap (↑↑f) U)
x : M
hx : x ∈ Submodule.comap (↑↑f) U
⊢ (↑f ∘SL (Submodule.comap (↑↑f) U).subtypeL) ⟨x, hx⟩ ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ ↑(f.ofSubmodule' U) = (↑f ∘SL (Submodule.comap (↑↑f) U).subtypeL).codRestrict U ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ (α • e).trans f = α • e.trans f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ e.trans (α • f) = α • e.trans f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
inst✝⁹ : Semiring S
S₁ : Type u_6
M : Type u_7
M₁ : Type u_8
inst✝⁸ : Semiring S₁
σ : S →+* S₁
σ' : S₁ →+* S
inst✝⁷ : RingHomInvPair σ σ'
inst✝⁶ : RingHomInvPair σ' σ
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
inst✝² : TopologicalSpace M₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module S₁ M₁
f : M ≃ₛₗ[σ] M₁
hf : IsHomeomorph ⇑f
⊢ ↑(ofIsHomeomorph f hf) = f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
inst✝⁹ : Semiring S
S₁ : Type u_6
M : Type u_7
M₁ : Type u_8
inst✝⁸ : Semiring S₁
σ : S →+* S₁
σ' : S₁ →+* S
inst✝⁷ : RingHomInvPair σ σ'
inst✝⁶ : RingHomInvPair σ' σ
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
inst✝² : TopologicalSpace M₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module S₁ M₁
f : M ≃ₛₗ[σ] M₁
hf : IsHomeomorph ⇑f
⊢ ⇑(ofIsHomeomorph f hf) = ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ((if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
      if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ∀ (x : left a ⟶ right b),
    x ∈
      {
        val :=
          (if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
            if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0,
        nodup := ⋯ }

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
⊢ Continuous fun a ↦ -a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
b : J.L
⊢ ∀ (x : right a ⟶ left b), x ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a b : J.R
⊢ ∀ (x : right a ⟶ right b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
by

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 : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
⊢ ofHom ↑e ≫ ofHom ↑e.symm = 𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
f g : a ⟶ b
h : (fun f ↦ mk f) f = (fun f ↦ mk f) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
⊢ Fintype (a ⟶ b)

Tactic:
have := Finite.of_injective (fun (f : a ⟶ b) ↦ Arrow.mk f)
        (fun f g h ↦ by
          change (Arrow.mk f).hom = (Arrow.mk g).hom
          congr)

Goal state after:
case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
this : Finite (a ⟶ b)
⊢ Fintype (a ⟶ b)
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
⊢ Finite (Arrow C) ↔ Nonempty (FinCategory C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : FinCategory C
⊢ Finite (Arrow C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, max u v} (Arrow C)
X Y : C
f g : X ⟶ Y
h : (fun f ↦ Arrow.mk f) f = (fun f ↦ Arrow.mk f) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : Arrow (ShrinkHoms.{u} C)
⊢ (ShrinkHoms.equivalence C).functor.mapArrow.obj ((ShrinkHoms.equivalence C).inverse.mapArrow.obj x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : Arrow C
⊢ (ShrinkHoms.equivalence C).inverse.mapArrow.obj ((ShrinkHoms.equivalence C).functor.mapArrow.obj x✝) = x✝

Tactic:
by

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 : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
⊢ ofHom ↑e.symm ≫ ofHom ↑e = 𝟙 Y

Tactic:
by

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 : TopModuleCat R
e : X ≅ Y
x : ↑X.toModuleCat
⊢ (Hom.hom e.inv) ((↑(Hom.hom e.hom)).toFun x) = x

Tactic:
by

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 : TopModuleCat R
e : X ≅ Y
x : ↑Y.toModuleCat
⊢ (↑(Hom.hom e.hom)).toFun ((Hom.hom e.inv) x) = x

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow (Shrink.{w, u} C)
⊢ ((Shrink.equivalence C).functor.mapArrow.obj ((Shrink.equivalence C).inverse.mapArrow.obj x✝)).hom =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
by

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 : TopModuleCat R
f : X ⟶ Y
hf : IsIso ((forget₂ (TopModuleCat R) TopCat).map f)
⊢ IsIso f

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow C
⊢ ((Shrink.equivalence C).inverse.mapArrow.obj ((Shrink.equivalence C).functor.mapArrow.obj x✝)).left = x✝.left

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)

Tactic:
by
  rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow C
⊢ ((Shrink.equivalence C).inverse.mapArrow.obj ((Shrink.equivalence C).functor.mapArrow.obj x✝)).right = x✝.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow C
⊢ ((Shrink.equivalence C).inverse.mapArrow.obj ((Shrink.equivalence C).functor.mapArrow.obj x✝)).hom =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
by

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) → (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))
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ toCoinduced c.ι.app Y = toCoinduced c.ι.app X ≫ ((Functor.const J).obj (coinduced c.ι.app)).map f

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
⊢ ((const J).obj (F.obj i₀)).map φ ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ h.cone.π.app j = s.π.app j

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
m : s.pt ⟶ h.cone.pt
hm : ∀ (j : J), m ≫ h.cone.π.app j = s.π.app j
⊢ m = s.π.app i₀

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (c.π.app i₀)

Tactic:
by

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.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
⊢ h.cone ≅ c

Tactic:
by

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) → (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
⊢ Continuous (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun

Tactic:
by

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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map φ)

Tactic:
by

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) → (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
⊢ (ofCocone c).ι.app i ≫
      ofHom
        { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)),
          cont := ⋯ } =
    s.ι.app i

Tactic:
by

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) → (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
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
⊢ m =
    ofHom
      { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)), cont := ⋯ }

Tactic:
by

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))
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (induced c.π.app)).map f ≫ fromInduced c.π.app Y = fromInduced c.π.app X ≫ F.map f

Tactic:
by

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
⊢ Continuous (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun

Tactic:
by

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'
β : i₀ ⟶ j'
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
by

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
⊢ h.coconeιApp i₀ = 𝟙 (F.obj i₀)

Tactic:
by

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
i : J
⊢ ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ } ≫
      (ofCone c).π.app i =
    s.π.app i

Tactic:
by

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
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
⊢ m =
    ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ }

Tactic:
by

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 ≫ ((const J).obj (F.obj i₀)).map φ

Tactic:
by

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 := ⊤
⊢ Continuous fun p ↦ p.1 + p.2

Tactic:
by

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 := ⊤
this : ContinuousAdd ↑X
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
by

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
s : Cocone F
j : J
⊢ h.cocone.ι.app j ≫ s.ι.app i₀ = s.ι.app j

Tactic:
by

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
s : Cocone F
m : h.cocone.pt ⟶ s.pt
hm : ∀ (j : J), h.cocone.ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app i₀

Tactic:
by

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
c : Cocone F
hc : IsColimit c
⊢ IsIso (c.ι.app i₀)

Tactic:
by

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 := ⊤
⊢ Continuous (ModuleCat.Hom.hom f).toFun

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ Continuous LinearMap.id.toFun

Tactic:
by

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
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
⊢ h.cocone ≅ c

Tactic:
by

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
hF : IsEventuallyConstant F
inst✝ : IsCofiltered J
⊢ HasLimit F

Tactic:
by

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
hF : IsEventuallyConstant F
inst✝ : IsFiltered J
⊢ HasColimit F

Tactic:
by

Goal state after:
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
F : C ⥤ D
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F

Tactic:
by

Goal state after:
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
⊢ PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (coyoneda.obj (op X))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : IsFiltered J
D : J ⥤ C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : (Functor.const J).obj X ⟶ D
inst✝ : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
⊢ ∃ j q, p ≫ q = s.app j ∧ q ≫ c.ι.app j = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ HasCardinalFilteredColimits C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C

Tactic:
by

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
⊢ Continuous (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M : TopCat
⊢ freeMap R (𝟙 M) = 𝟙 (freeObj R M)

Tactic:
by

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✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ freeMap R (f ≫ g) = freeMap R f ≫ freeMap R g

Tactic:
by

Goal state after:
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
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
by

Goal state after: