mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
⊢ ∀ {X Y : C} (x : X ≅ Y), P.colimitsOfShape J X → P.colimitsOfShape J Y

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ IsPullback (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
Q : ObjectProperty C
hPQ : P ≤ Q
⊢ P.colimitsOfShape J ≤ Q.colimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.diagonal.RespectsIso

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.isoClosure.colimitsOfShape J = P.colimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P
    ((pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫
      pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P.diagonal (x✝¹ ≫ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
h : P.diagonal g
⊢ P (Over.Hom.left (Over.homMk (pullback.diagonal g) ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.RespectsIso
⊢ ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P.diagonal g → P.diagonal (pullback.fst f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝⁶ : Category.{v', u'} J
J' : Type u''
inst✝⁵ : Category.{v'', u''} J'
inst✝⁴ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝³ : LocallySmall.{w, v_1, u_1} C
inst✝² : Small.{w, u'} J
inst✝¹ : LocallySmall.{w, v', u'} J
F : J ⥤ C
inst✝ : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ HasColimit (P.lift F hF ⋙ P.ι)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : P.HasOfPostcompProperty Q
X Y : C
f : X ⟶ Y
hf : Q f
⊢ P (pullback.diagonal f ≫ pullback.fst f f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op = pullback.diagonal f.op ≫ (pullbackIsoOpPushout f.op f.op).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ 𝟙 Y ≫ g ≫ f = g ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝⁵ : Category.{v', u'} J
J' : Type u''
inst✝⁴ : Category.{v'', u''} J'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.Small.{w, v_1, u_1} (P.strictColimitsOfShape J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
⊢ g = gr ≫ pullback.snd (g ≫ f) f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z X Y : C
f : X ⟶ Y
inst✝¹ : HasPushout f f
inst✝ : Epi f
⊢ IsIso (codiagonal f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ inl f f ≫ codiagonal f = inr f f ≫ codiagonal f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictColimitsOfShape J ≤ P
⊢ P.colimitsOfShape J ≤ P

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : Nonempty J
⊢ ⊥.colimitsOfShape J ≤ ⊥

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ i ≫ f = 𝟙 S ≫ i ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
x✝¹ : C
x✝ : ⊤.colimitsOfShape J x✝¹
⊢ ⊤ x✝¹

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ i ≫ g = 𝟙 S ≫ i ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (i ≫ f) ≫ 𝟙 X = i ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
e : J ≌ J'
⊢ P.IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
⊢ P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (i ≫ g) ≫ 𝟙 Y = i ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
e : J ≌ J'
inst✝ : P.IsClosedUnderColimitsOfShape J
⊢ P.IsClosedUnderColimitsOfShape J'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
⊢ (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (pullback.fst f.op g.op ≫ f.op) ≫ (Iso.refl (Opposite.op T)).hom =
    (pullbackIsoOpPushout f.op g.op).hom ≫ (pushout.inl f g).op ≫ f.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape J = (P.op.limitsOfShape Jᵒᵖ).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯ ≫
      (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom =
    (pullbackIsoOpPushout f.op g.op).hom ≫
      (pullbackIsoOpPushout f.op g.op).inv ≫
        pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯ ≫
          (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ pullback.diagonal i.op ≫ (pullbackIsoOpPushout i.op i.op).hom =
    (Iso.refl (Opposite.op T)).hom ≫ pullback.diagonal i.op ≫ (pullbackIsoOpPushout i.op i.op).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ IsPullback f' ?m.112 ?m.113 f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯ ≫
      (pullbackIsoOpPushout i.op i.op).hom =
    (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom ≫
      (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).inv ≫
        pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯ ≫
          (pullbackIsoOpPushout i.op i.op).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPushout (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯) (pushout.codiagonal i)
    (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯) (f ≫ pushout.inl f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.op.limitsOfShape J = (P.colimitsOfShape Jᵒᵖ).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.op.colimitsOfShape J = (P.limitsOfShape Jᵒᵖ).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.IsClosedUnderColimitsOfShape J ↔ P.op.IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ IsPullback f' ?m.217 ?m.218 f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.universally.RespectsIso

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.IsClosedUnderLimitsOfShape J ↔ P.op.IsClosedUnderColimitsOfShape Jᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
⊢ P f'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.IsClosedUnderColimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderLimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.universally ≤ P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.IsClosedUnderLimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderColimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape J
⊢ P.op.IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderLimitsOfShape J
⊢ P.op.IsClosedUnderColimitsOfShape Jᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ P.op.IsClosedUnderLimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
⊢ (P ⊓ Q).universally = P.universally ⊓ Q.universally

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderLimitsOfShape Jᵒᵖ
⊢ P.op.IsClosedUnderColimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderColimitsOfShape J
⊢ Q.unop.IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderLimitsOfShape J
⊢ Q.unop.IsClosedUnderColimitsOfShape Jᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ Q.unop.IsClosedUnderLimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
⊢ P.universally g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderLimitsOfShape Jᵒᵖ
⊢ Q.unop.IsClosedUnderColimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
⊢ (h.r ≫ h.i) ≫ h.r = 𝟙 Y ≫ h.r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChangeAgainst ⊤
x✝⁷ x✝⁶ x✝⁵ x✝⁴ : C
x✝³ : x✝⁷ ⟶ x✝⁴
x✝² : x✝⁶ ⟶ x✝⁴
x✝¹ : x✝⁵ ⟶ x✝⁶
x✝ : x✝⁵ ⟶ x✝⁷
h' : IsPullback x✝¹ x✝ x✝² x✝³
h'' : P x✝²
⊢ ⊤ x✝³

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
⊢ c.π ≫ h.i ≫ s.π = s.π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.HasPullbacksAgainst ⊤
X✝ Y✝ S✝ : C
f✝ : X✝ ⟶ S✝
x✝ : Y✝ ⟶ S✝
h' : P f✝
⊢ ⊤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChangeAgainst ⊤
x✝⁷ x✝⁶ x✝⁵ x✝⁴ : C
x✝³ : x✝⁷ ⟶ x✝⁶
x✝² : x✝⁷ ⟶ x✝⁵
x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁶ ⟶ x✝⁴
h' : IsPushout x✝² x✝³ x✝¹ x✝
h'' : P x✝³
⊢ ⊤ x✝²

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.HasPushoutsAgainst ⊤
X✝ Y✝ S✝ : C
f✝ : S✝ ⟶ X✝
x✝ : S✝ ⟶ Y✝
h' : P f✝
⊢ ⊤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
m : c.pt ⟶ s.pt
hm : c.π ≫ m = s.π
⊢ m = h.i ≫ s.π

Tactic:
by

Goal state after: