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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P.inverseImage F f
⊢ P.inverseImage F (e ≫ f)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P.inverseImage F f
⊢ P (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P.inverseImage F f
⊢ P.inverseImage F (f ≫ e)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P.inverseImage F f
⊢ P (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.inverseImage F).map F = P

Tactic:
erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫
      { left := F₁.obj Y.left, right := F₂.obj Y.right, hom := α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right }.hom =
    { left := F₁.obj X.left, right := F₂.obj X.right, hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right }.hom ≫
      R'.map (F₂.map φ.right)

Tactic:
by
        dsimp
        rw [assoc, assoc, ← Functor.comp_map, α.naturality_assoc, ← Functor.comp_map,
          ← β.naturality]
        dsimp
        rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w]

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right) =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right

Tactic:
rw [← Functor.comp_map, β.naturality]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G : AddCommGrpCat
h k : ↑G
w : asHom h = asHom k
⊢ h = k

Tactic:
simpa using

Goal state after:
G : AddCommGrpCat
h k : ↑G
w : asHom h = asHom k
⊢ h = k
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 : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
⊢ F.map f ≫ g = h ≫ k

Tactic:
simpa using

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
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
⊢ F.map f ≫ g = h ≫ k
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 : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k
⊢ f ≫ g = h ≫ G.map k

Tactic:
simpa using

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
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k
⊢ f ≫ g = h ≫ G.map k
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 : CoreUnitCounit F G
X : C
this :
  ∀ (x : C),
    (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x = (NatTrans.id (𝟭 C ⋙ F)).app x
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
simpa using

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
adj : CoreUnitCounit F G
X : C
this :
  ∀ (x : C),
    (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x = (NatTrans.id (𝟭 C ⋙ F)).app x
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
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 : CoreUnitCounit F G
Y : D
this :
  ∀ (x : D),
    (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x = (NatTrans.id (G ⋙ 𝟭 C)).app x
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)

Tactic:
simpa using

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
adj : CoreUnitCounit F G
Y : D
this :
  ∀ (x : D),
    (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x = (NatTrans.id (G ⋙ 𝟭 C)).app x
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: case mpr
X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
⊢ a = b → IsIso f

Tactic:
· rintro rfl
    rw [Subsingleton.elim f (𝟙 _)]
    infer_instance

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c

Tactic:
←
      cancel_epi (f ◁ (α_ _ _ _).inv),

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
t : F.obj X
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) = yoneda.map f.unop ≫ yonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
  rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
t : F.obj X
⊢ uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) =
    uliftYoneda.{w, v₁, u₁}.map f.unop ≫ uliftYonedaEquiv.symm t

Tactic:
by
  obtain ⟨u, rfl⟩ := uliftYonedaEquiv.surjective t
  rw [uliftYonedaEquiv_naturality]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)) x = (ConcreteCategory.hom (g.app X)) x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).map f ≫
              (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((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}).obj
                    X).map
                f)).toFun
        g).down

Tactic:
simpa using

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).obj Y
⊢ uliftYonedaEquiv (g ≫ f) = (ConcreteCategory.hom (f.app X)) (uliftYonedaEquiv g)
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

Goal state after:
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
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f.unop ≫ g) = (ConcreteCategory.hom (F.map f)) (uliftYonedaEquiv g)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                    X).map
                f)).toFun
        g).down

Tactic:
simpa using

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ coyonedaEquiv (g ≫ f) = (ConcreteCategory.hom (f.app X)) (coyonedaEquiv g)
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 v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                    f).app
              F)).toFun
        g).down

Tactic:
simpa using

Goal state after:
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 v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ coyonedaEquiv (coyoneda.map f.op ≫ g) = (ConcreteCategory.hom (F.map f)) (coyonedaEquiv g)
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ c.π.app j ≫ F.map f = c.π.app j'

Tactic:
simpa using

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ c.π.app j ≫ F.map f = c.π.app j'
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : C
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : C
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)) x = (ConcreteCategory.hom (g.app X)) x
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ f = f'

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ f = f'
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
              (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((uliftCoyonedaEquiv.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}).obj
                    X).map
                f)).toFun
        g).down

Tactic:
simpa using

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ uliftCoyonedaEquiv (g ≫ f) = (ConcreteCategory.hom (f.app X)) (uliftCoyonedaEquiv g)
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 : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.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

Goal state after:
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 : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ g) = (ConcreteCategory.hom (F.map f)) (uliftCoyonedaEquiv g)
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 : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
k : K
⊢ (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).π.app k =
    (Iso.refl (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).pt).hom ≫
      ((𝟭 (Cone (e.functor ⋙ F))).obj s).π.app k

Tactic:
simpa using

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 : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
k : K
⊢ s.π.app (e.inverse.obj (e.functor.obj k)) ≫ F.map (e.functor.map (e.unitInv.app k)) = s.π.app k
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 : J ⥤ C
G : C ⥤ D
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (G.preimage t.hom ≫ Y✝.π.app j) = G.map (X✝.π.app j)

Tactic:
simpa using

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 : J ⥤ C
G : C ⥤ D
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ t.hom ≫ G.map (Y✝.π.app j) = G.map (X✝.π.app j)
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi f → StrongEpi (F.map f)

Tactic:
· intro
    infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ ((Functor.const J).obj (F.obj X)).map k

Tactic:
dsimp
        rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Mono (α.app j)
Z : C
u v : Z ⟶ limit F
h : u ≫ limMap α = v ≫ limMap α
j : J
⊢ (u ≫ limit.π F j) ≫ α.app j = (v ≫ limit.π F j) ≫ α.app j

Tactic:
simpa using

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Mono (α.app j)
Z : C
u v : Z ⟶ limit F
h : u ≫ limMap α = v ≫ limMap α
j : J
⊢ u ≫ limit.π F j ≫ α.app j = v ≫ limit.π F j ≫ α.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✝ F G : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Epi (α.app j)
Z : C
u v : colimit G ⟶ Z
h : colimMap α ≫ u = colimMap α ≫ v
j : J
⊢ α.app j ≫ colimit.ι G j ≫ u = α.app j ≫ colimit.ι G j ≫ v

Tactic:
simpa using

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✝ F G : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Epi (α.app j)
Z : C
u v : colimit G ⟶ Z
h : colimMap α ≫ u = colimMap α ≫ v
j : J
⊢ α.app j ≫ colimit.ι G j ≫ u = α.app j ≫ colimit.ι G j ≫ v
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt
w :
  m ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        default =
    s.π.app default
⊢ m = s.π.app default

Tactic:
simpa using

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt
w :
  m ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        default =
    s.π.app default
⊢ m = s.π.app default
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv

Tactic:
simpa using

Goal state after:
case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m ≫ e.hom = s.proj default
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ (c.fst ≫ l) ≫ c.fst = 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }) ≫ c.fst

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ c.fst ≫ 𝟙 X = c.fst