awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
inst_3 : ∀ (Z : C) (g : X ⟶ Z), Mono (Y := Limits.pushout g f) (pushout.inl g f)
this :
  ∀ (Z : Under.{v, u} X), Mono (Y := (pushout f ⋙ map f).obj Z) (NatTrans.app (Adjunction.unit (mapPushoutAdj f)) Z)
⊢ (pushout f).Faithful

Tactic:
(mapPushoutAdj f).faithful_L_of_mono_unit_app

Premises used: CategoryTheory.Adjunction.faithful_L_of_mono_unit_app, CategoryTheory.Under.mapPushoutAdj
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
⊢ (pushout f).IsLeftAdjoint

Tactic:
⟨_, ⟨mapPushoutAdj f⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Under.mapPushoutAdj
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPushouts.{v₂, u₂} D
Y : D
G : Functor.{v₂, v, u₂, u} D C
inst_3 : G.IsRightAdjoint
⊢ Functor.IsRightAdjoint (C := Under.{v, u} (G.obj Y)) (post G)

Tactic:
let ⟨F, ⟨a⟩⟩ := ‹G.IsRightAdjoint›; ⟨_, ⟨postAdjunctionRight a⟩⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.IsRightAdjoint, CategoryTheory.Under.pushout, Nonempty.intro, CategoryTheory.Adjunction.counit, CategoryTheory.Under.postAdjunctionRight, _private.0.CategoryTheory.Under.isRightAdjoint_post.match_1, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Under.post, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasBinaryCoproducts.{v, u} C
⊢ Functor.IsLeftAdjoint (costar X)

Tactic:
⟨_, ⟨costarAdjForget X⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Under.costarAdjForget
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasBinaryCoproducts.{v, u} C
⊢ Functor.IsRightAdjoint (forget X)

Tactic:
⟨_, ⟨costarAdjForget X⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Under.costarAdjForget
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : Functor.obj yoneda X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
rw :
  Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X) ≫ μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
        u :
      A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
rw₁ :
  Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((ε ≫ μ).app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
        u :
      A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
rw₂ :
  Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
        u :
      A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
rw₃ rw₄ :
  Eq.{v + 1} (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (G.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj (op X)))
            u :
          (fun (X : Type v) ↦ X) (G.obj (op X))) :
      (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))

Tactic:
rw [← comp_apply, ← NatTrans.comp_app, hε, h.app]

Premises used: CategoryTheory.comp_apply, CategoryTheory.OverPresheafAux.MakesOverArrow.app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X Y : C
f : X ⟶ Y
s : Functor.obj yoneda X ⟶ A
t : Functor.obj yoneda Y ⟶ A
hst : Functor.map yoneda f ≫ t = s
u : F.obj (op Y)
h : MakesOverArrow η t u
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
            u :
          (fun (X : Type v) ↦ X) (F.obj (op X))) :
      (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))

Tactic:
simp [h.app, yonedaEquiv_naturality, hst]

Premises used: CategoryTheory.OverPresheafAux.MakesOverArrow.app, CategoryTheory.yonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
f : Functor.obj yoneda X ⟶ F
hf : f ≫ η = s
⊢ MakesOverArrow η s ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (op X)) f)

Tactic:
⟨hf ▸ rfl⟩

Premises used: Eq.rec, CategoryTheory.OverPresheafAux.MakesOverArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
Y : C
η : Functor.obj yoneda Y ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
f : X ⟶ Y
hf : Functor.map yoneda f ≫ η = s
⊢ MakesOverArrow η s f

Tactic:
simpa only [yonedaEquiv_yoneda_map f] using of_arrow hf

Premises used: CategoryTheory.yonedaEquiv_yoneda_map, CategoryTheory.OverPresheafAux.MakesOverArrow.of_arrow
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ val (Subtype.mk (p := MakesOverArrow η s) u h) = u

Tactic:
rfl

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
u v : OverArrows η s
⊢ u.val = v.val → u = v

Tactic:
Subtype.ext

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, CategoryTheory.OverPresheafAux.OverArrows, Subtype.ext
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
p : OverArrows η s
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
        p.val :
      (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))

Tactic:
p.prop.app

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, CategoryTheory.OverPresheafAux.MakesOverArrow.app, Subtype.prop
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
Y : C
η : Functor.obj yoneda Y ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
p : OverArrows η s
rw :
  Eq (α := A.obj (op (unop (op X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (unop (op X)))) :
          (a : (fun (X : Type v) ↦ X) ((yoneda.obj Y).obj (op (unop (op X))))) →
            (fun (X : Type v) ↦ X) (A.obj (op (unop (op X)))))
        p.val :
      (fun (X : Type v) ↦ X) (A.obj (op (unop (op X)))))
    ((yonedaEquiv : (a : yoneda.obj (unop (op X)) ⟶ A) → A.obj (op (unop (op X)))) s : A.obj (op (unop (op X))))
⊢ Functor.map yoneda p.val ≫ η = s

Tactic:
rw [← yonedaEquiv.injective.eq_iff, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Premises used: Function.Injective.eq_iff, CategoryTheory.yonedaEquiv_yoneda_map, Equiv.injective, CategoryTheory.yonedaEquiv, CategoryTheory.yonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
Y : C
η : Functor.obj yoneda Y ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
p : OverArrows η s
⊢ Eq (α := A.obj (op (unop (op X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (unop (op X)))) :
          (a : (fun (X : Type v) ↦ X) ((yoneda.obj Y).obj (op (unop (op X))))) →
            (fun (X : Type v) ↦ X) (A.obj (op (unop (op X)))))
        p.val :
      (fun (X : Type v) ↦ X) (A.obj (op (unop (op X)))))
    ((yonedaEquiv : (a : yoneda.obj (unop (op X)) ⟶ A) → A.obj (op (unop (op X)))) s : A.obj (op (unop (op X))))

Tactic:
simp only [unop_op, p.app_val]

Premises used: CategoryTheory.OverPresheafAux.OverArrows.app_val, Opposite.unop_op
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
u : OverArrows η s
ε : F ⟶ G
hε : ε ≫ μ = η
⊢ (u.map₁ ε hε).val =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj (op X)))
      u.val

Tactic:
rfl

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X Y : C
f : X ⟶ Y
s : Functor.obj yoneda X ⟶ A
t : Functor.obj yoneda Y ⟶ A
hst : Functor.map yoneda f ≫ t = s
u : OverArrows η t
⊢ (u.map₂ f hst).val =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      u.val

Tactic:
rfl

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X Y : C
s : Functor.obj yoneda X ⟶ A
t : Functor.obj yoneda Y ⟶ A
f : X ⟶ Y
hf : Functor.map yoneda f ≫ t = s
u : OverArrows η t
⊢ (u.map₁ ε hε).map₂ f hf = (u.map₂ f hf).map₁ ε hε

Tactic:
OverArrows.ext <| (elementwise_of% (ε.naturality f.op).symm) u.val

Premises used: congrArg, Quiver.Hom.op, CategoryTheory.OverPresheafAux.OverArrows.val, Eq.mp, id, CategoryTheory.Functor.map, CategoryTheory.OverPresheafAux.OverArrows.ext, Mathlib.Tactic.Elementwise.hom_elementwise, CategoryTheory.comp_apply, Opposite.op, CategoryTheory.NatTrans.naturality, congr, Eq.symm, Eq, CategoryTheory.NatTrans.app, forall_congr
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
Y : C
η : Functor.obj yoneda Y ⟶ A
X : C
s : Functor.obj yoneda X ⟶ A
f : X ⟶ Y
hf : Functor.map yoneda f ≫ η = s
⊢ (yonedaArrow f hf).val = f

Tactic:
rfl

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
s t : CostructuredArrow yoneda A
p : OverArrows s.hom t.hom
⊢ Functor.map yoneda p.val ≫ s.hom = t.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A_1 A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
s : CostructuredArrow yoneda A
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      (Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s).obj X ⟶
        Functor.obj (Functor.obj yoneda s) Y)
      ((Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s).map f ≫
        Iso.hom
          ((fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (OverArrows.costructuredArrowIso s (unop x) : OverArrows s.hom (unop x).hom ≅ unop x ⟶ s))
            Y))
      (Iso.hom
          ((fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (OverArrows.costructuredArrowIso s (unop x) : OverArrows s.hom (unop x).hom ≅ unop x ⟶ s))
            X) ≫
        Functor.map (Functor.obj yoneda s) f)
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      (Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s).obj X ⟶
        Functor.obj (Functor.obj yoneda s) Y)
      ((Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s).map f ≫
        Iso.hom
          ((fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (OverArrows.costructuredArrowIso s (unop x) : OverArrows s.hom (unop x).hom ≅ unop x ⟶ s))
            Y))
      (Iso.hom
          ((fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (OverArrows.costructuredArrowIso s (unop x) : OverArrows s.hom (unop x).hom ≅ unop x ⟶ s))
            X) ≫
        Functor.map (Functor.obj yoneda s) f)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A_1 A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : CostructuredArrow yoneda A} (f : X ⟶ Y),
    Eq (α := Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) X ⟶ Functor.obj yoneda Y)
      (Functor.map (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) f ≫
        Iso.hom
          ((fun (s : CostructuredArrow yoneda A) ↦
              (NatIso.ofComponents
                  (fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦ OverArrows.costructuredArrowIso s (unop x)) ⋯ :
                Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s ≅ Functor.obj yoneda s))
            Y))
      (Iso.hom
          ((fun (s : CostructuredArrow yoneda A) ↦
              (NatIso.ofComponents
                  (fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦ OverArrows.costructuredArrowIso s (unop x)) ⋯ :
                Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s ≅ Functor.obj yoneda s))
            X) ≫
        Functor.map yoneda f)
⊢ ∀ {X Y : CostructuredArrow yoneda A} (f : X ⟶ Y),
    Eq (α := Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) X ⟶ Functor.obj yoneda Y)
      (Functor.map (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) f ≫
        Iso.hom
          ((fun (s : CostructuredArrow yoneda A) ↦
              (NatIso.ofComponents
                  (fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦ OverArrows.costructuredArrowIso s (unop x)) ⋯ :
                Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s ≅ Functor.obj yoneda s))
            Y))
      (Iso.hom
          ((fun (s : CostructuredArrow yoneda A) ↦
              (NatIso.ofComponents
                  (fun (x : (CostructuredArrow yoneda A)ᵒᵖ) ↦ OverArrows.costructuredArrowIso s (unop x)) ⋯ :
                Functor.obj (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A) s ≅ Functor.obj yoneda s))
            X) ≫
        Functor.map yoneda f)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : Functor.obj yoneda Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
rw rw₁ : op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g')
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : Functor.obj yoneda Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
rw rw₁ : op (CostructuredArrow.mk (Functor.map yoneda f ≫ g')) = op (CostructuredArrow.mk (Functor.map yoneda f ≫ g'))
⊢ op (CostructuredArrow.mk (Functor.map yoneda f ≫ g')) = op (CostructuredArrow.mk (Functor.map yoneda f ≫ g))

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : Functor.obj yoneda X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
rw rw₁ : op (CostructuredArrow.mk s) = op (CostructuredArrow.mk s)
⊢ op (CostructuredArrow.mk s) =
    op
      (CostructuredArrow.mk (Y := X)
        ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A)
          ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s)))

Tactic:
rw [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : YonedaCollection F X
⊢ p.yonedaEquivFst = (yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) p.fst

Tactic:
rfl

Premises used: rfl, CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : Functor.obj yoneda X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ (mk s x).fst = s

Tactic:
Equiv.apply_symm_apply _ _

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.fst, Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : Functor.obj yoneda X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
rw rw₁ : op (CostructuredArrow.mk s) = op (CostructuredArrow.mk s)
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (mk s x).fst)

Tactic:
rw [YonedaCollection.mk_fst]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.mk_fst
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : Functor.obj yoneda X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ (mk s x).snd =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk s)))) →
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (mk s x).fst))))
      x

Tactic:
rfl

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.fst, CategoryTheory.OverPresheafAux.YonedaCollection.snd, rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
rw rw₁ : op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk q.fst)
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk p.fst)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
h' :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk q.fst)))) →
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk p.fst))))
      q.snd =
    p.snd
rcases :
  ∀ (p : A.obj (op X))
    (p' :
      F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) p))))
    (h :
      fst (F := F)
          (Sigma.mk (β := fun (s : A.obj (op X)) ↦
            F.obj
              (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
            p p') =
        q.fst)
    (h' :
      Eq (α :=
        (fun (X : Type v) ↦ X)
          (F.obj
            (op
              (CostructuredArrow.mk
                (fst (F := F)
                  (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                    F.obj
                      (op
                        (CostructuredArrow.mk (Y := X)
                          ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                    p p'))))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk q.fst)))) →
                (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, p'⟩)))))
            q.snd :
          (fun (X : Type v) ↦ X)
            (F.obj
              (op
                (CostructuredArrow.mk
                  (fst (F := F)
                    (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                      F.obj
                        (op
                          (CostructuredArrow.mk (Y := X)
                            ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                      p p'))))))
        (snd
            (Sigma.mk (β := fun (s : A.obj (op X)) ↦
              F.obj
                (op
                  (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
              p p') :
          F.obj
            (op
              (CostructuredArrow.mk
                (fst (F := F)
                  (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                    F.obj
                      (op
                        (CostructuredArrow.mk (Y := X)
                          ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                    p p')))))),
    Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        p p' =
      q
⊢ p = q

Tactic:
rcases p with ⟨p, p'⟩