awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C
⊢ HasColimitsOfSize.{v₁, u₁, v, u} C

Tactic:
hasColimitsOfSizeOfUnivLE.{max v₁ v₂, max u₁ u₂} C

Premises used: CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimits.{v, u} C
⊢ HasColimitsOfSize.{0, 0, v, u} C

Tactic:
hasColimitsOfSizeShrink.{0, 0} C

Premises used: CategoryTheory.Limits.hasColimitsOfSizeShrink
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : m = Quiver.Hom.op (P.lift s.unop)
⊢ m = Quiver.Hom.op (P.lift s.unop)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
rw : m = m.unop.op
rw₁ : ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j
⊢ m = Quiver.Hom.op (P.lift s.unop)

Tactic:
rw [← P.uniq s.unop m.unop]

Premises used: Quiver.Hom.unop, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Limits.Cocone.unop
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : ∀ (j : J), m.unop ≫ t.π.app j = Quiver.Hom.unop (s.ι.app (Opposite.op j))
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
rw : m.unop ≫ t.π.app j = Quiver.Hom.unop (t.op.ι.app (Opposite.op j) ≫ m)
⊢ m.unop ≫ t.π.app j = Quiver.Hom.unop (s.ι.app (Opposite.op j))

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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 = Quiver.Hom.unop (t.op.ι.app (Opposite.op j) ≫ m)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : m = Quiver.Hom.op (P.desc s.unop)
⊢ m = Quiver.Hom.op (P.desc s.unop)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
rw : m = m.unop.op
rw₁ : ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j
⊢ m = Quiver.Hom.op (P.desc s.unop)

Tactic:
rw [← P.uniq s.unop m.unop]

Premises used: Quiver.Hom.unop, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.Cone.unop
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : ∀ (j : J), t.ι.app j ≫ m.unop = Quiver.Hom.unop (s.π.app (Opposite.op j))
⊢ ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
rw : t.ι.app j ≫ m.unop = Quiver.Hom.unop (m ≫ t.op.π.app (Opposite.op j))
⊢ t.ι.app j ≫ m.unop = Quiver.Hom.unop (s.π.app (Opposite.op j))

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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 = Quiver.Hom.unop (m ≫ t.op.π.app (Opposite.op j))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : m = Quiver.Hom.unop (P.lift s.op)
⊢ m = Quiver.Hom.unop (P.lift s.op)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
rw : m = m.op.unop
rw₁ : ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = s.op.π.app j
⊢ m = Quiver.Hom.unop (P.lift s.op)

Tactic:
rw [← P.uniq s.op m.op]

Premises used: Quiver.Hom.op, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Limits.Cocone.op
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = Quiver.Hom.op (s.ι.app (Opposite.unop j))
⊢ ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = s.op.π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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ᵒᵖ
rw : m.op ≫ t.π.app j = Quiver.Hom.op (t.unop.ι.app (Opposite.unop j) ≫ m)
⊢ m.op ≫ t.π.app j = Quiver.Hom.op (s.ι.app (Opposite.unop j))

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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 = Quiver.Hom.op (t.unop.ι.app (Opposite.unop j) ≫ m)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : m = Quiver.Hom.unop (P.desc s.op)
⊢ m = Quiver.Hom.unop (P.desc s.op)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
rw : m = m.op.unop
rw₁ : ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = s.op.ι.app j
⊢ m = Quiver.Hom.unop (P.desc s.op)

Tactic:
rw [← P.uniq s.op m.op]

Premises used: Quiver.Hom.op, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.Cone.op
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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
dsimp : ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = Quiver.Hom.op (s.π.app (Opposite.unop j))
⊢ ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = s.op.ι.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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ᵒᵖ
rw : t.ι.app j ≫ m.op = Quiver.Hom.op (m ≫ t.unop.π.app (Opposite.unop j))
⊢ t.ι.app j ≫ m.op = Quiver.Hom.op (s.π.app (Opposite.unop j))

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} 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 = Quiver.Hom.op (m ≫ t.unop.π.app (Opposite.unop j))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
i : I
⊢ Eq (α := Functor.obj coyoneda (op (colimit F)) ⟶ (F.op ⋙ coyoneda).obj (op i))
    (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F) ≫ limit.π (F.op ⋙ coyoneda) (op i))
    (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F i)))

Tactic:
simp only [coyonedaOpColimitIsoLimitCoyoneda, Functor.mapIso_symm,
    Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π,
    ← Functor.map_comp, limitOpIsoOpColimit_inv_comp_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.mapIso_symm, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π, CategoryTheory.preservesLimitIso_hom_π, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
i : I
rw :
  Eq (α := limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda F))
        (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F) ≫ limit.π (F.op ⋙ coyoneda) (op i)) :
      limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (limit.π (F.op ⋙ coyoneda) (op i) : limit (F.op ⋙ coyoneda) ⟶ (F.op ⋙ coyoneda).obj (op i))
rw₁ :
  Eq (α := limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (CategoryStruct.comp (Y := limit (F.op ⋙ coyoneda))
        (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F)))
            (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda F)) (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F)) :
          limit (F.op ⋙ coyoneda) ⟶ limit (F.op ⋙ coyoneda))
        (limit.π (F.op ⋙ coyoneda) (op i) : limit (F.op ⋙ coyoneda) ⟶ (F.op ⋙ coyoneda).obj (op i)) :
      limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (limit.π (F.op ⋙ coyoneda) (op i) : limit (F.op ⋙ coyoneda) ⟶ (F.op ⋙ coyoneda).obj (op i))
rw₂ :
  Eq (α := limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (𝟙 (limit (F.op ⋙ coyoneda)) ≫ limit.π (F.op ⋙ coyoneda) (op i)) (limit.π (F.op ⋙ coyoneda) (op i))
rw₃ rw₄ :
  Eq (α := limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i))) (limit.π (F.op ⋙ coyoneda) (op i))
    (limit.π (F.op ⋙ coyoneda) (op i))
⊢ Eq (α := limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda F))
        (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F i))) :
      limit (F.op ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj i)))
    (limit.π (F.op ⋙ coyoneda) (op i) : limit (F.op ⋙ coyoneda) ⟶ (F.op ⋙ coyoneda).obj (op i))

Tactic:
rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} Iᵒᵖ (Type u₂)
A : C
i : I
simp :
  Eq (α := (colimit F ⟶ A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F)) A ≫
      CategoryStruct.comp (Y := limit (F.op ⋙ Functor.obj yoneda A))
        (Iso.hom (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A) :
          (limit (F.op ⋙ coyoneda)).obj A ⟶ limit (F.op ⋙ Functor.obj yoneda A))
        (limit.π (F.op ⋙ Functor.obj yoneda A) (op i) :
          limit (F.op ⋙ Functor.obj yoneda A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i)))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))
⊢ Eq (α := (colimit F ⟶ A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
    (Iso.hom (colimitHomIsoLimitYoneda F A) ≫ limit.π (F.op ⋙ Functor.obj yoneda A) (op i))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))

Tactic:
simp only [colimitHomIsoLimitYoneda, Iso.trans_hom, Iso.app_hom, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.app_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.colimitHomIsoLimitYoneda
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} Iᵒᵖ (Type u₂)
A : C
i : I
erw :
  Eq (α := (colimit F ⟶ A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F)) A ≫ NatTrans.app (limit.π (F.op ⋙ coyoneda) (op i)) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))
⊢ Eq (α := (colimit F ⟶ A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F)) A ≫
      CategoryStruct.comp (Y := limit (F.op ⋙ Functor.obj yoneda A))
        (Iso.hom (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A) :
          (limit (F.op ⋙ coyoneda)).obj A ⟶ limit (F.op ⋙ Functor.obj yoneda A))
        (limit.π (F.op ⋙ Functor.obj yoneda A) (op i) :
          limit (F.op ⋙ Functor.obj yoneda A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i)))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))

Tactic:
erw [limitObjIsoLimitCompEvaluation_hom_π]

Premises used: CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} Iᵒᵖ (Type u₂)
A : C
i : I
change :
  Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.op ⋙ coyoneda).obj (op i)).obj A)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F) ≫ limit.π (F.op ⋙ coyoneda) (op i)) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))
⊢ Eq (α := (colimit F ⟶ A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F)) A ≫ NatTrans.app (limit.π (F.op ⋙ coyoneda) (op i)) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))

Tactic:
change ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ _).app A = _

Premises used: CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} Iᵒᵖ (Type u₂)
A : C
i : I
rw :
  Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.op ⋙ coyoneda).obj (op i)).obj A)
    (NatTrans.app (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F i))) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))
rw₁ rw₂ :
  Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.op ⋙ coyoneda).obj (op i)).obj A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)) :
      Functor.obj (Functor.obj yoneda A) (op (colimit F)) ⟶ Functor.obj (Functor.obj yoneda A) (op (F.obj i)))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))
⊢ Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.op ⋙ coyoneda).obj (op i)).obj A)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda F) ≫ limit.π (F.op ⋙ coyoneda) (op i)) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F i)))

Tactic:
rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, Functor.flip_map_app]

Premises used: CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, CategoryTheory.Functor.flip_map_app
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} I C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} Iᵒᵖ (Type u₂)
A : C
i : I
rw :
  Eq (α := limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda F A))
        (Iso.hom (colimitHomIsoLimitYoneda F A) ≫ limit.π (F.op ⋙ Functor.obj yoneda A) (op i)) :
      limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (limit.π (F.op ⋙ Functor.obj yoneda A) (op i) :
      limit (F.op ⋙ Functor.obj yoneda A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
rw₁ :
  Eq (α := limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (CategoryStruct.comp (Y := limit (F.op ⋙ Functor.obj yoneda A))
        (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda F A))
            (Iso.hom (colimitHomIsoLimitYoneda F A)) :
          limit (F.op ⋙ Functor.obj yoneda A) ⟶ limit (F.op ⋙ Functor.obj yoneda A))
        (limit.π (F.op ⋙ Functor.obj yoneda A) (op i) :
          limit (F.op ⋙ Functor.obj yoneda A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i)) :
      limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (limit.π (F.op ⋙ Functor.obj yoneda A) (op i) :
      limit (F.op ⋙ Functor.obj yoneda A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))
rw₂ :
  Eq (α := limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (𝟙 (limit (F.op ⋙ Functor.obj yoneda A)) ≫ limit.π (F.op ⋙ Functor.obj yoneda A) (op i))
    (limit.π (F.op ⋙ Functor.obj yoneda A) (op i))
rw₃ rw₄ :
  Eq (α := limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A) (limit.π (F.op ⋙ Functor.obj yoneda A) (op i))
    (limit.π (F.op ⋙ Functor.obj yoneda A) (op i))
⊢ Eq (α := limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda F A))
        (↾fun (g : colimit F ⟶ A) ↦ colimit.ι F i ≫ g) :
      limit (F.op ⋙ Functor.obj yoneda A) ⟶ F.obj i ⟶ A)
    (limit.π (F.op ⋙ Functor.obj yoneda A) (op i) :
      limit (F.op ⋙ Functor.obj yoneda A) ⟶ (F.op ⋙ Functor.obj yoneda A).obj (op i))

Tactic:
rw [← dsimp% colimitHomIsoLimitYoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Premises used: CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π, CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
i : I
⊢ Eq (α := Functor.obj coyoneda (op (colimit F)) ⟶ (F.rightOp ⋙ coyoneda).obj i)
    (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i)
    (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i))))

Tactic:
simp only [coyonedaOpColimitIsoLimitCoyoneda', Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
    Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π, ← Functor.map_comp,
    limitRightOpIsoOpColimit_inv_comp_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda', CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.mapIso_symm, CategoryTheory.Functor.mapIso_inv, CategoryTheory.preservesLimitIso_hom_π, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π