awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom
have rw₁ : t ≫ eX.hom ≫ CategoryStruct.comp (Y := functorObj f πX) (ιFunctorObj f πX) (πFunctorObj f πX) = f i ≫ b ≫ eS.hom
Tactic: rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom
have rw₂ : t ≫ ι' ≫ eZ.hom ≫ πFunctorObj f πX = f i ≫ b ≫ eS.hom
Tactic: rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom
have rw₃ : t ≫ ι' ≫ πZ' ≫ eS.hom = f i ≫ b ≫ eS.hom
Tactic: rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom
have rw₄ : t ≫ πX' ≫ eS.hom = f i ≫ b ≫ eS.hom
Tactic: rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom
have rw₅ : f i ≫ b ≫ eS.hom = f i ≫ b ≫ eS.hom
Tactic: rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 ⟶ Z'), f i ≫ l = t ≫ ι' ∧ l ≫ πZ' = b
have 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
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]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
have refine_1 : f i ≫ l ≫ eZ.inv = t ≫ ι'
Tactic: refine ⟨l ≫ eZ.inv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 ≫ ι'
⊢ ∃ (l : B i ⟶ Z'), f i ≫ l = t ≫ ι' ∧ l ≫ πZ' = b
have refine_2 : (l ≫ eZ.inv) ≫ πZ' = b
Tactic: refine ⟨l ≫ eZ.inv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ f i ≫ l ≫ eZ.inv = t ≫ ι'
have refine_1 : t ≫ eX.hom ≫ ιFunctorObj f πX ≫ eZ.inv = t ≫ ι'
Tactic: rw [reassoc_of% hl₁, ← reassoc_of% commι, eZ.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 ≫ ι'
⊢ f i ≫ l ≫ eZ.inv = t ≫ ι'
have refine_1₁ : t ≫ ι' ≫ eZ.hom ≫ eZ.inv = t ≫ ι'
Tactic: rw [reassoc_of% hl₁, ← reassoc_of% commι, eZ.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 ≫ ι'
⊢ f i ≫ l ≫ eZ.inv = t ≫ ι'
have refine_1₂ : t ≫ ι' ≫ 𝟙 Z' = t ≫ ι'
Tactic: rw [reassoc_of% hl₁, ← reassoc_of% commι, eZ.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 ≫ ι'
⊢ f i ≫ l ≫ eZ.inv = t ≫ ι'
have refine_1₃ : t ≫ ι' = t ≫ ι'
Tactic: rw [reassoc_of% hl₁, ← reassoc_of% commι, eZ.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 ≫ eZ.inv) ≫ πZ' = b
have refine_2 : ((l ≫ eZ.inv) ≫ πZ') ≫ eS.hom = b ≫ eS.hom
Tactic: rw [← cancel_mono eS.hom, assoc, assoc, commπ, eZ.inv_hom_id_assoc, hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (l ≫ eZ.inv) ≫ πZ' = b
have refine_2₁ : (l ≫ eZ.inv) ≫ πZ' ≫ eS.hom = b ≫ eS.hom
Tactic: rw [← cancel_mono eS.hom, assoc, assoc, commπ, eZ.inv_hom_id_assoc, hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (l ≫ eZ.inv) ≫ πZ' = b
have refine_2₂ : l ≫ eZ.inv ≫ πZ' ≫ eS.hom = b ≫ eS.hom
Tactic: rw [← cancel_mono eS.hom, assoc, assoc, commπ, eZ.inv_hom_id_assoc, hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (l ≫ eZ.inv) ≫ πZ' = b
have refine_2₃ : l ≫ eZ.inv ≫ eZ.hom ≫ πFunctorObj f πX = b ≫ eS.hom
Tactic: rw [← cancel_mono eS.hom, assoc, assoc, commπ, eZ.inv_hom_id_assoc, hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ (l ≫ eZ.inv) ≫ πZ' = b
have refine_2₅ : b ≫ eS.hom = b ≫ eS.hom
Tactic: rw [← cancel_mono eS.hom, assoc, assoc, commπ, eZ.inv_hom_id_assoc, hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯ =
    𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom))
have h₁ : Arrow.Hom.left (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) sorry) =
  Arrow.Hom.left (𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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)))
⊢ Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯ =
    𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom))
have h₂ : Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) sorry) =
  Arrow.Hom.right (𝟙 (Arrow.mk (X := functorObj f g.hom) (πFunctorObj f g.hom)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯ =
    Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯
have h₁ : Arrow.Hom.left (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) sorry) =
  Arrow.Hom.left
    (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) sorry ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 τ') ⋯)
⊢ Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯ =
    Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯
have h₂ : Arrow.Hom.right (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) sorry) =
  Arrow.Hom.right
    (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) sorry ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') sorry)
Tactic: ext