mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m = (extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m

Tactic:
]

Goal state after:
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m = (extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m
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 ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯ ≫ x✝)

Tactic:
]

Goal state after:
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 ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯ ≫ x✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m = c₁.ι.app { as := j } ≫ c₂.inr ≫ m

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : K ≅ Discrete.functor fun n_1 ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit (Discrete.functor fun n_1 ↦ K.obj { as := n_1 })

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : K ≅ Discrete.functor fun n_1 ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit (Discrete.functor fun n_1 ↦ K.obj { as := n_1 })
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 : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : (g (h a) h₁).fst = (g r hx).fst ∧ (g (h a) h₁).snd = (g r hx).snd
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i

Tactic:
]

Goal state after:
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 : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : (g (h a) h₁).fst = (g r hx).fst ∧ (g (h a) h₁).snd = (g r hx).snd
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i
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
inst✝ : W.IsStableUnderColimitsOfShape J
⊢ W.IsStableUnderColimitsOfShape J

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : W.IsStableUnderColimitsOfShape J
⊢ W.IsStableUnderColimitsOfShape J
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ ∃ J, W.colimitsOfShape (Discrete J) f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ ∃ J, W.colimitsOfShape (Discrete J) f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ W.colimitsOfShape (Discrete J) f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ W.colimitsOfShape (Discrete J) f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : 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₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁

Tactic:
]

Goal state after:
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₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι }.ι.app (⊥_ Discrete PUnit.{w + 1}) =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι }.ι.app (⊥_ Discrete PUnit.{w + 1}) =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f
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₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι } = f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι })

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι } = f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι })
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J, W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J, W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f
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✝ Z : 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₃
⊢ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂

Tactic:
]

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₃
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ = map f g f' g' i₁ i₂ i₃ e₁ e₂

Tactic:
]

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₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ ≫ fst (fst f' g') i₁ =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂

Tactic:
rw [lift_fst, lift_fst]

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
hf : ∃ J, W.colimitsOfShape (Discrete J) f
⊢ W f

Tactic:
]

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 : ∃ J, W.colimitsOfShape (Discrete J) f
⊢ W f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_coproducts

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.strictColimitsOfShape J ≤ ⊥

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.strictColimitsOfShape J ≤ ⊥
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.colimitsOfShape J ≤ ⊥

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.colimitsOfShape J ≤ ⊥
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_1
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 ≤ P.colimitsOfShape J

Tactic:
]

Goal state after:
case refine_1
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 ≤ P.colimitsOfShape J
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
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
⊢ P (pullback.diagonal f)

Tactic:
]

Goal state after:
case hprecomp
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
⊢ P (pullback.diagonal 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
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv = pullback.diagonal f.op

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv = pullback.diagonal f.op
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

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

Tactic:
]

Goal state after:
case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
⊢ P (pullback.diagonal 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.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
    (pullback.diagonal x✝¹ ≫
      (pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫
        pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))

Tactic:
]

Goal state after:
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
    (pullback.diagonal x✝¹ ≫
      (pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫
        pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))
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.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))

Tactic:
]

Goal state after:
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.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))
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 (inv (inl f f))

Tactic:
]

Goal state after:
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 (inv (inl f f))
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:
]

Goal state after:
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)
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.strictColimitsOfShape J).isoClosure ≤ P.isoClosure

Tactic:
]

Goal state after:
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.strictColimitsOfShape J).isoClosure ≤ P.isoClosure
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:
]

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
⊢ ⊥ ≤ ⊥

Tactic:
]

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

Goal state after:
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
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
⊢ IsPullback (f ≫ pushout.inl f g).op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯).op (pushout.codiagonal i).op
    (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯).op

Tactic:
]

Goal state after:
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
⊢ IsPullback (f ≫ pushout.inl f g).op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯).op (pushout.codiagonal i).op
    (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯).op
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)
⊢ i₁ = i₁

Tactic:
]

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.op.limitsOfShape J

Tactic:
]

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.op.colimitsOfShape J

Tactic:
]

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.op ↔ P.op.limitsOfShape Jᵒᵖ ≤ P.op

Tactic:
]

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.op ↔ P.op.colimitsOfShape Jᵒᵖ ≤ P.op

Tactic:
]

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)
H : IsPullback (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g = f'
⊢ P (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g)

Tactic:
]

Goal state after:
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)
H : IsPullback (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g = f'
⊢ P (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g)
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 ↔ P.colimitsOfShape Jᵒᵖ ≤ P

Tactic:
]

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 = f

Tactic:
]

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 ↔ P.limitsOfShape Jᵒᵖ ≤ P

Tactic:
]

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.IsClosedUnderColimitsOfShape J

Tactic:
]

Goal state after:
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.IsClosedUnderColimitsOfShape J
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.IsClosedUnderLimitsOfShape J

Tactic:
]

Goal state after:
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.IsClosedUnderLimitsOfShape J