C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
⊢ Transitive (PseudoEqual P)
intro f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst ≫ p) ≫ f.hom = (pullback.snd ≫ q') ≫ h.hom
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h
refine' ⟨pullback q p', pullback.fst ≫ p, pullback.snd ≫ q', epi_comp _ _, epi_comp _ _, _⟩
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst ≫ p) ≫ f.hom = (pullback.snd ≫ q') ≫ h.hom
rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
  Category.assoc]