awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
rw : t ≫ eX.hom ≫ πX = f i ≫ b ≫ eS.hom
rw₁ : t ≫ eX.hom ≫ CategoryStruct.comp (Y := functorObj f πX) (ιFunctorObj f πX) (πFunctorObj f πX) = f i ≫ b ≫ eS.hom
rw₂ : t ≫ ι' ≫ eZ.hom ≫ πFunctorObj f πX = f i ≫ b ≫ eS.hom
rw₃ : t ≫ ι' ≫ πZ' ≫ eS.hom = f i ≫ b ≫ eS.hom
rw₄ : t ≫ πX' ≫ eS.hom = f i ≫ b ≫ eS.hom
rw₅ rw₆ : f i ≫ b ≫ eS.hom = f i ≫ b ≫ eS.hom
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom

Tactic:
rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
obtain :
  ∀ (l : B i ⟶ functorObj f πX) (hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX)
    (hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom), ∃ (l : B i ⟶ Z'), f i ≫ l = t ≫ ι' ∧ l ≫ πZ' = b
⊢ ∃ (l : B i ⟶ Z'), f i ≫ l = t ≫ ι' ∧ l ≫ πZ' = b

Tactic:
obtain ⟨l, hl₁, hl₂⟩ :=
    ιFunctorObj_extension f (πX := πX) (i := i) (t ≫ eX.hom) (b ≫ eS.hom) ⟨by
      rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.SmallObject.ιFunctorObj_extension, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
⊢ ∃ (l : B i ⟶ Z'), f i ≫ l = t ≫ ι' ∧ l ≫ πZ' = b

Tactic:
⟨l ≫ eZ.inv, ?_, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
refine_1 : f i ≫ l ≫ eZ.inv = t ≫ ι'
refine_2 : (l ≫ eZ.inv) ≫ πZ' = b
⊢ ∃ (l : B i ⟶ Z'), f i ≫ l = t ≫ ι' ∧ l ≫ πZ' = b

Tactic:
refine ⟨l ≫ eZ.inv, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
refine_1 : t ≫ eX.hom ≫ ιFunctorObj f πX ≫ eZ.inv = t ≫ ι'
refine_1₁ : t ≫ ι' ≫ eZ.hom ≫ eZ.inv = t ≫ ι'
refine_1₂ : t ≫ ι' ≫ 𝟙 Z' = t ≫ ι'
refine_1₃ refine_1₄ : t ≫ ι' = t ≫ ι'
⊢ f i ≫ l ≫ eZ.inv = t ≫ ι'

Tactic:
rw [reassoc_of% hl₁, ← reassoc_of% commι, eZ.hom_inv_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
refine_2 : ((l ≫ eZ.inv) ≫ πZ') ≫ eS.hom = b ≫ eS.hom
refine_2₁ : (l ≫ eZ.inv) ≫ πZ' ≫ eS.hom = b ≫ eS.hom
refine_2₂ : l ≫ eZ.inv ≫ πZ' ≫ eS.hom = b ≫ eS.hom
refine_2₃ : l ≫ eZ.inv ≫ eZ.hom ≫ πFunctorObj f πX = b ≫ eS.hom
refine_2₄ : l ≫ πFunctorObj f πX = b ≫ eS.hom
refine_2₅ refine_2₆ : b ≫ eS.hom = b ≫ eS.hom
⊢ (l ≫ eZ.inv) ≫ πZ' = b

Tactic:
rw [← cancel_mono eS.hom, assoc, assoc, commπ, eZ.inv_hom_id_assoc, hl₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow.{v, u} C
h₁ :
  Arrow.Hom.left (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom)))
h₂ :
  Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom)))
⊢ Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯ =
    𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow.{v, u} C
⊢ Arrow.Hom.left (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom)))

Tactic:
apply functorMap_id

Premises used: CategoryTheory.SmallObject.functorMap_id
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow.{v, u} C
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
h₁ :
  Arrow.Hom.left (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)
h₂ :
  Arrow.Hom.right (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)
⊢ Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯ =
    Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
h₁ :
  Eq (α := functorObj f π₁.hom ⟶ functorObj f π₃.hom) (functorMap f (τ ≫ τ'))
    (CategoryStruct.comp (Y := functorObj f π₂.hom) (functorMap f τ) (functorMap f τ'))
⊢ Arrow.Hom.left (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ (t ≫ Arrow.Hom.left τ) ≫ π₂.hom = f i ≫ b ≫ Arrow.Hom.right τ

Tactic:
simp [reassoc_of% w]
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ (b ≫ Arrow.Hom.right τ) ≫ Arrow.Hom.right τ' = b ≫ Arrow.Hom.right τ ≫ Arrow.Hom.right τ'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ (t ≫ Arrow.Hom.left τ) ≫ Arrow.Hom.left τ' = t ≫ Arrow.Hom.left (τ ≫ τ')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ IsSmall.{w, v, u} I

Tactic:
IsCardinalForSmallObjectArgument.isSmall κ

Premises used: CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.isSmall
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ LocallySmall.{w, v, u} C

Tactic:
IsCardinalForSmallObjectArgument.locallySmall I κ

Premises used: CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ HasIterationOfShape.{w, v, u} κ.ord.ToType C

Tactic:
IsCardinalForSmallObjectArgument.hasIterationOfShape I

Premises used: CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasIterationOfShape
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ HasPushouts.{v, u} C

Tactic:
IsCardinalForSmallObjectArgument.hasPushouts I κ

Premises used: CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasPushouts
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ HasCoproducts.{w, v, u} C

Tactic:
IsCardinalForSmallObjectArgument.hasCoproducts I κ

Premises used: CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasCoproducts
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
A B X Y : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦ (↑I.toSet : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑I.toSet : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑I.toSet : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ I.homFamily) f
⊢ PreservesColimit hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦ (↑I.toSet : Type (max u v))).F
    (Functor.obj coyoneda (Opposite.op A))

Tactic:
IsCardinalForSmallObjectArgument.preservesColimit i hi f hf

Premises used: CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
⊢ LocallySmall.{w, v, u} C

Tactic:
haveI := locallySmall I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this : LocallySmall.{w, v, u} C
⊢ IsSmall.{w, v, u} I

Tactic:
haveI := isSmall I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this_1 : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ HasCoproducts.{w, v, u} C

Tactic:
haveI := hasCoproducts I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this : HasCoproducts.{w, v, u} C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
hasColimitsOfShape_of_equivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, equivShrink, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this : HasCoproducts.{w, v, u} C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
exact hasColimitsOfShape_of_equivalence
    (Discrete.equivalence (equivShrink.{w} _)).symm
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ LocallySmall.{w, v, u} C

Tactic:
haveI := locallySmall I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
this : LocallySmall.{w, v, u} C
⊢ IsSmall.{w, v, u} I

Tactic:
haveI := isSmall I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
this_1 : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
haveI := hasColimitsOfShape_discrete I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
⊢ HasPushouts.{v, u} C

Tactic:
haveI := hasPushouts I κ
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X : Arrow.{v, u} C ⥤ Arrow.{v, u} C
_ :
  ∀ ⦃Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C⦄ (f : X ⟶ Y),
    (succStruct I κ).prop f → (propArrow I).functorCategory (Arrow.{v, u} C) f
⊢ ∀ ⦃Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C⦄ (f : X ⟶ Y),
    (succStruct I κ).prop f → (propArrow I).functorCategory (Arrow.{v, u} C) f

Tactic:
_
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
_ : ∀ (f : X ⟶ Y), (succStruct I κ).prop f → (propArrow I).functorCategory (Arrow.{v, u} C) f
⊢ ∀ (f : X ⟶ Y), (succStruct I κ).prop f → (propArrow I).functorCategory (Arrow.{v, u} C) f

Tactic:
_