case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h
case intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
obtain ⟨l, hl₁, hl₂⟩ := @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom) (by
  simp only [Category.assoc]
  exact comm)
no goals
case intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
exact ⟨l, ⟨Quotient.sound ⟨Z, 𝟙 Z, a, inferInstance, ea, by rwa [Category.id_comp]⟩,
  Quotient.sound ⟨Z, 𝟙 Z, b, inferInstance, eb, by rwa [Category.id_comp]⟩⟩⟩
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ (a ≫ x.hom) ≫ f = (b ≫ y.hom) ≫ g
simp only [Category.assoc]
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g
exact comm
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 => app pullback.fst g_1) (Over.mk l)).hom = a ≫ x.hom
rwa [Category.id_comp]
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 => app pullback.snd g_1) (Over.mk l)).hom = b ≫ y.hom
rwa [Category.id_comp]