J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ g1 = g2
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2
intro h1 h2
case w
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ ∀ (j : WidePushoutShape J),
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) j ≫ g1 =
      colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) j ≫ g2
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ g1 = g2
apply colimit.hom_ext
case w.none
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) none ≫ g2

case w.some
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) (some val✝) ≫ g2
case w
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ ∀ (j : WidePushoutShape J),
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) j ≫ g1 =
      colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) j ≫ g2
rintro (_ | _)
no goals
case w.none
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) none ≫ g2
apply h2
no goals
case w.some
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) (some val✝) ≫ g2
apply h1