-- Mathlib/CategoryTheory/Elements.lean
theorem costructuredArrow_yoneda_equivalence_naturality {F₁ F₂ : Cᵒᵖ ⥤ Type v} (α : F₁ ⟶ F₂) :
    (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
simp

Result:
no goals

Proof state:
case h_obj.e_f.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj (unop ((map α).obj (unop X)).1)).obj x✝
⊢ (yonedaEquiv.symm ((map α).obj (unop X)).snd).app x✝ f = (yonedaEquiv.symm (unop X).snd ≫ α).app x✝ f

Tactic:
simpa using congr_fun (α.naturality f.op).symm (unop X).snd

Result:
no goals

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : F₁.Elementsᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

Tactic:
intro X

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ CostructuredArrow.mk (yonedaEquiv.symm ((map α).obj (unop X)).snd) =
    CostructuredArrow.mk (yonedaEquiv.symm (unop X).snd ≫ α)

Tactic:
congr

Result:
case h_obj.e_f
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ yonedaEquiv.symm ((map α).obj (unop X)).snd = yonedaEquiv.symm (unop X).snd ≫ α

Proof state:
case h_obj.e_f
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ yonedaEquiv.symm ((map α).obj (unop X)).snd = yonedaEquiv.symm (unop X).snd ≫ α

Tactic:
ext _ f

Result:
case h_obj.e_f.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj (unop ((map α).obj (unop X)).1)).obj x✝
⊢ (yonedaEquiv.symm ((map α).obj (unop X)).snd).app x✝ f = (yonedaEquiv.symm (unop X).snd ≫ α).app x✝ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α

Tactic:
fapply Functor.ext

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : F₁.Elementsᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    _auto✝

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

Tactic:
simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
  Functor.comp_obj]

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ CostructuredArrow.mk (yonedaEquiv.symm ((map α).obj (unop X)).snd) =
    CostructuredArrow.mk (yonedaEquiv.symm (unop X).snd ≫ α)