mathlib-initiative/mathlib-tactics huggingface dataset:
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 : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      snd (fst f g) (fst f g) ≫ snd f g =
    fst (snd g g ≫ g) f ≫ snd g g

Tactic:
simp

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

Goal state before:
pp: case h₀.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ fst (fst f g) (fst f g)) ≫ fst f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst (fst f g) (fst f g)) ≫
      fst f g

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ fst (fst f g) (fst f g)) ≫ snd f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst (fst f g) (fst f g)) ≫
      snd f g

Tactic:
simp

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

Goal state before:
pp: case h₁.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ snd (fst f g) (fst f g)) ≫ fst f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd (fst f g) (fst f g)) ≫
      fst f g

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal (fst f g) ≫ snd (fst f g) (fst f g)) ≫ snd f g =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd (fst f g) (fst f g)) ≫
      snd f g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.IsStableUnderLimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ ∀ (j : J), h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f } ≫ c₂✝.π.app j = c₁✝.π.app j ≫ f.app j

Tactic:
simp

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✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ 𝟙 Y ≫ g ≫ f = g ≫ f

Tactic:
simp

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✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ (g ≫ f) ≫ 𝟙 S = g ≫ f

Tactic:
simp

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✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ f ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
simp

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✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
⊢ f = 𝟙 X ≫ f

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
⊢ W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
⊢ ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ
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✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ (g ≫ f) ≫ 𝟙 S = g ≫ f

Tactic:
simp

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✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ f ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
simp

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✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ (𝟙 X ≫ f) ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
simp

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✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ diagonal f ≫ 𝟙 (diagonalObj f) = 𝟙 X ≫ diagonal f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
X : C
pres : ColimitPresentation J X
i j : J
f : i ⟶ j
⊢ pres.diag.map f ≫ pres.ι.app j = pres.ι.app i

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : Category.{t, w} J
X : C
P : ColimitPresentation J X
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
⊢ ∀ (j : J),
    (F.mapCocone { pt := X, ι := P.ι }).ι.app j ≫ (Iso.refl (F.mapCocone { pt := X, ι := P.ι }).pt).hom =
      { pt := F.obj X, ι := Functor.whiskerRight P.ι F ≫ (Functor.constComp J X F).hom }.ι.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : Type w
inst✝³ : Category.{t, w} J✝
X✝ : C
J : Type w
inst✝² : Category.{t, w} J
X : C
P : LimitPresentation J X
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
⊢ ∀ (j : J),
    (F.mapCone { pt := X, π := P.π }).π.app j =
      (Iso.refl (F.mapCone { pt := X, π := P.π }).pt).hom ≫
        { pt := F.obj X, π := (Functor.constComp J X F).inv ≫ Functor.whiskerRight P.π F }.π.app j

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ fst f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ fst f f

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ snd f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ snd f f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝ : HasZeroObject C
⊢ ⊤ 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
X Y : C
h : Retract Y X
hX : Q X
⊢ (h.r ≫ h.i) ≫ h.r ≫ h.i = h.r ≫ h.i

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y x : C
hx : Q x
r : Retract y x
⊢ (r.r ≫ r.i) ≫ r.r ≫ r.i = r.r ≫ r.i

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
⊢ ∀ (j : J),
    (constCocone J (F.obj ⊥)).ι.app j ≫ c.ι.app ⊥ =
      { app := fun k ↦ F.map (homOfLE ⋯), naturality := ⋯ }.app j ≫ c.ι.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.IsStableUnderColimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ ∀ (j : J), c₁✝.ι.app j ≫ h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι } = f.app j ≫ c₂✝.ι.app j

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
⊢ W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
⊢ ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ W f → W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f
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 S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯

Tactic:
simp

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 S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯

Tactic:
simp

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
⊢ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ ≫ fst g h = fst (fst f g) (fst f h) ≫ snd f g

Tactic:
simp

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

Goal state before:
pp: case refine_1.refine_2
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
c : PullbackCone (fst g h) (snd f g)
⊢ c.snd ≫ fst f g = lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯ ≫ fst f h

Tactic:
simp

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

Goal state before:
pp: case refine_3.h₀
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
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ fst f g = c.snd ≫ fst f g

Tactic:
simp

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

Goal state before:
pp: case h₁
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
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ snd f g = c.snd ≫ snd f g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
⊢ coproducts.{w, v, u} W f → W f

Tactic:
hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W f
⊢ W f
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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case refine_2
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 ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (gr ≫ pullback.snd (g ≫ f) f)

Tactic:
apply P.comp_mem

Goal state after:
case refine_2.hf
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 := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P gr

case refine_2.hg
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 := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (pullback.snd (g ≫ f) f)
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:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ P.universally f → P.universally (e.hom ≫ f)

Tactic:
hf

Goal state after:
case hprecomp
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
⊢ P.universally (e.hom ≫ f)
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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ P.universally f → P.universally (f ≫ e.hom)

Tactic:
hf

Goal state after:
case hpostcomp
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
⊢ P.universally (f ≫ e.hom)
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
⊢ P.universally f → P f

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ P f
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:
simp

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✝ : IsEmpty J
X : C
x✝ : Nonempty (IsTerminal X)
h : IsTerminal X
⊢ ∀ (j : J),
    P
      ({ diag := (Functor.const J).obj X, π := 𝟙 ((Functor.const J).obj X),
              isLimit :=
                (isLimitEquivIsTerminalOfIsEmpty C { pt := X, π := 𝟙 ((Functor.const J).obj X) }).symm h }.diag.obj
        j)

Tactic:
simp

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✝ : IsEmpty J
X : C
x✝ : Nonempty (IsInitial X)
h : IsInitial X
⊢ ∀ (j : J),
    P
      ({ diag := (Functor.const J).obj X, ι := 𝟙 ((Functor.const J).obj X),
              isColimit :=
                (isColimitEquivIsInitialOfIsEmpty C { pt := X, ι := 𝟙 ((Functor.const J).obj X) }).symm h }.diag.obj
        j)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
              (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
      (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.left } =
    ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
      (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after: