C : Type u₁
inst✝² : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inl s
C : Type u₁
inst✝² : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit (CommSq.cocone sq)
refine'
  PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => _)
    (by aesop_cat) (by aesop_cat)
no goals
C : Type u₁
inst✝² : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inl s
simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]
no goals
C : Type u₁
inst✝² : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g), inr ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inr s
aesop_cat
no goals
C : Type u₁
inst✝² : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt),
    inl ≫ m = PushoutCocone.inl s → inr ≫ m = PushoutCocone.inr s → m = (fun s => inv inr ≫ PushoutCocone.inr s) s
aesop_cat