C : Type u₁
inst✝² : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun s => PullbackCone.fst s ≫ inv fst) s ≫ snd = PullbackCone.snd s
C : Type u₁
inst✝² : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ IsLimit (CommSq.cone sq)
refine'
  PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by aesop_cat)
    (fun s => _) (by aesop_cat)
no goals
C : Type u₁
inst✝² : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun s => PullbackCone.fst s ≫ inv fst) s ≫ snd = PullbackCone.snd s
simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition]
no goals
C : Type u₁
inst✝² : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g), (fun s => PullbackCone.fst s ≫ inv fst) s ≫ fst = PullbackCone.fst s
aesop_cat
no goals
C : Type u₁
inst✝² : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P),
    m ≫ fst = PullbackCone.fst s → m ≫ snd = PullbackCone.snd s → m = (fun s => PullbackCone.fst s ≫ inv fst) s
aesop_cat