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

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).1 = eqToHom ⋯

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).2 = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj✝ : Cᵒᵖ → D
map✝ : {X Y : Cᵒᵖ} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : Cᵒᵖ), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
⊢ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.rightOp.leftOp =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x : (i : I) → C i
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom

Tactic:
rfl

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ C i ≌ C i

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (G.obj (unop x✝))).op = 𝟙 (op (G.obj (unop x✝)))

Tactic:
rfl

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ eval C i ⋙ (eqToEquivalence C ⋯).functor = eval C i

Tactic:
rfl

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' : J
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) ⋯).functor

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
as✝ : C
⊢ { as := as✝ } = { as := { as := as✝ }.as }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj (unop x✝))).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
unop✝ : C
f : Opposite.unop (Opposite.op unop✝) ⟶ Opposite.unop (Opposite.op (Opposite.unop (Opposite.op unop✝)))
⊢ Opposite.op (Opposite.unop (Opposite.op unop✝)) = Opposite.op unop✝

Tactic:
rfl

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

Goal state before:
pp: case mk
T : Type u
inst✝ : Category.{v, u} T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk (hom { left := left✝, right := right✝, hom := hom✝ }) = { left := left✝, right := right✝, hom := hom✝ }

Tactic:
rfl

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

Goal state before:
pp: case refl
T : Type u
inst✝ : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage F f ↔ P (F.map f)

Tactic:
rfl

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

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
S : Type u
as✝ : S
f : (𝟭 (Discrete S)).obj { as := as✝ } ⟶ (𝟭 (Discrete S)).obj { as := ((𝟭 (Discrete S)).obj { as := as✝ }).as }
⊢ (fun s ↦ mk (𝟙 { as := s }))
      ((fun f ↦ f.left.as)
        { left := { as := as✝ }, right := { as := ((𝟭 (Discrete S)).obj { as := as✝ }).as }, hom := f }) =
    { left := { as := as✝ }, right := { as := ((𝟭 (Discrete S)).obj { as := as✝ }).as }, hom := f }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx0 : f0x0 ≫ fx10 = fx00 ≫ f1x0
inst✝ : Epi f00x
⊢ f00x ≫ f0x1 ≫ fx11 = f00x ≫ fx01 ≫ f1x1

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx1 : f0x1 ≫ fx11 = fx01 ≫ f1x1
inst✝ : Mono f11x
⊢ (f0x0 ≫ fx10) ≫ f11x = (fx00 ≫ f1x0) ≫ f11x

Tactic:
grind

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

Goal state before:
pp: X Y : Type u
x✝ : Fun X Y
⊢ (fun f ↦ { toFun := f }) ((fun f ↦ ⇑f) x✝) = x✝

Tactic:
rfl

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

Goal state before:
pp: X Y : Type u
x✝ : X → Y
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f }) x✝) = x✝

Tactic:
rfl

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom f)

Tactic:
rfl

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x : X
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : Fun X Y
⊢ ⇑f = ⇑f

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : Fun X Y
x : X
⊢ f x = f x

Tactic:
rfl

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

Goal state before:
pp: X : Type u
⊢ ToType X = X

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f ↔ IsIso f

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ monomorphisms C f ↔ Mono f

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ epimorphisms C f ↔ Epi f

Tactic:
rfl

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

Goal state before:
pp: case refl
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
X : Comma L R
⊢ X.left = X.left

Tactic:
rfl

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

Goal state before:
pp: case refl
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
X : Comma L R
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
rfl

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

Goal state before:
pp: case refl
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
X : Comma L R
⊢ X.right = X.right

Tactic:
rfl

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

Goal state before:
pp: case refl
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
X : Comma L R
⊢ (eqToHom ⋯).right = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : C
val✝¹ inv✝¹ : End X
val_inv✝¹ : val✝¹ * inv✝¹ = 1
inv_val✝¹ : inv✝¹ * val✝¹ = 1
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ {
      hom :=
        ↑({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
            { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }),
      inv :=
        ({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
            { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }).inv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := ↑{ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ },
        inv := { val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ } *
      { hom := ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ },
        inv := { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ }

Tactic:
rfl

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 ≫ (R ⋙ F).map (F₂.preimage φ.right) ≫ β.app Y.right

Tactic:
β.naturality

Goal state after:
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 ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right)
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X : MonCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
rfl

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

Goal state before:
pp: X Y Z : MonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
rfl

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

Goal state before:
pp: X : CommMonCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
rfl

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

Goal state before:
pp: X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
rfl

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

Goal state before:
pp: X : GrpCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
rfl

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

Goal state before:
pp: X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
rfl

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

Goal state before:
pp: X : CommGrpCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
rfl

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

Goal state before:
pp: X Y Z : CommGrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
rfl

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
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ ↑p j' = ↑p j ≫ F.map f

Tactic:
exact (p.2 f).symm

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

Goal state before:
pp: case mk
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
X : C
h : F.cones.RepresentableBy X
j : J
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
h₁ : { pt := pt✝, π := π✝ }.pt = pt✝
h₂ : (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π = π✝
⊢ homOfCone h { pt := pt✝, π := π✝ } ≫ (limitCone h).π.app j =
    { pt := pt✝, π := (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π }.π.app j

Tactic:
rfl

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
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    (e (G_obj Y) Y'').symm
      ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫
        (e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'))

Tactic:
← he'' e he,

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
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫
      (e (G_obj Y') Y'').symm ((e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'))
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case mk
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
X : C
h : F.cocones.CorepresentableBy X
j : J
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
h₁ : { pt := pt✝, ι := ι✝ }.pt = pt✝
h₂ : (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) = ι✝
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt✝, ι := ι✝ } =
    { pt := pt✝, ι := (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) }.ι.app j

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.ULift

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

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝¹ : Preorder X
inst✝ : OrderTop X
x : X
a : x ⟶ ⊤
⊢ a = homOfLE ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝¹ : Preorder X
inst✝ : OrderBot X
x : X
a : ⊥ ⟶ x
⊢ a = homOfLE ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e, homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e, homEquiv_comp := he' }.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = { homEquiv := e, homEquiv_comp := he' }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e, homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e, homEquiv_comp := he' }.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = { homEquiv := e, homEquiv_comp := he' }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
yonedaEquiv_yoneda_map

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.app (op Y))) g = (ConcreteCategory.hom (f.app (op Y))) g
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
yonedaEquiv_yoneda_map

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (op (unop Y)))) g.unop = (ConcreteCategory.hom (f.app Y)) g.unop
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
x✝¹ x✝ : ThinSkeleton C
f₁ down✝ : x✝¹ ≤ x✝
⊢ { down := { down := f₁ } } = { down := { down := down✝ } }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F G : C ⥤ Type v₁
α : coyoneda.obj (op X) ⟶ F
β : F ⟶ G
⊢ coyonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app X)) (coyonedaEquiv α)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case ofFunctor
C D : Cat
toFunctor✝ : ↑C ⥤ ↑D
⊢ 𝟙 C ≫ { toFunctor := toFunctor✝ } = { toFunctor := toFunctor✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case ofFunctor
C D : Cat
toFunctor✝ : ↑C ⥤ ↑D
⊢ { toFunctor := toFunctor✝ } ≫ 𝟙 D = { toFunctor := toFunctor✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = F.toFunctor.rightUnitor

Tactic:
rfl

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

Goal state before:
pp: case mk
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✝ F : J ⥤ C
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd })).toFun
      { pt := pt✝, π := π✝ } =
    (ConcreteCategory.hom (𝟙 (Cone F))).toFun { pt := pt✝, π := π✝ }

Tactic:
rfl

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

Goal state before:
pp: case fst.mk
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✝ F : J ⥤ C
fst✝ : Cᵒᵖ
snd✝ : (const J).obj (unop fst✝) ⟶ F
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun
        ⟨fst✝, snd✝⟩).fst =
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun ⟨fst✝, snd✝⟩).fst

Tactic:
rfl

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

Goal state before:
pp: case snd
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✝ F : J ⥤ C
X : (X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun X).snd

Tactic:
rfl

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

Goal state before:
pp: case mk
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✝ F : J ⥤ C
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd })).toFun { pt := pt✝, ι := ι✝ } =
    (ConcreteCategory.hom (𝟙 (Cocone F))).toFun { pt := pt✝, ι := ι✝ }

Tactic:
rfl

Goal state after: