[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X✝ Y✝ : C
g : X✝ ⟶ 0
f : X✝ ⟶ Y✝
inst✝ : Mono f
⊢ f ≫ 0 = g
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono
[GOAL]
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨h ≫ i.hom, _⟩
[GOAL]
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g
[PROOFSTEP]
rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
z : Y✝
⊢ X
[PROOFSTEP]
classical exact if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
z : Y✝
⊢ X
[PROOFSTEP]
exact if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ fun z => if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some (_ : Nonempty X)) = g
[PROOFSTEP]
ext y
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (f ≫ fun z => if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some (_ : Nonempty X)) y = g y
[PROOFSTEP]
classical
change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
split_ifs <;> rename_i h
· rw [mono_iff_injective] at mono
  erw [mono (Classical.choose_spec h)]
· exact False.elim (h ⟨y, rfl⟩)
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (f ≫ fun z => if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some (_ : Nonempty X)) y = g y
[PROOFSTEP]
change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (if h : f y ∈ Set.range f then g (Classical.choose h) else (fun h => Nonempty.some (_ : Nonempty X)) h) = g y
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h✝ : f y ∈ Set.range f
⊢ g (Classical.choose h✝) = g y
[PROOFSTEP]
rename_i h
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h✝ : ¬f y ∈ Set.range f
⊢ (fun h => Nonempty.some (_ : Nonempty X)) h✝ = g y
[PROOFSTEP]
rename_i h
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : f y ∈ Set.range f
⊢ g (Classical.choose h) = g y
[PROOFSTEP]
rw [mono_iff_injective] at mono
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Function.Injective f
y : X✝
h : f y ∈ Set.range f
⊢ g (Classical.choose h) = g y
[PROOFSTEP]
erw [mono (Classical.choose_spec h)]
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : ¬f y ∈ Set.range f
⊢ (fun h => Nonempty.some (_ : Nonempty X)) h = g y
[PROOFSTEP]
exact False.elim (h ⟨y, rfl⟩)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Type u₁
⊢ Mono some
[PROOFSTEP]
rw [mono_iff_injective]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Type u₁
⊢ Function.Injective some
[PROOFSTEP]
exact Option.some_injective X
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
use Limits.prod.lift (factorThru (g ≫ Limits.prod.fst) f) (factorThru (g ≫ Limits.prod.snd) f)
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ f ≫ prod.lift (factorThru (g ≫ prod.fst) f) (factorThru (g ≫ prod.snd) f) = g
[PROOFSTEP]
simp only [prod.comp_lift, comp_factorThru]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g
[PROOFSTEP]
ext
[GOAL]
case h.h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.fst = g ≫ prod.fst
[PROOFSTEP]
simp only [prod.lift_fst]
[GOAL]
case h.h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.snd = g ≫ prod.snd
[PROOFSTEP]
simp only [prod.lift_snd]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨Pi.lift fun b => factorThru (g ≫ Pi.π c _) f, _⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ Pi.lift fun b => factorThru (g ≫ Pi.π c b) f) = g
[PROOFSTEP]
ext b
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
b : β
⊢ (f ≫ Pi.lift fun b => factorThru (g ≫ Pi.π c b) f) ≫ Pi.π c b = g ≫ Pi.π c b
[PROOFSTEP]
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app, comp_factorThru]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f), _⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) ≫ biprod.fst = g ≫ biprod.fst
[PROOFSTEP]
simp only [Category.assoc, biprod.lift_fst, comp_factorThru]
[GOAL]
case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) ≫ biprod.snd = g ≫ biprod.snd
[PROOFSTEP]
simp only [Category.assoc, biprod.lift_snd, comp_factorThru]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, _⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biproduct.lift fun b => factorThru (g ≫ biproduct.π c b) f) = g
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
j✝ : β
⊢ (f ≫ biproduct.lift fun b => factorThru (g ≫ biproduct.π c b) f) ≫ biproduct.π c j✝ = g ≫ biproduct.π c j✝
[PROOFSTEP]
simp only [Category.assoc, biproduct.lift_π, comp_factorThru]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ
inst✝ : Projective P
X✝ Y✝ : C
g : X✝ ⟶ P.unop
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.op f.op).unop).op = g.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Cᵒᵖ
inst✝ : Injective J
E✝ X✝ : C
f : J.unop ⟶ X✝
e : E✝ ⟶ X✝
he : Epi e
⊢ ((factorThru f.op e.op).unop ≫ e).op = f.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : C
inst✝ : Injective J
E✝ X✝ : Cᵒᵖ
f : op J ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ ((factorThru f.unop e.unop).op ≫ e).unop = f.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : C
inst✝ : Projective P
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ op P
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.unop f.unop).op).unop = g.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op (op J))) ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
exact Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝¹ : PreservesMonomorphisms L
adj : L ⊣ R
J : D
inst✝ : Injective J
A x✝ : C
g : A ⟶ R.obj J
f : A ⟶ x✝
im : Mono f
⊢ ↑(Adjunction.homEquiv adj A J).symm
      (f ≫ ↑(Adjunction.homEquiv adj x✝ J) (factorThru (↑(Adjunction.homEquiv adj A J).symm g) (L.map f))) =
    ↑(Adjunction.homEquiv adj A J).symm g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasImages Cᵒᵖ
inst✝¹ : HasEqualizers Cᵒᵖ
J Q R S : C
inst✝ : Injective J
h : R ⟶ J
f : Q ⟶ R
g : R ⟶ S
hgf : Exact g.op f.op
w : f ≫ h = 0
⊢ g ≫ desc h f g hgf w = h
[PROOFSTEP]
convert congr_arg Quiver.Hom.unop (Exact.lift_comp h.op g.op f.op hgf (congrArg Quiver.Hom.op w))
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
⊢ ∀ [inst : Mono g], ∃ h, g ≫ h = f
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w, h⟩
[GOAL]
case intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ NatTrans.app adj.counit I
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
use adj.unit.app Y ≫ G.map w
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ NatTrans.app adj.counit I
⊢ g ≫ NatTrans.app adj.unit Y ≫ G.map w = f
[PROOFSTEP]
rw [← unit_naturality_assoc, ← G.map_comp, h]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ NatTrans.app adj.counit I
⊢ NatTrans.app adj.unit X ≫ G.map (F.map f ≫ NatTrans.app adj.counit I) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full G
inst✝ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
⊢ ∀ [inst : Mono g], ∃ h, g ≫ h = f
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjointPreservesLimits
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
rcases hI.factors (G.map f) (G.map g) with ⟨w, h⟩
[GOAL]
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ g ≫ inv (NatTrans.app adj.counit Y) ≫ F.map w ≫ NatTrans.app adj.counit I = f
[PROOFSTEP]
refine' Faithful.map_injective (F := G) _
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ G.map (g ≫ inv (NatTrans.app adj.counit Y) ≫ F.map w ≫ NatTrans.app adj.counit I) = G.map f
[PROOFSTEP]
simpa
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{?u.56282, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesMonomorphisms F
X : D
I : InjectivePresentation X
⊢ Mono (G.map I.f)
[PROOFSTEP]
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjointPreservesLimits
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{?u.56282, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesMonomorphisms F
X : D
I : InjectivePresentation X
this : PreservesLimitsOfSize.{0, 0, ?u.56282, v₁, u_1, u₁} G
⊢ Mono (G.map I.f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives C ↔ EnoughInjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives C → EnoughInjectives D
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives D → EnoughInjectives C
[PROOFSTEP]
all_goals intro H; constructor; intro X; constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives C → EnoughInjectives D
[PROOFSTEP]
intro H
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
⊢ EnoughInjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
⊢ ∀ (X : D), Nonempty (InjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mp.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
X : D
⊢ Nonempty (InjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives D → EnoughInjectives C
[PROOFSTEP]
intro H
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
⊢ EnoughInjectives C
[PROOFSTEP]
constructor
[GOAL]
case mpr.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
⊢ ∀ (X : C), Nonempty (InjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mpr.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
X : C
⊢ Nonempty (InjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation.val
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
X : D
⊢ InjectivePresentation X
[PROOFSTEP]
exact F.symm.injectivePresentationOfMapInjectivePresentation _ (Nonempty.some (H.presentation (F.inverse.obj X)))
[GOAL]
case mpr.presentation.val
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
X : C
⊢ InjectivePresentation X
[PROOFSTEP]
exact F.injectivePresentationOfMapInjectivePresentation X (Nonempty.some (H.presentation (F.functor.obj X)))


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
E✝ X✝ : C
f : 0 ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
⊢ 0 ≫ e = f
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q : C
i : P ≅ Q
hP : Projective P
E✝ X✝ : C
f : Q ⟶ X✝
e : E✝ ⟶ X✝
e_epi : Epi e
f' : P ⟶ E✝
hf' : f' ≫ e = i.hom ≫ f
⊢ (i.inv ≫ f') ≫ e = f
[PROOFSTEP]
simp [hf']
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
P Q : C
inst✝² : HasBinaryCoproduct P Q
inst✝¹ : Projective P
inst✝ : Projective Q
E✝ X✝ : C
f : P ⨿ Q ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ coprod.desc (factorThru (coprod.inl ≫ f) e) (factorThru (coprod.inr ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
β : Type v
g : β → C
inst✝¹ : HasCoproduct g
inst✝ : ∀ (b : β), Projective (g b)
E✝ X✝ : C
f : ∐ g ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ (Sigma.desc fun b => factorThru (Sigma.ι g b ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Projective P
inst✝ : Projective Q
E✝ X✝ : C
f : P ⊞ Q ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ biprod.desc (factorThru (biprod.inl ≫ f) e) (factorThru (biprod.inr ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
β : Type v
g : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct g
inst✝ : ∀ (b : β), Projective (g b)
E✝ X✝ : C
f : ⨁ g ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ (biproduct.desc fun b => factorThru (biproduct.ι g b ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = NatTrans.app adj.unit P ≫ G.map f
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
use F.map f' ≫ adj.counit.app _
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = NatTrans.app adj.unit P ≫ G.map f
⊢ (F.map f' ≫ NatTrans.app adj.counit E✝) ≫ g = f
[PROOFSTEP]
rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = NatTrans.app adj.unit P ≫ G.map f
⊢ F.map (NatTrans.app adj.unit P ≫ G.map f) ≫ NatTrans.app adj.counit X✝ = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
haveI := Adjunction.leftAdjointPreservesColimits.{0, 0} adj
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
rcases(@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
use adj.unit.app _ ≫ G.map f' ≫ (inv <| adj.unit.app _)
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ (NatTrans.app adj.unit P ≫ G.map f' ≫ inv (NatTrans.app adj.unit E✝)) ≫ g = f
[PROOFSTEP]
refine' Faithful.map_injective (F := F) _
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ F.map ((NatTrans.app adj.unit P ≫ G.map f' ≫ inv (NatTrans.app adj.unit E✝)) ≫ g) = F.map f
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives C ↔ EnoughProjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
[PROOFSTEP]
all_goals intro H; constructor; intro X; constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D
[PROOFSTEP]
intro H
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
⊢ EnoughProjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
⊢ ∀ (X : D), Nonempty (ProjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mp.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
X : D
⊢ Nonempty (ProjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
[PROOFSTEP]
intro H
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ EnoughProjectives C
[PROOFSTEP]
constructor
[GOAL]
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X
[PROOFSTEP]
exact F.symm.projectivePresentationOfMapProjectivePresentation _ (Nonempty.some (H.presentation (F.inverse.obj X)))
[GOAL]
case mpr.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X
[PROOFSTEP]
exact F.projectivePresentationOfMapProjectivePresentation X (Nonempty.some (H.presentation (F.functor.obj X)))
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
⊢ lift h f g hfg w ≫ f = h
[PROOFSTEP]
simp only [Exact.lift]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
⊢ factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
        (factorThruImageSubobject f) ≫
      f =
    h
[PROOFSTEP]
conv_lhs =>
  congr
  rfl
  rw [← imageSubobject_arrow_comp f]
    -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
      (factorThruImageSubobject f) ≫
    f
[PROOFSTEP]
  congr
  rfl
  rw [← imageSubobject_arrow_comp f]
    -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
      (factorThruImageSubobject f) ≫
    f
[PROOFSTEP]
  congr
  rfl
  rw [← imageSubobject_arrow_comp f]
    -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
      (factorThruImageSubobject f) ≫
    f
[PROOFSTEP]
congr
[GOAL]
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
    (factorThruImageSubobject f)
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| f
[PROOFSTEP]
rfl
[GOAL]
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| f
[PROOFSTEP]
rw [← imageSubobject_arrow_comp f]
  -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
⊢ factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
        (factorThruImageSubobject f) ≫
      factorThruImageSubobject f ≫ Subobject.arrow (imageSubobject f) =
    h
[PROOFSTEP]
haveI := hfg.epi
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
        (factorThruImageSubobject f) ≫
      factorThruImageSubobject f ≫ Subobject.arrow (imageSubobject f) =
    h
[PROOFSTEP]
rw [← Category.assoc, factorThru_comp, ← imageToKernel_arrow f g, ← Category.assoc,
  CategoryTheory.Projective.factorThru_comp, factorThruKernelSubobject_comp_arrow]


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ EckmannHilton.IsUnital (fun x x_1 => leftAdd X Y x x_1) 0
[PROOFSTEP]
have hr : ∀ f : X ⟶ Y, biprod.lift (0 : X ⟶ Y) f = f ≫ biprod.inr :=
  by
  intro f
  ext
  · aesop_cat
  · simp [biprod.lift_fst, Category.assoc, biprod.inr_fst, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
[PROOFSTEP]
intro f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f = f ≫ biprod.inr
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f ≫ biprod.fst = (f ≫ biprod.inr) ≫ biprod.fst
[PROOFSTEP]
aesop_cat
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f ≫ biprod.snd = (f ≫ biprod.inr) ≫ biprod.snd
[PROOFSTEP]
simp [biprod.lift_fst, Category.assoc, biprod.inr_fst, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
⊢ EckmannHilton.IsUnital (fun x x_1 => leftAdd X Y x x_1) 0
[PROOFSTEP]
have hl : ∀ f : X ⟶ Y, biprod.lift f (0 : X ⟶ Y) = f ≫ biprod.inl :=
  by
  intro f
  ext
  · aesop_cat
  · simp [biprod.lift_snd, Category.assoc, biprod.inl_snd, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
⊢ ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
[PROOFSTEP]
intro f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
f : X ⟶ Y
⊢ biprod.lift f 0 = f ≫ biprod.inl
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
f : X ⟶ Y
⊢ biprod.lift f 0 ≫ biprod.fst = (f ≫ biprod.inl) ≫ biprod.fst
[PROOFSTEP]
aesop_cat
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
f : X ⟶ Y
⊢ biprod.lift f 0 ≫ biprod.snd = (f ≫ biprod.inl) ≫ biprod.snd
[PROOFSTEP]
simp [biprod.lift_snd, Category.assoc, biprod.inl_snd, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
⊢ EckmannHilton.IsUnital (fun x x_1 => leftAdd X Y x x_1) 0
[PROOFSTEP]
exact
  ⟨⟨fun f => by simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc]⟩,
    ⟨fun f => by simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]⟩⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
f : X ⟶ Y
⊢ leftAdd X Y 0 f = f
[PROOFSTEP]
simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
f : X ⟶ Y
⊢ leftAdd X Y f 0 = f
[PROOFSTEP]
simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ EckmannHilton.IsUnital (fun x x_1 => rightAdd X Y x x_1) 0
[PROOFSTEP]
have h₂ : ∀ f : X ⟶ Y, biprod.desc (0 : X ⟶ Y) f = biprod.snd ≫ f :=
  by
  intro f
  ext
  · aesop_cat
  · simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
[PROOFSTEP]
intro f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.desc 0 f = biprod.snd ≫ f
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.inl ≫ biprod.desc 0 f = biprod.inl ≫ biprod.snd ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.inr ≫ biprod.desc 0 f = biprod.inr ≫ biprod.snd ≫ f
[PROOFSTEP]
simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
⊢ EckmannHilton.IsUnital (fun x x_1 => rightAdd X Y x x_1) 0
[PROOFSTEP]
have h₁ : ∀ f : X ⟶ Y, biprod.desc f (0 : X ⟶ Y) = biprod.fst ≫ f :=
  by
  intro f
  ext
  · aesop_cat
  · simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
⊢ ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
[PROOFSTEP]
intro f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
f : X ⟶ Y
⊢ biprod.desc f 0 = biprod.fst ≫ f
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
f : X ⟶ Y
⊢ biprod.inl ≫ biprod.desc f 0 = biprod.inl ≫ biprod.fst ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
f : X ⟶ Y
⊢ biprod.inr ≫ biprod.desc f 0 = biprod.inr ≫ biprod.fst ≫ f
[PROOFSTEP]
simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
⊢ EckmannHilton.IsUnital (fun x x_1 => rightAdd X Y x x_1) 0
[PROOFSTEP]
exact
  ⟨⟨fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp]⟩,
    ⟨fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]⟩⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
f : X ⟶ Y
⊢ rightAdd X Y 0 f = f
[PROOFSTEP]
simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
f : X ⟶ Y
⊢ rightAdd X Y f 0 = f
[PROOFSTEP]
simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
let diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
have hd₁ : biprod.inl ≫ diag = biprod.lift f h := by ext <;> simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ biprod.inl ≫ diag = biprod.lift f h
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ (biprod.inl ≫ diag) ≫ biprod.fst = biprod.lift f h ≫ biprod.fst
[PROOFSTEP]
simp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ (biprod.inl ≫ diag) ≫ biprod.snd = biprod.lift f h ≫ biprod.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
have hd₂ : biprod.inr ≫ diag = biprod.lift g k := by ext <;> simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ biprod.inr ≫ diag = biprod.lift g k
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ (biprod.inr ≫ diag) ≫ biprod.fst = biprod.lift g k ≫ biprod.fst
[PROOFSTEP]
simp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ (biprod.inr ≫ diag) ≫ biprod.snd = biprod.lift g k ≫ biprod.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
have h₁ : biprod.lift (f +ᵣ g) (h +ᵣ k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag := by ext <;> aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) ≫ biprod.fst = (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.fst
[PROOFSTEP]
aesop_cat
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) ≫ biprod.snd = (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.snd
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
have h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (f +ₗ h) (g +ₗ k) := by
  ext <;> simp [reassoc_of% hd₁, reassoc_of% hd₂]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ biprod.inl ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.inl ≫ biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
simp [reassoc_of% hd₁, reassoc_of% hd₂]
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ biprod.inr ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.inr ≫ biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
simp [reassoc_of% hd₁, reassoc_of% hd₂]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
[PROOFSTEP]
rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
[PROOFSTEP]
simp only [add_eq_right_addition, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g ≫ h = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc (f ≫ h) (g ≫ h)
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.desc f g ≫ h = biprod.desc (f ≫ h) (g ≫ h)
[PROOFSTEP]
ext
[GOAL]
case e_a.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.inl ≫ biprod.desc f g ≫ h = biprod.inl ≫ biprod.desc (f ≫ h) (g ≫ h)
[PROOFSTEP]
simp
[GOAL]
case e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ biprod.inr ≫ biprod.desc f g ≫ h = biprod.inr ≫ biprod.desc (f ≫ h) (g ≫ h)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
[PROOFSTEP]
simp only [add_eq_left_addition, ← Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ (f ≫ biprod.lift g h) ≫ biprod.desc (𝟙 Z) (𝟙 Z) = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.desc (𝟙 Z) (𝟙 Z)
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ biprod.lift g h = biprod.lift (f ≫ g) (f ≫ h)
[PROOFSTEP]
ext
[GOAL]
case e_a.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ (f ≫ biprod.lift g h) ≫ biprod.fst = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.fst
[PROOFSTEP]
simp
[GOAL]
case e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ (f ≫ biprod.lift g h) ≫ biprod.snd = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.snd
[PROOFSTEP]
simp


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
[PROOFSTEP]
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (yoneda.obj J) ↔ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
[PROOFSTEP]
refine' ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGroupCat)).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : Functor.PreservesEpimorphisms (preadditiveYoneda.obj J ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J) → Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
⊢ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (yoneda.obj J) ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
refine' ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : Functor.PreservesEpimorphisms (preadditiveYonedaObj J ⋙ forget (ModuleCat (End J)))
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J) → Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P)) ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
refine' ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P)) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P)) → Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P)) ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
refine' ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P)) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P)) → Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
⊢ AddCommGroup (End X)
[PROOFSTEP]
dsimp [End]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
⊢ AddCommGroup (X ⟶ X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ (fun g => f ≫ g) (g + g') = (fun g => f ≫ g) g + (fun g => f ≫ g) g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
g : Q ⟶ R
f f' : P ⟶ Q
⊢ (fun f => f ≫ g) (f + f') = (fun f => f ≫ g) f + (fun f => f ≫ g) f'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f f' : P ⟶ Q
g g' : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : (-f) ≫ g = (-f) ≫ g'
⊢ g = g'
[PROOFSTEP]
rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
⊢ g = g'
[PROOFSTEP]
rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ 0 * f = 0
[PROOFSTEP]
dsimp [mul]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ f ≫ 0 = 0
[PROOFSTEP]
exact HasZeroMorphisms.comp_zero f _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ f * 0 = 0
[PROOFSTEP]
dsimp [mul]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ 0 ≫ f = 0
[PROOFSTEP]
exact HasZeroMorphisms.zero_comp _ f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g✝ g' : Q ⟶ R
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ g = 0
[PROOFSTEP]
rw [← kernel.lift_ι f g h, w, Limits.comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g✝ g' : Q ⟶ R
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0
[PROOFSTEP]
rw [← cokernel.π_desc f g h, w, Limits.zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f f' : P ⟶ Q
g g' : Q ⟶ R
inst✝ : IsIso f
⊢ f ≫ g = 0 ↔ g = 0
[PROOFSTEP]
rw [← IsIso.eq_inv_comp, Limits.comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f f' : P ⟶ Q
g g' : Q ⟶ R
inst✝ : IsIso g
⊢ f ≫ g = 0 ↔ f = 0
[PROOFSTEP]
rw [← IsIso.eq_comp_inv, Limits.zero_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g
[PROOFSTEP]
rw [← sub_eq_zero, ← comp_sub, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ Fork.ι c ≫ (f - g) = Fork.ι c ≫ 0
[PROOFSTEP]
rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (forkOfKernelFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (forkOfKernelFork c) = Fork.ι s
⊢ m✝ = IsLimit.lift i (kernelForkOfFork s)
[PROOFSTEP]
apply Fork.IsLimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (forkOfKernelFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (forkOfKernelFork c) = Fork.ι s
⊢ m✝ ≫ Fork.ι c = IsLimit.lift i (kernelForkOfFork s) ≫ Fork.ι c
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (kernelForkOfFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = Fork.ι s
⊢ m✝ = IsLimit.lift i (forkOfKernelFork s)
[PROOFSTEP]
apply Fork.IsLimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (kernelForkOfFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = Fork.ι s
⊢ m✝ ≫ Fork.ι c = IsLimit.lift i (forkOfKernelFork s) ≫ Fork.ι c
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c
[PROOFSTEP]
rw [← sub_eq_zero, ← sub_comp, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ (f - g) ≫ Cofork.π c = 0 ≫ Cofork.π c
[PROOFSTEP]
rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj (coforkOfCokernelCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coforkOfCokernelCofork c) ≫ m✝ = Cofork.π s
⊢ m✝ = IsColimit.desc i (cokernelCoforkOfCofork s)
[PROOFSTEP]
apply Cofork.IsColimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj (coforkOfCokernelCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coforkOfCokernelCofork c) ≫ m✝ = Cofork.π s
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ IsColimit.desc i (cokernelCoforkOfCofork s)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj (cokernelCoforkOfCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = Cofork.π s
⊢ m✝ = IsColimit.desc i (coforkOfCokernelCofork s)
[PROOFSTEP]
apply Cofork.IsColimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj (cokernelCoforkOfCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = Cofork.π s
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ IsColimit.desc i (coforkOfCokernelCofork s)
[PROOFSTEP]
aesop_cat