mathlib-initiative/mathlib-tactics huggingface dataset:
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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
j : J
⊢ { pt := c₁'.pt, π := c₁'.π ≫ f }.π.app j = g ≫ c₂'.π.app 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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
j : J
⊢ { pt := c₁'.pt, π := c₁'.π ≫ f }.π.app j = g ≫ c₂'.π.app j
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) g ↔
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) g

Tactic:
]

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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } })

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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } })
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P ((↑e.symm).comp (algebraMap R' S'))

Tactic:
]

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P ((↑e.symm).comp (algebraMap R' S'))
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.IsStableUnderLimitsOfShape J
⊢ W.IsStableUnderLimitsOfShape 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.IsStableUnderLimitsOfShape J
⊢ W.IsStableUnderLimitsOfShape J
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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
⊢ ⊥.strictLimitsOfShape 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
⊢ ⊥.strictLimitsOfShape J ≤ ⊥
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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
⊢ ⊥.limitsOfShape 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
⊢ ⊥.limitsOfShape J ≤ ⊥
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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.strictLimitsOfShape J ≤ P.limitsOfShape 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.strictLimitsOfShape J ≤ P.limitsOfShape J
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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.EssentiallySmall.{w, v_1, u_1} (P.strictLimitsOfShape J).isoClosure

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✝³ : 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.EssentiallySmall.{w, v_1, u_1} (P.strictLimitsOfShape J).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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.strictLimitsOfShape J ≤ P
⊢ (P.strictLimitsOfShape 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.strictLimitsOfShape J ≤ P
⊢ (P.strictLimitsOfShape J).isoClosure ≤ P.isoClosure
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
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })

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
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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.LimitsOfShape

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.IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape 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.IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape J
Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
Z₀ : C
hZ₀ : IsZero Z₀
h₀ : P Z₀
⊢ P Z

Tactic:
exact P.prop_of_iso (hZ₀.iso hZ) h₀

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
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₂ ≫ g' =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ ≫ g'

Tactic:
]

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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
⊢ { pt := c₂'.pt, ι := f ≫ c₂'.ι }.ι.app j = c₁'.ι.app j ≫ g

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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
⊢ { pt := c₂'.pt, ι := f ≫ c₂'.ι }.ι.app j = c₁'.ι.app j ≫ 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 : 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.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
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)
j : Fin (n + 1)
i : Fin n
⊢ { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }.ι.app { as := i } =
    s.ι.app { as := i.succ }

Tactic:
]

Goal state after:
case refine_2
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)
j : Fin (n + 1)
i : Fin n
⊢ { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }.ι.app { as := i } =
    s.ι.app { as := i.succ }
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
⊢ c₂.inl ≫ m = s.ι.app { as := 0 }

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
⊢ c₂.inl ≫ m = s.ι.app { as := 0 }
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ Q ≤ Q

Tactic:
]

Goal state after:
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
⊢ c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }

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
⊢ c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }
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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
⊢ W.colimitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } })

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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
⊢ W.colimitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } })
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.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
⊢ Q.retractClosure ≤ (ofObj Y).isoClosure

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
⊢ Q.retractClosure ≤ (ofObj Y).isoClosure