J : Type w
C : Type u
inst✝² : Category C
D : Type ?u.254030
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
g : widePushout B (fun j => objs j) arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
J : Type w
C : Type u
inst✝² : Category C
D : Type ?u.254030
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
g : widePushout B (fun j => objs j) arrows ⟶ X
j : J
⊢ arrows j ≫ (fun j => ι arrows j ≫ g) j = head arrows ≫ g
rw [← Category.assoc]
no goals
J : Type w
C : Type u
inst✝² : Category C
D : Type ?u.254030
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
g : widePushout B (fun j => objs j) arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
simp
case a
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ ∀ (j : J), ι arrows j ≫ g = ι arrows j ≫ g

case a
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ g =
    desc (head arrows ≫ g) (fun j => ι arrows j ≫ g)
      (_ : ∀ (j : J), arrows j ≫ (fun j => ι arrows j ≫ g) j = head arrows ≫ g)
apply eq_desc_of_comp_eq
case a
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g
case a
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ ∀ (j : J), ι arrows j ≫ g = ι arrows j ≫ g

case a
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g
aesop_cat
no goals
case a
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
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g
rfl