awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
p q : F.Elements
f : p ⟶ q
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((↑f : p.fst ⟶ q.fst) ≫ Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (p.snd (β := fun (c : G) ↦ F.obj c)) =
    p.snd (β := fun (c : G) ↦ F.obj c)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑f : p.fst ⟶ q.fst) ≫ F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (p.snd (β := fun (c : G) ↦ F.obj c)) =
    p.snd (β := fun (c : G) ↦ F.obj c)

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((↑f : p.fst ⟶ q.fst) ≫ Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (p.snd (β := fun (c : G) ↦ F.obj c)) =
    p.snd (β := fun (c : G) ↦ F.obj c)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
X Y : F.Elements
x : X ⟶ Y
w :
  (↑(Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
                (Y.snd (β := fun (c : G) ↦ F.obj c)) =
              X.snd (β := fun (c : G) ↦ F.obj c))
            (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯ ≫
          x) :
      Y.fst ⟶ Y.fst) =
    (↑(𝟙 Y) : Y.fst ⟶ Y.fst)
⊢ Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
            (Y.snd (β := fun (c : G) ↦ F.obj c)) =
          X.snd (β := fun (c : G) ↦ F.obj c))
        (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯ ≫
      x =
    𝟙 Y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
X Y : F.Elements
x : X ⟶ Y
⊢ (↑(Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
                (Y.snd (β := fun (c : G) ↦ F.obj c)) =
              X.snd (β := fun (c : G) ↦ F.obj c))
            (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯ ≫
          x) :
      Y.fst ⟶ Y.fst) =
    (↑(𝟙 Y) : Y.fst ⟶ Y.fst)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
X Y : F.Elements
x : X ⟶ Y
w :
  (↑(x ≫
          Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
                (Y.snd (β := fun (c : G) ↦ F.obj c)) =
              X.snd (β := fun (c : G) ↦ F.obj c))
            (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯) :
      X.fst ⟶ X.fst) =
    (↑(𝟙 X) : X.fst ⟶ X.fst)
⊢ x ≫
      Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
            (Y.snd (β := fun (c : G) ↦ F.obj c)) =
          X.snd (β := fun (c : G) ↦ F.obj c))
        (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯ =
    𝟙 X

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
X Y : F.Elements
x : X ⟶ Y
⊢ (↑(x ≫
          Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
                (Y.snd (β := fun (c : G) ↦ F.obj c)) =
              X.snd (β := fun (c : G) ↦ F.obj c))
            (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯) :
      X.fst ⟶ X.fst) =
    (↑(𝟙 X) : X.fst ⟶ X.fst)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : F.Elements
f : A ⟶ B
h : IsIso ((π F).map f)
⊢ IsIso f

Tactic:
⟨⟨(inv ((π F).map f) :), ?_⟩, ?_, ?_⟩

Premises used: CategoryTheory.CategoryOfElements.π, CategoryTheory.Functor.map, Subtype.mk, And.intro, Exists.intro, CategoryTheory.inv, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : F.Elements
f : A ⟶ B
h : IsIso ((π F).map f)
refine_1 :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (inv ((π F).map f))) :
        (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
      (B.snd (β := fun (c : C) ↦ F.obj c)) =
    A.snd (β := fun (c : C) ↦ F.obj c)
refine_2 :
  f ≫
      Subtype.mk (p := fun (f : B.fst (β := fun (c : C) ↦ F.obj c) ⟶ A.fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
            (B.snd (β := fun (c : C) ↦ F.obj c)) =
          A.snd (β := fun (c : C) ↦ F.obj c))
        (inv ((π F).map f)) ⋯ =
    𝟙 A
refine_3 :
  Subtype.mk (p := fun (f : B.fst (β := fun (c : C) ↦ F.obj c) ⟶ A.fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
            (B.snd (β := fun (c : C) ↦ F.obj c)) =
          A.snd (β := fun (c : C) ↦ F.obj c))
        (inv ((π F).map f)) ⋯ ≫
      f =
    𝟙 B
⊢ IsIso f

Tactic:
refine ⟨⟨(inv ((π F).map f) :), ?_⟩, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : F.Elements
f : A ⟶ B
h : IsIso ((π F).map f)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (inv ((π F).map f))) :
        (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
      (B.snd (β := fun (c : C) ↦ F.obj c)) =
    A.snd (β := fun (c : C) ↦ F.obj c)

Tactic:
simp only [← map_snd f, ← Functor.map_comp_apply,
        π_obj, π_map, IsIso.hom_inv_id, Functor.map_id_apply]

Premises used: CategoryTheory.CategoryOfElements.map_snd, CategoryTheory.Functor.map_comp_apply, CategoryTheory.CategoryOfElements.π_map, CategoryTheory.Functor.map_id_apply, CategoryTheory.CategoryOfElements.π_obj, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
α : F₁ ⟶ F₂
t₁ t₂ : F₁.Elements
k : t₁ ⟶ t₂
⊢ Eq (α :=
    (fun (X : Type w) ↦ X)
      (F₂.obj
        (Sigma.fst (β := fun (c : C) ↦ F₂.obj c)
          (Sigma.mk (β := fun (c : C) ↦ F₂.obj c) (t₂.fst (β := fun (c : C) ↦ F₁.obj c))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (t₂.fst (β := fun (c : C) ↦ F₁.obj c))) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj t₂.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₂.fst))
              (t₂.snd (β := fun (c : C) ↦ F₁.obj c)))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map (↑k : t₁.fst ⟶ t₂.fst)) :
          (a :
              (fun (X : Type w) ↦ X)
                (F₂.obj
                  ⟨t₁.fst,
                      (ConcreteCategory.hom (α.app t₁.fst) :
                          (a : (fun (X : Type w) ↦ X) (F₁.obj t₁.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₁.fst))
                        t₁.snd⟩.fst)) →
            (fun (X : Type w) ↦ X)
              (F₂.obj
                ⟨t₂.fst,
                    (ConcreteCategory.hom (α.app t₂.fst) :
                        (a : (fun (X : Type w) ↦ X) (F₁.obj t₂.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₂.fst))
                      t₂.snd⟩.fst))
        (Sigma.snd (β := fun (c : C) ↦ F₂.obj c)
          (Sigma.mk (β := fun (c : C) ↦ F₂.obj c) (t₁.fst (β := fun (c : C) ↦ F₁.obj c))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (t₁.fst (β := fun (c : C) ↦ F₁.obj c))) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj t₁.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₁.fst))
              (t₁.snd (β := fun (c : C) ↦ F₁.obj c))))) :
      (fun (X : Type w) ↦ X)
        (F₂.obj
          (Sigma.fst (β := fun (c : C) ↦ F₂.obj c)
            (Sigma.mk (β := fun (c : C) ↦ F₂.obj c) (t₂.fst (β := fun (c : C) ↦ F₁.obj c))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (t₂.fst (β := fun (c : C) ↦ F₁.obj c))) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj t₂.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₂.fst))
                (t₂.snd (β := fun (c : C) ↦ F₁.obj c)))))))
    (Sigma.snd (β := fun (c : C) ↦ F₂.obj c)
        (Sigma.mk (β := fun (c : C) ↦ F₂.obj c) (t₂.fst (β := fun (c : C) ↦ F₁.obj c))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (t₂.fst (β := fun (c : C) ↦ F₁.obj c))) :
              (a : (fun (X : Type w) ↦ X) (F₁.obj t₂.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₂.fst))
            (t₂.snd (β := fun (c : C) ↦ F₁.obj c)))) :
      F₂.obj
        (Sigma.fst (β := fun (c : C) ↦ F₂.obj c)
          (Sigma.mk (β := fun (c : C) ↦ F₂.obj c) (t₂.fst (β := fun (c : C) ↦ F₁.obj c))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (t₂.fst (β := fun (c : C) ↦ F₁.obj c))) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj t₂.fst)) → (fun (X : Type w) ↦ X) (F₂.obj t₂.fst))
              (t₂.snd (β := fun (c : C) ↦ F₁.obj c))))))

Tactic:
simpa [map_snd] using (NatTrans.naturality_apply α k.1 t₁.2).symm

Premises used: CategoryTheory.CategoryOfElements.map_snd, CategoryTheory.NatTrans.naturality_apply, Eq.symm, Subtype.val
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
α : F₁ ⟶ F₂
⊢ map α ⋙ π F₂ = π F₁

Tactic:
rfl

Premises used: CategoryTheory.Functor.Elements, CategoryTheory.Functor.comp, CategoryTheory.CategoryOfElements.π, rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : F.Elements
f : X ⟶ Y
h :
  ∀ (x : PUnit.{w + 1}),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (StructuredArrow.hom
                (StructuredArrow.mk (Y := X.fst (β := fun (c : C) ↦ F.obj c))
                  (↾fun (x : PUnit.{w + 1}) ↦ X.snd (β := fun (c : C) ↦ F.obj c))) ≫
              F.map (↑f : X.fst ⟶ Y.fst))).toFun
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (StructuredArrow.hom
            (StructuredArrow.mk (Y := Y.fst (β := fun (c : C) ↦ F.obj c))
              (↾fun (x : PUnit.{w + 1}) ↦ Y.snd (β := fun (c : C) ↦ F.obj c)))))
        x
⊢ StructuredArrow.hom
        (StructuredArrow.mk (Y := X.fst (β := fun (c : C) ↦ F.obj c))
          (↾fun (x : PUnit.{w + 1}) ↦ X.snd (β := fun (c : C) ↦ F.obj c))) ≫
      F.map (↑f : X.fst ⟶ Y.fst) =
    StructuredArrow.hom
      (StructuredArrow.mk (Y := Y.fst (β := fun (c : C) ↦ F.obj c))
        (↾fun (x : PUnit.{w + 1}) ↦ Y.snd (β := fun (c : C) ↦ F.obj c)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : F.Elements
f : X ⟶ Y
x : PUnit.{w + 1}
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (StructuredArrow.hom
              (StructuredArrow.mk (Y := X.fst (β := fun (c : C) ↦ F.obj c))
                (↾fun (x : PUnit.{w + 1}) ↦ X.snd (β := fun (c : C) ↦ F.obj c))) ≫
            F.map (↑f : X.fst ⟶ Y.fst))).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := Y.fst (β := fun (c : C) ↦ F.obj c))
            (↾fun (x : PUnit.{w + 1}) ↦ Y.snd (β := fun (c : C) ↦ F.obj c)))))
      x

Tactic:
simp [f.2]

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : F.Elements
⊢ (toStructuredArrow F).obj X =
    { left := { as := PUnit.unit }, right := X.fst (β := fun (c : C) ↦ F.obj c),
      hom :=
        ↾fun (x : Functor.obj (Functor.fromPUnit PUnit.{w + 1}) { as := PUnit.unit : Discrete PUnit.{1} }) ↦
          X.snd (β := fun (c : C) ↦ F.obj c) }

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : F.Elements
f : X ⟶ Y
⊢ StructuredArrow.Hom.right ((toStructuredArrow F).map f) = (↑f : X.fst ⟶ Y.fst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
simp :
  Eq (α := F.obj Y.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
          (a : F.obj X.right) → F.obj Y.right)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom : (a : PUnit.{w + 1}) → F.obj X.right) PUnit.unit :
          F.obj X.right) :
      F.obj Y.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.hom ≫ F.map (StructuredArrow.Hom.right f)) :
          (a : PUnit.{w + 1}) → F.obj Y.right)
        PUnit.unit :
      F.obj Y.right)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
        (a :
            (fun (X : Type w) ↦ X)
              (F.obj
                (F.elementsMk X.right
                    ((ConcreteCategory.hom X.hom :
                        (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj X.right))
                      PUnit.unit)).fst)) →
          (fun (X : Type w) ↦ X)
            (F.obj
              (F.elementsMk Y.right
                  ((ConcreteCategory.hom Y.hom :
                      (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj Y.right))
                    PUnit.unit)).fst))
      ((F.elementsMk X.right
            ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom :
                (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj X.right))
              PUnit.unit)).snd
        (β := fun (c : C) ↦ F.obj c)) =
    (F.elementsMk Y.right
          ((ConcreteCategory.hom (FC := TypeCat.Fun) Y.hom :
              (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj Y.right))
            PUnit.unit)).snd
      (β := fun (c : C) ↦ F.obj c)

Tactic:
simp [ConcreteCategory.congr_hom f.w.symm .unit]

Premises used: CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ Eq (α := F.obj Y.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
          (a : F.obj X.right) → F.obj Y.right)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom : (a : PUnit.{w + 1}) → F.obj X.right) PUnit.unit :
          F.obj X.right) :
      F.obj Y.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.hom ≫ F.map (StructuredArrow.Hom.right f)) :
          (a : PUnit.{w + 1}) → F.obj Y.right)
        PUnit.unit :
      F.obj Y.right)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : StructuredArrow PUnit.{w + 1} F
⊢ (fromStructuredArrow F).obj X =
    Sigma.mk (β := fun (c : C) ↦ F.obj c) X.right
      ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom :
          (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj X.right))
        PUnit.unit)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
simp :
  Eq (α := F.obj Y.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
          (a : F.obj X.right) → F.obj Y.right)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom : (a : PUnit.{w + 1}) → F.obj X.right) PUnit.unit :
          F.obj X.right) :
      F.obj Y.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.hom ≫ F.map (StructuredArrow.Hom.right f)) :
          (a : PUnit.{w + 1}) → F.obj Y.right)
        PUnit.unit :
      F.obj Y.right)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ((fromStructuredArrow F).obj X).fst)) →
          (fun (X : Type w) ↦ X) (F.obj ((fromStructuredArrow F).obj Y).fst))
      (((fromStructuredArrow F).obj X).snd (β := fun (c : C) ↦ F.obj c)) =
    ((fromStructuredArrow F).obj Y).snd (β := fun (c : C) ↦ F.obj c)

Tactic:
simp [ConcreteCategory.congr_hom f.w.symm PUnit.unit]

Premises used: CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (fromStructuredArrow F).map f =
    Subtype.mk (p :=
      fun
        (f :
          ((fromStructuredArrow F).obj X).fst (β := fun (c : C) ↦ F.obj c) ⟶
            ((fromStructuredArrow F).obj Y).fst (β := fun (c : C) ↦ F.obj c)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w) ↦ X) (F.obj ((fromStructuredArrow F).obj X).fst)) →
              (fun (X : Type w) ↦ X) (F.obj ((fromStructuredArrow F).obj Y).fst))
          (((fromStructuredArrow F).obj X).snd (β := fun (c : C) ↦ F.obj c)) =
        ((fromStructuredArrow F).obj Y).snd (β := fun (c : C) ↦ F.obj c))
      (StructuredArrow.Hom.right f) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
w :
  ∀ (Z : Cᵒᵖ)
    (y :
      Functor.obj
        (Functor.obj yoneda
          (CostructuredArrow.left (S := (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)))
            (CostructuredArrow.mk (Y := unop (unop X).1)
                ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                  ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
              CostructuredArrow yoneda F)))
        Z),
    Eq (α := F.obj Z)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Functor.map yoneda (↑f.unop : (unop Y).fst ⟶ (unop X).fst).unop ≫
              CostructuredArrow.hom
                (CostructuredArrow.mk (Y := unop (unop Y).1)
                  ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop Y).1))) → yoneda.obj (unop (unop Y).1) ⟶ F)
                    ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
            Z))
        y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (CostructuredArrow.hom
              (CostructuredArrow.mk (Y := unop (unop X).1)
                ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                  ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
            Z))
        y)
⊢ Eq (α :=
    Functor.obj yoneda
        (CostructuredArrow.left (S := (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)))
          (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
            CostructuredArrow yoneda F)) ⟶
      F)
    (Functor.map yoneda (↑f.unop : (unop Y).fst ⟶ (unop X).fst).unop ≫
      CostructuredArrow.hom
        (CostructuredArrow.mk (Y := unop (unop Y).1)
          ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop Y).1))) → yoneda.obj (unop (unop Y).1) ⟶ F)
            ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))

Tactic:
ext Z y
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
Z : Cᵒᵖ
y :
  Functor.obj
    (Functor.obj yoneda
      (CostructuredArrow.left (S := (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)))
        (CostructuredArrow.mk (Y := unop (unop X).1)
            ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
              ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
          CostructuredArrow yoneda F)))
    Z
⊢ Eq (α := F.obj Z)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map yoneda (↑f.unop : (unop Y).fst ⟶ (unop X).fst).unop ≫
            CostructuredArrow.hom
              (CostructuredArrow.mk (Y := unop (unop Y).1)
                ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop Y).1))) → yoneda.obj (unop (unop Y).1) ⟶ F)
                  ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
          Z))
      y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CostructuredArrow.hom
            (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
          Z))
      y)

Tactic:
simp [yonedaEquiv]

Premises used: CategoryTheory.yonedaEquiv
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.unop.left.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩.fst)) →
          (fun (X : Type v) ↦ X) (F.obj ⟨op (unop Y).left, yonedaEquiv.toFun (unop Y).hom⟩.fst))
      ((Sigma.mk (β := fun (c : Cᵒᵖ) ↦ F.obj c) (op (unop X).left) (Equiv.toFun yonedaEquiv (unop X).hom)).snd (β :=
        fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (Sigma.mk (β := fun (c : Cᵒᵖ) ↦ F.obj c) (op (unop Y).left) (Equiv.toFun yonedaEquiv (unop Y).hom)).snd (β :=
      fun (c : Cᵒᵖ) ↦ F.obj c)

Tactic:
simp [yonedaEquiv_naturality]

Premises used: CategoryTheory.yonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : C
f : Functor.obj yoneda X ⟶ F
⊢ (fromCostructuredArrow F).obj (op (CostructuredArrow.mk f)) =
    Sigma.mk (β := fun (c : Cᵒᵖ) ↦ F.obj c) (op X) (Equiv.toFun yonedaEquiv f)

Tactic:
rfl

Premises used: rfl