C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
⊢ Function.Injective (pseudoApply f)
intro abar abar'
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ Quotient.mk (setoid P) a = Quotient.mk (setoid P) a'
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'
refine' Quotient.inductionOn₂ abar abar' fun a a' ha => _
case a
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ a ≈ a'
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ Quotient.mk (setoid P) a = Quotient.mk (setoid P) a'
apply Quotient.sound
case a
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
⊢ a ≈ a'
case a
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ a ≈ a'
have : ⟦(a.hom ≫ f : Over Q)⟧ = ⟦↑(a'.hom ≫ f)⟧ := by convert ha
case a
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ a ≈ a'
case a
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
⊢ a ≈ a'
have ⟨R, p, q, ep, Eq, comm⟩ := Quotient.exact this
no goals
case a
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ a ≈ a'
exact ⟨R, p, q, ep, Eq, (cancel_mono f).1 <| by
  simp only [Category.assoc]
  exact comm⟩
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ Quotient.mk ?m.297761 (Over.mk (a.hom ≫ f)) = Quotient.mk ?m.297761 (Over.mk (a'.hom ≫ f))
convert ha
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f
simp only [Category.assoc]
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
exact comm