case intro.none.intro
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ (∃ y_1, (forget C).map (head f) y_1 = (forget C).map (colimit.ι (wideSpan B X f) none) y) ∨
    ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (colimit.ι (wideSpan B X f) none) y

case intro.some.intro
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (forget C).map (head f) y_1 = (forget C).map (colimit.ι (wideSpan B X f) (some j)) y) ∨
    ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (colimit.ι (wideSpan B X f) (some j)) y
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : (forget C).obj (widePushout B X f)
⊢ (∃ y, (forget C).map (head f) y = x) ∨ ∃ i y, (forget C).map (ι f i) y = x
obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x
case intro.none.intro.h
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ ∃ y_1, (forget C).map (head f) y_1 = (forget C).map (colimit.ι (wideSpan B X f) none) y
case intro.none.intro
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ (∃ y_1, (forget C).map (head f) y_1 = (forget C).map (colimit.ι (wideSpan B X f) none) y) ∨
    ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (colimit.ι (wideSpan B X f) none) y
left
no goals
case intro.none.intro.h
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ ∃ y_1, (forget C).map (head f) y_1 = (forget C).map (colimit.ι (wideSpan B X f) none) y
use y
case intro.some.intro.h
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (colimit.ι (wideSpan B X f) (some j)) y
case intro.some.intro
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (forget C).map (head f) y_1 = (forget C).map (colimit.ι (wideSpan B X f) (some j)) y) ∨
    ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (colimit.ι (wideSpan B X f) (some j)) y
right
no goals
case intro.some.intro.h
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (colimit.ι (wideSpan B X f) (some j)) y
use j, y