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

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

Tactic:
Y

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
Y

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
Y

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
Y

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
by
    rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]
    simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) ≫
      P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) =
    𝟙 s.pt

Tactic:
apply hom_ext P; intro j
      dsimp [w']
      simp only [Limits.Cone.whisker_π, Limits.Cone.postcompose_obj_π, fac, whiskerLeft_app,
        assoc, id_comp, invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]
      rw [counit_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]
      simp

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f : (const J).obj W ⟶ F
j : J
⊢ h.homEquiv.symm f ≫ t.π.app j = f.app j

Tactic:
simp [homEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
⊢ ∀ {Y : D} (f : X ⟶ X') (g : X' ⟶ (rightAdjointOfEquiv e he).obj Y), (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g

Tactic:
Y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
Y : D
⊢ ∀ (f : X ⟶ X') (g : X' ⟶ (rightAdjointOfEquiv e he).obj Y), (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
⊢ ∀ {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (e X Y') (f ≫ g) = (e X Y) f ≫ (rightAdjointOfEquiv e he).map g

Tactic:
Y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
Y : D
⊢ ∀ {Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (e X Y') (f ≫ g) = (e X Y) f ≫ (rightAdjointOfEquiv e he).map g
Module: Mathlib.CategoryTheory.Category.ULift

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : AsSmall C
h : X = Y
⊢ (eqToHom h).down = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : AsSmall C
⊢ (eqToHom ⋯).down = eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ IsIso (homOfLE ⋯)

Tactic:
subst h

Goal state after:
X : Type u
inst✝ : Preorder X
x : X
⊢ IsIso (homOfLE ⋯)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X : Cᵒᵖ
⊢ ∀ {Y : Cᵒᵖ} (f : X ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
Y

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X Y : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X✝ : C
R : F.CorepresentableBy X✝
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y),
    (uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
Y

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X✝ : C
R : F.CorepresentableBy X✝
X Y : C
⊢ ∀ (f : X ⟶ Y),
    (uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ ∀ {Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f

Tactic:
Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X : Cᵒᵖ
⊢ ∀ {Y : Cᵒᵖ} (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
      yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f

Tactic:
Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
      yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f) = { down := f }

Tactic:
by
  simp [uliftYonedaEquiv, uliftYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type (max w v₁)
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                        (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).map
                    f).app
              F)).toFun
        g).down

Tactic:
simpa using (uliftYonedaEquiv_naturality _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom ≫ (evaluation C (Type u₁)).map f

Tactic:
Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : C
⊢ ∀ (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom ≫ (evaluation C (Type u₁)).map f
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.21 + 1} ⥤ C
X : Discrete PUnit.{?u.21 + 1}
⊢ ∀ ⦃Y : Discrete PUnit.{?u.21 + 1}⦄ (f : X ⟶ Y),
    (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).map f ≫
        match Y with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
      (match X with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
        F.map f

Tactic:
Y

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.21 + 1} ⥤ C
X Y : Discrete PUnit.{?u.21 + 1}
⊢ ∀ (f : X ⟶ Y),
    (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).map f ≫
        match Y with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
      (match X with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
        F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫
        coyonedaEquiv.toIso.hom =
      coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f

Tactic:
Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
X Y : C
⊢ ∀ (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫
        coyonedaEquiv.toIso.hom =
      coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map
X✝ : Type u
X : Discrete X✝
⊢ ∀ (Y : Discrete X✝) (f : X ⟶ Y),
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map f =
      eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
case h_map
X✝ : Type u
X Y : Discrete X✝
⊢ ∀ (f : X ⟶ Y),
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map f =
      eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none

pp: case some.none.term.term
J : Type w
b : J
⊢ Hom.term b = Hom.term b

pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
· rfl

Goal state after:
case some.none.term.term
J : Type w
b : J
⊢ Hom.term b = Hom.term b

case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some.none.term.term
J : Type w
b : J
⊢ Hom.term b = Hom.term b

pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
· rfl

Goal state after:
case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
· rfl

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

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePullbackShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
by
  constructor
  intro a b
  casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
  · rfl
  · rfl
  · rfl

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = m.unop.op

pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j

Tactic:
· rfl

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ m = m.unop.op

pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j

Tactic:
· rfl

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ m = m.op.unop

pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = s.op.π.app j

Tactic:
· rfl

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = s.op.π.app j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ m = m.op.unop

pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = s.op.ι.app j

Tactic:
· rfl

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = s.op.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)

Tactic:
· exact facπ t _

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
S : D
T : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X : StructuredArrow S T
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left.left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.left } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.left }

pp: case left.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.right } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.right }

Tactic:
· simpa using w ⟨.left⟩

Goal state after:
case left.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.right } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
h : f = g
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Over X
⊢ Hom.left (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Under X
h : f = g
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f : Under X
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯
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
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ (eqToHom h).left = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom ⋯).left = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: 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)

Tactic:
simp [pushout.condition]

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
    · simpa using congrArg (fun f => coprod.inl ≫ f) h
    · simpa using congrArg (fun f => coprod.inr ≫ f) h

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 f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ (image.eqToHom h ≫ image.eqToHom ⋯) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f

Tactic:
subst h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasImage f
⊢ (image.eqToHom ⋯ ≫ image.eqToHom ⋯) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ (image.eqToHom ⋯ ≫ image.eqToHom h) ≫ image.ι f' = 𝟙 (image f') ≫ image.ι f'

Tactic:
subst h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasImage f
⊢ (image.eqToHom ⋯ ≫ image.eqToHom ⋯) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f