case h₀
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst = 𝟙 (pullback f f) ≫ pullback.fst

case h₁
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd = 𝟙 (pullback f f) ≫ pullback.snd
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom = 𝟙 (pullback f f)
ext
case h₁
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd = 𝟙 (pullback f f) ≫ pullback.snd
case h₀
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst = 𝟙 (pullback f f) ≫ pullback.fst

case h₁
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd = 𝟙 (pullback f f) ≫ pullback.snd
simp [fst_eq_snd_of_mono_eq]
no goals
case h₁
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd = 𝟙 (pullback f f) ≫ pullback.snd
simp [fst_eq_snd_of_mono_eq]