no goals
C : Type ?u.9333
inst✝¹ : Category C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f
simp [condition]
no goals
C : Type ?u.9333
inst✝¹ : Category C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f
simp [condition]
C : Type u_2
inst✝¹ : Category C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ fst ≫ i₁ ≫ fst = fst ≫ 𝟙 X
C : Type u_2
inst✝¹ : Category C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ fst ≫ i₁ ≫ fst = fst
conv_rhs => rw [← Category.comp_id pullback.fst]
no goals
C : Type u_2
inst✝¹ : Category C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ fst ≫ i₁ ≫ fst = fst ≫ 𝟙 X
rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]