awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ : Cocone D₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
refine_1 : v ≫ c'.ι.app j₃ ≫ t₂.app j₂ = u
refine_2 : P (p ≫ v)
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)

Tactic:
refine ⟨D'.obj j₃, v, c'.ι.app j₃ ≫ t₂.app j₂, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ : Cocone D₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
refine_1 refine_1₁ refine_1₂ refine_1₃ : q ≫ t₂.app j₂ = u
⊢ v ≫ c'.ι.app j₃ ≫ t₂.app j₂ = u

Tactic:
rwa [reassoc_of% hq]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ : Cocone D₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
refine_2 : P (s'.app j₃)
⊢ P (p ≫ v)

Tactic:
rw [hcomp']
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ : Cocone D₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
⊢ P (s'.app j₃)

Tactic:
P.comp_mem _ _ (h₁ _).left (P.pushout_inl _ _ hf')

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.pushout_inl, And.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ : Cocone D₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
⊢ P (s'.app j₃)

Tactic:
exact P.comp_mem _ _ (h₁ _).left (P.pushout_inl _ _ hf')

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.pushout_inl, And.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
ι : Type t
inst_1 : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : (i : ι) → (↑(ofHoms f).toSet : Type (max u v)) :=
  fun (i : ι) ↦ Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯
X Y : C
i : ι
⊢ ∃ (a : ι),
    φ a = Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) { left := A i, right := B i, hom := f i } ⋯

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
ι : Type t
inst_1 : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : (i : ι) → (↑(ofHoms f).toSet : Type (max u v)) :=
  fun (i : ι) ↦ Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯
X Y : C
i : ι
⊢ ∃ (a : ι),
    φ a = Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) { left := A i, right := B i, hom := f i } ⋯

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
ι : Type t
inst_1 : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : (i : ι) → (↑(ofHoms f).toSet : Type (max u v)) :=
  fun (i : ι) ↦ Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯
⊢ Function.Surjective φ

Tactic:
have hφ : Function.Surjective φ := by
    rintro ⟨⟨_, _, f⟩, ⟨i⟩⟩
    exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
ι : Type t
inst_1 : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : (i : ι) → (↑(ofHoms f).toSet : Type (max u v)) :=
  fun (i : ι) ↦ Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯
hφ : Function.Surjective φ
⊢ IsSmall.{w, v, u} (ofHoms f)

Tactic:
⟨small_of_surjective hφ⟩

Premises used: small_of_surjective, CategoryTheory.MorphismProperty.IsSmall.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
ι : Type t
inst_1 : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : (i : ι) → (↑(ofHoms f).toSet : Type (max u v)) :=
  fun (i : ι) ↦ Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯
hφ : Function.Surjective φ
⊢ IsSmall.{w, v, u} (ofHoms f)

Tactic:
exact ⟨small_of_surjective hφ⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
mp : IsSmall.{w, v, u} W → ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f
mpr : (∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f) → IsSmall.{w, v, u} W
⊢ IsSmall.{w, v, u} W ↔ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
⊢ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f

Tactic:
⟨Shrink.{w} W.toSet, _, _, fun i ↦ ((equivShrink _).symm i).1.hom, ?_⟩

Premises used: Set.Elem, CategoryTheory.Arrow.hom, CategoryTheory.MorphismProperty.toSet, Exists.intro, Shrink, Equiv.symm, equivShrink, Subtype.val, DFunLike.coe
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
mp :
  W =
    ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.right.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.hom
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C)
⊢ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f

Tactic:
refine ⟨Shrink.{w} W.toSet, _, _, fun i ↦ ((equivShrink _).symm i).1.hom, ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
mp :
  ∀ ⦃A B : C⦄ (f : A ⟶ B),
    W f ↔
      ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
        Arrow.left.{v, u}
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
        (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
        Arrow.right.{v, u}
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
        (fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
          Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
        f
⊢ W =
    ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.right.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.hom
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C)

Tactic:
ext A B f
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
mp :
  W f ↔
    ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
⊢ W f ↔
    ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.right.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
        Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
      f

Tactic:
rw [ofHoms_iff]

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
mp :
  W f →
    ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
mp₁ :
  (∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))) →
    W f
⊢ W f ↔
    ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ Arrow.mk f =
    Arrow.mk (X :=
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              ((equivShrink (↑W.toSet : Type (max u v)) :
                  (a : (↑W.toSet : Type (max u v))) → Shrink.{w, max u v} (↑W.toSet : Type (max u v)))
                (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ W.toSet) (Arrow.mk f) hf))) :
          Arrow C))
      (Arrow.hom
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              ((equivShrink (↑W.toSet : Type (max u v)) :
                  (a : (↑W.toSet : Type (max u v))) → Shrink.{w, max u v} (↑W.toSet : Type (max u v)))
                (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ W.toSet) (Arrow.mk f) hf))) :
          Arrow C))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
    Arrow.mk f =
      Arrow.mk (X :=
        Arrow.left.{v, u}
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
        (Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))

Tactic:
exact ⟨equivShrink _ ⟨f, hf⟩, by simp⟩