mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f g : Under X✝
φ : f ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Under (F.obj ((𝟭 T).obj X))
⊢ { app := fun A ↦ homMk (a.unit.app A.right) ⋯, naturality := ⋯ }.app ((post G ⋙ map (a.unit.app X)).obj A) ≫
      (post G ⋙ map (a.unit.app X)).map ({ app := fun A ↦ homMk (a.counit.app A.right) ⋯, naturality := ⋯ }.app A) =
    𝟙 ((post G ⋙ map (a.unit.app X)).obj A)

Tactic:
ext

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f g : Under X✝
φ : f ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Under (F.obj ((𝟭 T).obj X))
⊢ Hom.right
      ({ app := fun A ↦ homMk (a.unit.app A.right) ⋯, naturality := ⋯ }.app ((post G ⋙ map (a.unit.app X)).obj A) ≫
        (post G ⋙ map (a.unit.app X)).map ({ app := fun A ↦ homMk (a.counit.app A.right) ⋯, naturality := ⋯ }.app A)) =
    Hom.right (𝟙 ((post G ⋙ map (a.unit.app X)).obj A))
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
⊢ (liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc ((forget X).mapCocone t)) ⋯ = t.ι.app j

Tactic:
ext

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
⊢ Hom.right ((liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc ((forget X).mapCocone t)) ⋯) = Hom.right (t.ι.app j)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x✝ : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x✝ = t.ι.app j
⊢ x✝ = homMk (hc.desc ((forget X).mapCocone t)) ⋯

Tactic:
ext

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x✝ : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x✝ = t.ι.app j
⊢ Hom.right x✝ = Hom.right (homMk (hc.desc ((forget X).mapCocone t)) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ = 𝟙 (pullback f g)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) ≫ pullback.fst f g = 𝟙 (pullback f g) ≫ pullback.fst f g

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) ≫ pullback.snd f g = 𝟙 (pullback f g) ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯ = 𝟙 (pullback f g)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) ≫ pullback.fst f g = 𝟙 (pullback f g) ≫ pullback.fst f g

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) ≫ pullback.snd f g = 𝟙 (pullback f g) ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = 𝟙 (pushout f g)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inl f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inl f g ≫ 𝟙 (pushout f g)

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inr f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inr f g ≫ 𝟙 (pushout f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = 𝟙 (pushout f g)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inl f g ≫ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = pushout.inl f g ≫ 𝟙 (pushout f g)

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inr f g ≫ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = pushout.inr f g ≫ 𝟙 (pushout f g)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ (unop (op (Over.mk Z.hom.unop))).hom = (unop (op (Over.mk Y.hom.unop))).hom

Tactic:
by dsimp; rw [← unop_comp, Under.w]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ → W₁.HasFactorization W₂

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.HasFactorization W₂ → W₁.comp W₂ = ⊤
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
      Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯ =
    Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
      Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.left
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

case h₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.right
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasBinaryProduct X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h : i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g) = i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g)
⊢ i₁ = i₂

Tactic:
ext

Goal state after:
case h₀
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasBinaryProduct X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h : i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g) = i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g)
⊢ i₁ ≫ pullback.fst f g = i₂ ≫ pullback.fst f g

case h₁
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasBinaryProduct X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h : i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g) = i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g)
⊢ i₁ ≫ pullback.snd f g = i₂ ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom = 𝟙 (pullback f f)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst✝ : Epi g
W : C
h k : t.pt ⟶ W
i : t.inl ≫ h = t.inl ≫ k
⊢ t.inr ≫ h = t.inr ≫ k

Tactic:
simp [← cancel_epi g, ← t.condition_assoc, i]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ i₁ = i₂

Tactic:
ext

Goal state after:
case h₀
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂

case h₁
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
        (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop =
    ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ StructuredArrow.Hom.right
      ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
          (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop =
    StructuredArrow.Hom.right
      ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (pushoutSymmetry f f).hom = 𝟙 (pushout f f)

Tactic:
ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inl f f ≫ (pushoutSymmetry f f).hom = pushout.inl f f ≫ 𝟙 (pushout f f)

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ pushout.inr f f ≫ (pushoutSymmetry f f).hom = pushout.inr f f ≫ 𝟙 (pushout f f)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
        (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f).unop

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
          (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop.left =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
            f).unop.left
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ IsZero F

Tactic:
constructor

Goal state after:
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (F ⟶ Y))

case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (Y ⟶ F))
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
⊢ f = default

Tactic:
ext

Goal state after:
case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
x✝ : C
⊢ f.app x✝ = default.app x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
⊢ f = default

Tactic:
ext

Goal state after:
case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
x✝ : C
⊢ f.app x✝ = default.app x✝
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝

Tactic:
ext

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).1

case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).2
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f g : X ≅ 0
⊢ f = g

Tactic:
ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : 0 ⟶ X
Z✝ : C
g h : Z✝ ⟶ 0
x✝ : g ≫ f = h ≫ f
⊢ g = h

Tactic:
ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : X ⟶ 0
Z✝ : C
g h : 0 ⟶ Z✝
x✝ : f ≫ g = f ≫ h
⊢ g = h

Tactic:
ext

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝

Tactic:
ext

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).1.left

case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).2.left
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Cofork f g
⊢ s.ι.app zero = g ≫ s.π

Tactic:
by
  rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (preComp f g)

Tactic:
apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)
  exact epi_comp _ _

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ preComp f g ≫
      lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ } =
    𝟙 (image (f ≫ g))

Tactic:
ext

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ factorThruImage (f ≫ g) ≫
      preComp f g ≫
        lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ } =
    factorThruImage (f ≫ g) ≫ 𝟙 (image (f ≫ g))
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ } ≫
      preComp f g =
    𝟙 (image g)

Tactic:
ext

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ factorThruImage g ≫
      lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ } ≫
        preComp f g =
    factorThruImage g ≫ 𝟙 (image g)
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e ≫ ↟↑e.symm = 𝟙 (of R X₁)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₁)
⊢ (Hom.hom (↟↑e ≫ ↟↑e.symm)) x✝ = (Hom.hom (𝟙 (of R X₁))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e.symm ≫ ↟↑e = 𝟙 (of R X₂)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₂)
⊢ (Hom.hom (↟↑e.symm ≫ ↟↑e)) x✝ = (Hom.hom (𝟙 (of R X₂))) x✝