awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
J' : Type u₂
inst_2 : Category.{v₂, u₂} J'
e : Equivalence.{v₁, v₂, u₁, u₂} J J'
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J' C
have has_colimit : autoParam (∀ (F : Functor.{v₂, v, u₂, u} J' C), HasColimit F) HasColimitsOfShape.has_colimit._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : Small.{u₁, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J C
have this : HasColimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
Tactic: have := HasColimitsOfSize.has_colimits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : EssentiallySmall.{u₁, v₂, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J C
have this : HasColimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C
Tactic: have := HasColimitsOfShape.of_small.{v₁, u₁} C (SmallModel.{u₁} J)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.op (P.lift s.unop)
have dsimp : m = Quiver.Hom.op (P.lift s.unop)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.op (P.lift s.unop)
have rw : m = m.unop.op
Tactic: rw [← P.uniq s.unop m.unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ m = Quiver.Hom.op (P.lift s.unop)
have rw₁ : ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j
Tactic: rw [← P.uniq s.unop m.unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = s.unop.π.app j
have dsimp : ∀ (j : J), m.unop ≫ t.π.app j = Quiver.Hom.unop (s.ι.app (Opposite.op j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 (s.ι.app (Opposite.op j))
have rw : m.unop ≫ t.π.app j = Quiver.Hom.unop (t.op.ι.app (Opposite.op j) ≫ m)
Tactic: rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.op (P.desc s.unop)
have dsimp : m = Quiver.Hom.op (P.desc s.unop)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.op (P.desc s.unop)
have rw : m = m.unop.op
Tactic: rw [← P.uniq s.unop m.unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ m = Quiver.Hom.op (P.desc s.unop)
have rw₁ : ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j
Tactic: rw [← P.uniq s.unop m.unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = s.unop.ι.app j
have dsimp : ∀ (j : J), t.ι.app j ≫ m.unop = Quiver.Hom.unop (s.π.app (Opposite.op j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 (s.π.app (Opposite.op j))
have rw : t.ι.app j ≫ m.unop = Quiver.Hom.unop (m ≫ t.op.π.app (Opposite.op j))
Tactic: rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.unop (P.lift s.op)
have dsimp : m = Quiver.Hom.unop (P.lift s.op)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.unop (P.lift s.op)
have rw : m = m.op.unop
Tactic: rw [← P.uniq s.op m.op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ m = Quiver.Hom.unop (P.lift s.op)
have rw₁ : ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = s.op.π.app j
Tactic: rw [← P.uniq s.op m.op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = s.op.π.app j
have dsimp : ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = Quiver.Hom.op (s.ι.app (Opposite.unop j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 (s.ι.app (Opposite.unop j))
have rw : m.op ≫ t.π.app j = Quiver.Hom.op (t.unop.ι.app (Opposite.unop j) ≫ m)
Tactic: rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.unop (P.desc s.op)
have dsimp : m = Quiver.Hom.unop (P.desc s.op)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = Quiver.Hom.unop (P.desc s.op)
have rw : m = m.op.unop
Tactic: rw [← P.uniq s.op m.op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ m = Quiver.Hom.unop (P.desc s.op)
have rw₁ : ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = s.op.ι.app j
Tactic: rw [← P.uniq s.op m.op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 = s.op.ι.app j
have dsimp : ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = Quiver.Hom.op (s.π.app (Opposite.unop j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 (s.π.app (Opposite.unop j))
have rw : t.ι.app j ≫ m.op = Quiver.Hom.op (m ≫ t.unop.π.app (Opposite.unop j))
Tactic: rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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 (α := 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))
have 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))
Tactic: rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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
⊢ 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)))
have 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)))
Tactic: simp only [colimitHomIsoLimitYoneda, Iso.trans_hom, Iso.app_hom, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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
⊢ 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)))
have 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)))
Tactic: erw [limitObjIsoLimitCompEvaluation_hom_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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
⊢ 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)))
have 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)))
Tactic: change ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ _).app A = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, Functor.flip_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, Functor.flip_map_app]