case inl.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
⊢ ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (head f) y

case inr.intro.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : (forget C).obj (X i)
⊢ ∃ i_1 y_1, (forget C).map (ι f i_1) y_1 = (forget C).map (ι f i) 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
inst✝² : Nonempty α
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)
⊢ ∃ i y, (forget C).map (ι f i) y = x
rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)
case inl.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
inhabited_h : Inhabited α
⊢ ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (head f) y
case inl.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
⊢ ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (head f) y
inhabit α
case inl.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
inhabited_h : Inhabited α
⊢ (forget C).map (ι f default) ((forget C).map (f default) y) = (forget C).map (head f) y
case inl.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
inhabited_h : Inhabited α
⊢ ∃ i y_1, (forget C).map (ι f i) y_1 = (forget C).map (head f) y
use default, f _ y
no goals
case inl.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
inhabited_h : Inhabited α
⊢ (forget C).map (ι f default) ((forget C).map (f default) y) = (forget C).map (head f) y
simp only [← arrow_ι _ default, comp_apply]
no goals
case inr.intro.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
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : (forget C).obj (X i)
⊢ ∃ i_1 y_1, (forget C).map (ι f i_1) y_1 = (forget C).map (ι f i) y
use i, y