awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : Dᵒᵖ
⊢ Cat.Hom.toFunctor (Functor.toCatHom (map (Quiver.Hom.unop (𝟙 d)))) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T)))

Tactic:
exact Functor.ext (fun ⟨_, _, _⟩ => by simp)

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq (α :=
    (↑(Cat.of (StructuredArrow (Opposite.unop X) T)) : Type (max u₁ v₂)) ⥤
      (↑(Cat.of (StructuredArrow (Opposite.unop Z) T)) : Type (max u₁ v₂)))
    (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g).unop)))
    (Cat.Hom.toFunctor (Functor.toCatHom (map f.unop) ≫ Functor.toCatHom (map g.unop)))
⊢ Eq (α := Cat.of (StructuredArrow (Opposite.unop X) T) ⟶ Cat.of (StructuredArrow (Opposite.unop Z) T))
    (Functor.toCatHom (map (f ≫ g).unop)) (Functor.toCatHom (map f.unop) ≫ Functor.toCatHom (map g.unop))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x : (↑(Cat.of (StructuredArrow (Opposite.unop X) T)) : Type (max u₁ v₂))
⊢ Functor.obj (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g).unop))) x =
    Functor.obj (Cat.Hom.toFunctor (Functor.toCatHom (map f.unop) ≫ Functor.toCatHom (map g.unop))) x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (↑(Cat.of (StructuredArrow (Opposite.unop X) T)) : Type (max u₁ v₂)) ⥤
      (↑(Cat.of (StructuredArrow (Opposite.unop Z) T)) : Type (max u₁ v₂)))
    (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g).unop)))
    (Cat.Hom.toFunctor (Functor.toCatHom (map f.unop) ≫ Functor.toCatHom (map g.unop)))

Tactic:
exact Functor.ext (fun _ => by simp)

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : D
h : Cat.Hom.toFunctor (Functor.toCatHom (map (𝟙 d))) = Cat.Hom.toFunctor (𝟙 (Cat.of (CostructuredArrow T d)))
⊢ Functor.toCatHom (map (𝟙 d)) = 𝟙 (Cat.of (CostructuredArrow T d))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : D
x : (↑(Cat.of (CostructuredArrow T d)) : Type (max u₁ v₂))
left : C
right : Discrete PUnit.{1}
hom : T.obj left ⟶ Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit d) right
⊢ Functor.obj (Cat.Hom.toFunctor (Functor.toCatHom (map (𝟙 d))))
      { left := left, right := right, hom := hom : Comma T (Functor.fromPUnit d) } =
    (Cat.Hom.toFunctor (𝟙 (Cat.of (CostructuredArrow T d)))).obj { left := left, right := right, hom := hom }

Tactic:
simp [CostructuredArrow.map, Comma.mapRight]

Premises used: CategoryTheory.Comma.mapRight, CategoryTheory.CostructuredArrow.map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : D
⊢ Cat.Hom.toFunctor (Functor.toCatHom (map (𝟙 d))) = Cat.Hom.toFunctor (𝟙 (Cat.of (CostructuredArrow T d)))

Tactic:
exact Functor.ext (fun ⟨_, _, _⟩ => by simp [CostructuredArrow.map, Comma.mapRight])

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq (α :=
    (↑(Cat.of (CostructuredArrow T X)) : Type (max u₁ v₂)) ⥤ (↑(Cat.of (CostructuredArrow T Z)) : Type (max u₁ v₂)))
    (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g))))
    (Cat.Hom.toFunctor (Functor.toCatHom (map f) ≫ Functor.toCatHom (map g)))
⊢ Eq (α := Cat.of (CostructuredArrow T X) ⟶ Cat.of (CostructuredArrow T Z)) (Functor.toCatHom (map (f ≫ g)))
    (Functor.toCatHom (map f) ≫ Functor.toCatHom (map g))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
x : (↑(Cat.of (CostructuredArrow T X)) : Type (max u₁ v₂))
⊢ Functor.obj (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g)))) x =
    Functor.obj (Cat.Hom.toFunctor (Functor.toCatHom (map f) ≫ Functor.toCatHom (map g))) x

Tactic:
simp [CostructuredArrow.map, Comma.mapRight]

Premises used: CategoryTheory.Comma.mapRight, CategoryTheory.CostructuredArrow.map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (↑(Cat.of (CostructuredArrow T X)) : Type (max u₁ v₂)) ⥤ (↑(Cat.of (CostructuredArrow T Z)) : Type (max u₁ v₂)))
    (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g))))
    (Cat.Hom.toFunctor (Functor.toCatHom (map f) ≫ Functor.toCatHom (map g)))

Tactic:
exact Functor.ext (fun _ => by simp [CostructuredArrow.map, Comma.mapRight])

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₃, v₂, u₃, u₂} E D
X Y : Grothendieck (R ⋙ functor L)
f : X ⟶ Y
⊢ L.map f.fiber.left ≫ { left := left Y.fiber, right := Y.base, hom := hom Y.fiber : Comma L R }.hom =
    { left := left X.fiber, right := X.base, hom := hom X.fiber : Comma L R }.hom ≫ R.map f.base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₃, v₂, u₃, u₂} E D
X : E
X_1 Y : (↑((R ⋙ functor L).obj X) : Type (max v₂ u₁))
x : X_1 ⟶ Y
⊢ Eq (α :=
    (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_1 ⟶
      Functor.obj (proj L (R.obj X)) Y)
    ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).map x ≫
      Iso.hom
        ((fun (X_2 : (↑((R ⋙ functor L).obj X) : Type (max v₂ u₁))) ↦
            (Iso.refl
                ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_2) :
              (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_2 ≅
                (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_2))
          Y))
    (Iso.hom
        ((fun (X_2 : (↑((R ⋙ functor L).obj X) : Type (max v₂ u₁))) ↦
            (Iso.refl
                ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_2) :
              (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_2 ≅
                (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X_2))
          X_1) ≫
      Functor.map (proj L (R.obj X)) x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₃, v₂, u₃, u₂} E D
X : Comma L R
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom (V :=
      (↑((R ⋙ functor L).obj
            (Grothendieck.base (F := R ⋙ functor L)
              { base := X.right, fiber := mk X.hom : Grothendieck (R ⋙ functor L) })) :
        Type (max u₁ v₂)))
      (Functor.obj
        (Cat.Hom.toFunctor
          ((R ⋙ functor L).map
            (Grothendieck.Hom.base (𝟙 { base := X.right, fiber := mk X.hom : Grothendieck (R ⋙ functor L) }))))
        (Grothendieck.fiber { base := X.right, fiber := mk X.hom }))
      (Grothendieck.fiber { base := X.right, fiber := mk X.hom }))
    (eqToHom ⋯ ≫
      Grothendieck.Hom.fiber { base := CommaMorphism.right (𝟙 X), fiber := homMk (CommaMorphism.left (𝟙 X)) ⋯ })
    (Grothendieck.Hom.fiber (𝟙 { base := X.right, fiber := mk X.hom }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₃, v₂, u₃, u₂} E D
X Y Z : Comma L R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom (V :=
      (↑((R ⋙ functor L).obj
            (Grothendieck.base (F := R ⋙ functor L)
              { base := Z.right, fiber := mk Z.hom : Grothendieck (R ⋙ functor L) })) :
        Type (max u₁ v₂)))
      (Functor.obj (C :=
        (↑((R ⋙ functor L).obj
              (Grothendieck.base (F := R ⋙ functor L)
                { base := X.right, fiber := mk X.hom : Grothendieck (R ⋙ functor L) })) :
          Type (max u₁ v₂)))
        (Cat.Hom.toFunctor
          ((R ⋙ functor L).map
            (Grothendieck.Hom.base
              (CategoryStruct.comp (Y := { base := Y.right, fiber := mk Y.hom })
                { base := f.right, fiber := homMk f.left ⋯ } { base := g.right, fiber := homMk g.left ⋯ }))))
        (Grothendieck.fiber { base := X.right, fiber := mk X.hom }))
      (Grothendieck.fiber { base := Z.right, fiber := mk Z.hom }))
    (eqToHom ⋯ ≫ Grothendieck.Hom.fiber { base := (f ≫ g).right, fiber := homMk (f ≫ g).left ⋯ })
    (Grothendieck.Hom.fiber
      (CategoryStruct.comp (Y := { base := Y.right, fiber := mk Y.hom }) { base := f.right, fiber := homMk f.left ⋯ }
        { base := g.right, fiber := homMk g.left ⋯ }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
f : StructuredArrow S T
obtain :
  ∀ (X : C) (f : S ⟶ T.obj X),
    ∃ (a : (X : C) × (S ⟶ T.obj X)),
      (fun (f : (X : C) × (S ⟶ T.obj X)) ↦ mk (f.snd (β := fun (X : C) ↦ S ⟶ T.obj X))) a = mk f
⊢ ∃ (a : (X : C) × (S ⟶ T.obj X)),
    (fun (f : (X : C) × (S ⟶ T.obj X)) ↦ mk (f.snd (β := fun (X : C) ↦ S ⟶ T.obj X))) a = f

Tactic:
obtain ⟨X, f, rfl⟩ := f.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
X : C
f : S ⟶ T.obj X
⊢ ∃ (a : (X : C) × (S ⟶ T.obj X)),
    (fun (f : (X : C) × (S ⟶ T.obj X)) ↦ mk (f.snd (β := fun (X : C) ↦ S ⟶ T.obj X))) a = mk f

Tactic:
⟨⟨X, f⟩, rfl⟩

Premises used: Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
X : C
f : S ⟶ T.obj X
⊢ ∃ (a : (X : C) × (S ⟶ T.obj X)),
    (fun (f : (X : C) × (S ⟶ T.obj X)) ↦ mk (f.snd (β := fun (X : C) ↦ S ⟶ T.obj X))) a = mk f

Tactic:
exact ⟨⟨X, f⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
this :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))
rw :
  ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (C := StructuredArrow S T)
    (ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C))))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
this :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (C := StructuredArrow S T)
    (ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C))))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
suffices :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
    rw [this]
    infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
h :
  ∀ (X : StructuredArrow S T),
    P.inverseImage (proj S T) X ↔
      ObjectProperty.ofObj
        (fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C))))
        X
⊢ P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
X : StructuredArrow S T
h : P X.right ↔ ∃ (a : C), P a ∧ ∃ (b : S ⟶ T.obj a), mk b = X
⊢ P.inverseImage (proj S T) X ↔
    ObjectProperty.ofObj
      (fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))) X

Tactic:
simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff, Sigma.exists, Subtype.exists, exists_prop, CategoryTheory.StructuredArrow.proj_obj, CategoryTheory.ObjectProperty.prop_inverseImage_iff
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
w : C
h : P w
w_1 : S ⟶ T.obj w
⊢ P (mk w_1).right

Tactic:
h
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
w : C
h : P w
w_1 : S ⟶ T.obj w
⊢ P (mk w_1).right

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
X : StructuredArrow S T
⊢ P X.right ↔ ∃ (a : C), P a ∧ ∃ (b : S ⟶ T.obj a), mk b = X

Tactic:
exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
rw :
  EssentiallySmall.{w, w, max v₂ w}
    (StructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) S (Equivalence.inverse (equivSmallModel C) ⋙ T))
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (StructuredArrow S T)

Tactic:
rw [← essentiallySmall_congr
    (StructuredArrow.pre S (equivSmallModel.{w} C).inverse T).asEquivalence]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, w, max v₂ w}
    (StructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) S (Equivalence.inverse (equivSmallModel C) ⋙ T))

Tactic:
essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.essentiallySmall_of_small_of_locallySmall
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, w, max v₂ w}
    (StructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) S (Equivalence.inverse (equivSmallModel C) ⋙ T))

Tactic:
exact essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.essentiallySmall_of_small_of_locallySmall
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
f : CostructuredArrow S T
obtain :
  ∀ (X : C) (f : S.obj X ⟶ T),
    ∃ (a : (X : C) × (S.obj X ⟶ T)),
      (fun (f : (X : C) × (S.obj X ⟶ T)) ↦ mk (f.snd (β := fun (X : C) ↦ S.obj X ⟶ T))) a = mk f
⊢ ∃ (a : (X : C) × (S.obj X ⟶ T)),
    (fun (f : (X : C) × (S.obj X ⟶ T)) ↦ mk (f.snd (β := fun (X : C) ↦ S.obj X ⟶ T))) a = f

Tactic:
obtain ⟨X, f, rfl⟩ := f.mk_surjective

Premises used: CategoryTheory.CostructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
X : C
f : S.obj X ⟶ T
⊢ ∃ (a : (X : C) × (S.obj X ⟶ T)),
    (fun (f : (X : C) × (S.obj X ⟶ T)) ↦ mk (f.snd (β := fun (X : C) ↦ S.obj X ⟶ T))) a = mk f

Tactic:
⟨⟨X, f⟩, rfl⟩

Premises used: Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
X : C
f : S.obj X ⟶ T
⊢ ∃ (a : (X : C) × (S.obj X ⟶ T)),
    (fun (f : (X : C) × (S.obj X ⟶ T)) ↦ mk (f.snd (β := fun (X : C) ↦ S.obj X ⟶ T))) a = mk f

Tactic:
exact ⟨⟨X, f⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
this :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))
rw :
  ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (C := CostructuredArrow S T)
    (ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T)))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
this :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (C := CostructuredArrow S T)
    (ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
suffices :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S.obj G ⟶ T => mk f.2 by
    rw [this]
    infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
h :
  ∀ (X : CostructuredArrow S T),
    P.inverseImage (proj S T) X ↔
      ObjectProperty.ofObj
        (fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T)))
        X
⊢ P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
h : P X.left ↔ ∃ (a : C), P a ∧ ∃ (b : S.obj a ⟶ T), mk b = X
⊢ P.inverseImage (proj S T) X ↔
    ObjectProperty.ofObj
      (fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))) X

Tactic:
simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff, Sigma.exists, CategoryTheory.CostructuredArrow.proj_obj, Subtype.exists, exists_prop, CategoryTheory.ObjectProperty.prop_inverseImage_iff
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
w : C
h : P w
w_1 : S.obj w ⟶ T
⊢ P (mk w_1).left

Tactic:
h