-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma counitForward_naturality₂ (s t : (CostructuredArrow yoneda A)ᵒᵖ) (f : t ⟶ s) (x : F.obj t) :
    counitForward F s.unop (F.map f x) =
      OverArrows.map₂ (counitForward F t.unop x) f.unop.left (by simp)

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op.unop = (f ≫ eqToHom ⋯).unop

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ yoneda.map f.unop.left ≫ (unop t).hom = (unop s).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ F.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) (F.map f x)).val

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op.unop = (f ≫ eqToHom ⋯).unop

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ s = op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ (unop t).hom))

Tactic:
simp [← CostructuredArrow.eq_mk]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ F.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) (F.map f x)).val

Tactic:
have : (CostructuredArrow.mkPrecomp t.unop.hom f.unop.left).op =
    f ≫ eqToHom (by simp [← CostructuredArrow.eq_mk]) := by
  apply Quiver.Hom.unop_inj
  simp

Result:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ F.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) (F.map f x)).val

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ counitForward F (unop s) (F.map f x) = (counitForward F (unop t) x).map₂ f.unop.left ⋯

Tactic:
refine OverArrows.ext <| YonedaCollection.ext (by simp) ?_

Result:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ F.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) (F.map f x)).val

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ YonedaCollection.fst (counitForward F (unop s) (F.map f x)).val =
    YonedaCollection.fst ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val

Tactic:
simp

Result:
no goals