awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := 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))
have 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))
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda_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
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))
⊢ 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))
have 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))
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda_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
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))
⊢ 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))
have 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))
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda_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
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))
⊢ 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))
have 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))
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda_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
⊢ Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
have rw : Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
  (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
      (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) :
    limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
  (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj 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.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
⊢ Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
have rw₁ : Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
  (CategoryStruct.comp (Y := limit (F.rightOp ⋙ coyoneda))
      (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
          (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) :
        limit (F.rightOp ⋙ coyoneda) ⟶ limit (F.rightOp ⋙ coyoneda))
      (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i) :
    limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
  (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj 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.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
rw₁ :
  Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := limit (F.rightOp ⋙ coyoneda))
        (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F)))
            (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F)) (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) :
          limit (F.rightOp ⋙ coyoneda) ⟶ limit (F.rightOp ⋙ coyoneda))
        (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
⊢ Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
have rw₂ : 𝟙 (limit (F.rightOp ⋙ coyoneda)) ≫ limit.π (F.rightOp ⋙ coyoneda) i = limit.π (F.rightOp ⋙ coyoneda) 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.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
rw₁ :
  Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := limit (F.rightOp ⋙ coyoneda))
        (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F)))
            (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F)) (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) :
          limit (F.rightOp ⋙ coyoneda) ⟶ limit (F.rightOp ⋙ coyoneda))
        (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
rw₂ : 𝟙 (limit (F.rightOp ⋙ coyoneda)) ≫ limit.π (F.rightOp ⋙ coyoneda) i = limit.π (F.rightOp ⋙ coyoneda) i
⊢ Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
have rw₃ : Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i)))) (limit.π (F.rightOp ⋙ coyoneda) i)
  (limit.π (F.rightOp ⋙ coyoneda) 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.rightOp ⋙ Functor.obj yoneda A).obj i)
    (Iso.hom (colimitHomIsoLimitYoneda' F A) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
have simp : Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
  (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
    CategoryStruct.comp (Y := limit (F.rightOp ⋙ Functor.obj yoneda A))
      (Iso.hom (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A) :
        (limit (F.rightOp ⋙ coyoneda)).obj A ⟶ limit (F.rightOp ⋙ Functor.obj yoneda A))
      (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
        limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i))
  (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op 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.rightOp ⋙ Functor.obj yoneda A).obj i)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
      CategoryStruct.comp (Y := limit (F.rightOp ⋙ Functor.obj yoneda A))
        (Iso.hom (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A) :
          (limit (F.rightOp ⋙ coyoneda)).obj A ⟶ limit (F.rightOp ⋙ Functor.obj yoneda A))
        (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
          limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
have erw : Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
  (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫ NatTrans.app (limit.π (F.rightOp ⋙ coyoneda) i) A)
  (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op 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.rightOp ⋙ Functor.obj yoneda A).obj i)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
      NatTrans.app (limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
have change : Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
  (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) A)
  (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op 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.rightOp ⋙ coyoneda).obj i).obj A)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
have rw : Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
  (NatTrans.app (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) A)
  (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op 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.rightOp ⋙ coyoneda).obj i).obj A)
    (NatTrans.app (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
⊢ Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
have rw₁ : Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
  (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))) :
    Functor.obj (Functor.obj yoneda A) (op (colimit F)) ⟶ Functor.obj (Functor.obj yoneda A) (op (F.obj (op i))))
  (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op 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
⊢ Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
        (↾fun (g : colimit F ⟶ A) ↦ colimit.ι F (op i) ≫ g) :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
have rw : Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
  (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
      (Iso.hom (colimitHomIsoLimitYoneda' F A) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i) :
    limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
  (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
    limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda'_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
rw :
  Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
        (Iso.hom (colimitHomIsoLimitYoneda' F A) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i) :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
⊢ Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
        (↾fun (g : colimit F ⟶ A) ↦ colimit.ι F (op i) ≫ g) :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
have rw₁ : Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
  (CategoryStruct.comp (Y := limit (F.rightOp ⋙ Functor.obj yoneda A))
      (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
          (Iso.hom (colimitHomIsoLimitYoneda' F A)) :
        limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ limit (F.rightOp ⋙ Functor.obj yoneda A))
      (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
        limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i) :
    limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
  (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
    limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]