[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ HasKernel f
[PROOFSTEP]
have := NatIso.naturality_1 i f
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : NatTrans.app i.inv X✝ ≫ (F ⋙ G).map f ≫ NatTrans.app i.hom Y✝ = (𝟭 C).map f
⊢ HasKernel f
[PROOFSTEP]
simp at this
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasKernel f
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasKernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
this : HasKernel (G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
⊢ HasKernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
apply Limits.hasKernel_iso_comp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ HasCokernel f
[PROOFSTEP]
have : PreservesColimits G := adj.leftAdjointPreservesColimits
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : PreservesColimits G
⊢ HasCokernel f
[PROOFSTEP]
have := NatIso.naturality_1 i f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : NatTrans.app i.inv X✝ ≫ (F ⋙ G).map f ≫ NatTrans.app i.hom Y✝ = (𝟭 C).map f
⊢ HasCokernel f
[PROOFSTEP]
simp at this
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasCokernel f
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasCokernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝¹ : PreservesColimits G
this✝ : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
this : HasCokernel (G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
⊢ HasCokernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
apply Limits.hasCokernel_epi_comp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ G.obj (cokernel (F.map f)) ≅ cokernel f
[PROOFSTEP]
have : PreservesColimits G := adj.leftAdjointPreservesColimits
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ G.obj (cokernel (F.map f)) ≅ cokernel f
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ G.obj (cokernel (F.map f)) ≅ cokernel f
[PROOFSTEP]
calc
  G.obj (cokernel (F.map f)) ≅ cokernel (G.map (F.map f)) := (asIso (cokernelComparison _ G)).symm
  _ ≅ cokernel (i.hom.app X ≫ f ≫ i.inv.app Y) := (cokernelIsoOfEq (NatIso.naturality_2 i f).symm)
  _ ≅ cokernel (f ≫ i.inv.app Y) := (cokernelEpiComp (i.hom.app X) (f ≫ i.inv.app Y))
  _ ≅ cokernel f := cokernelCompIsIso f (i.inv.app Y)
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
⊢ kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π f)
[PROOFSTEP]
have : PreservesColimits G := adj.leftAdjointPreservesColimits
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π f)
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π f)
[PROOFSTEP]
calc
  kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G) :=
    kernelIsoOfEq (π_comp_cokernelComparison _ _).symm
  _ ≅ kernel (cokernel.π (G.map (F.map f))) := (kernelCompMono _ _)
  _ ≅ kernel (cokernel.π (_ ≫ f ≫ _) ≫ (cokernelIsoOfEq _).hom) :=
    (kernelIsoOfEq (π_comp_cokernelIsoOfEq_hom (NatIso.naturality_2 i f)).symm)
  _ ≅ kernel (cokernel.π (_ ≫ f ≫ _)) := (kernelCompMono _ _)
  _ ≅ kernel (cokernel.π (f ≫ i.inv.app Y) ≫ (cokernelEpiComp (i.hom.app X) _).inv) :=
    (kernelIsoOfEq (by simp only [cokernel.π_desc, cokernelEpiComp_inv]))
  _ ≅ kernel (cokernel.π (f ≫ _)) := (kernelCompMono _ _)
  _ ≅ kernel (inv (i.inv.app Y) ≫ cokernel.π f ≫ (cokernelCompIsIso f (i.inv.app Y)).inv) :=
    (kernelIsoOfEq
      (by simp only [cokernel.π_desc, cokernelCompIsIso_inv, Iso.hom_inv_id_app_assoc, NatIso.inv_inv_app]))
  _ ≅ kernel (cokernel.π f ≫ _) := (kernelIsIsoComp _ _)
  _ ≅ kernel (cokernel.π f) := kernelCompMono _ _
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
    cokernel.π (f ≫ NatTrans.app i.inv Y) ≫ (cokernelEpiComp (NatTrans.app i.hom X) (f ≫ NatTrans.app i.inv Y)).inv
[PROOFSTEP]
simp only [cokernel.π_desc, cokernelEpiComp_inv]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ cokernel.π (f ≫ NatTrans.app i.inv Y) =
    inv (NatTrans.app i.inv Y) ≫ cokernel.π f ≫ (cokernelCompIsIso f (NatTrans.app i.inv Y)).inv
[PROOFSTEP]
simp only [cokernel.π_desc, cokernelCompIsIso_inv, Iso.hom_inv_id_app_assoc, NatIso.inv_inv_app]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
⊢ Abelian.coimage f ≅ Abelian.image f
[PROOFSTEP]
have : PreservesLimits F := adj.rightAdjointPreservesLimits
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this : PreservesLimits F
⊢ Abelian.coimage f ≅ Abelian.image f
[PROOFSTEP]
haveI : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝ : PreservesLimits F
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
⊢ Abelian.coimage f ≅ Abelian.image f
[PROOFSTEP]
calc
  Abelian.coimage f ≅ cokernel (kernel.ι f) := Iso.refl _
  _ ≅ G.obj (cokernel (F.map (kernel.ι f))) := (cokernelIso _ _ i adj _).symm
  _ ≅ G.obj (cokernel (kernelComparison f F ≫ kernel.ι (F.map f))) := (G.mapIso (cokernelIsoOfEq (by simp)))
  _ ≅ G.obj (cokernel (kernel.ι (F.map f))) := (G.mapIso (cokernelEpiComp _ _))
  _ ≅ G.obj (Abelian.coimage (F.map f)) := (Iso.refl _)
  _ ≅ G.obj (Abelian.image (F.map f)) := (G.mapIso (Abelian.coimageIsoImage _))
  _ ≅ G.obj (kernel (cokernel.π (F.map f))) := (Iso.refl _)
  _ ≅ kernel (G.map (cokernel.π (F.map f))) := (PreservesKernel.iso _ _)
  _ ≅ kernel (cokernel.π f) := (coimageIsoImageAux F G i adj f)
  _ ≅ Abelian.image f := Iso.refl _
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝ : PreservesLimits F
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
⊢ F.map (kernel.ι f) = kernelComparison f F ≫ kernel.ι (F.map f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝¹ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this✝ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasKernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝² : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this✝¹ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
this✝ : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasKernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
dsimp only [coimageIsoImage, Iso.instTransIso_trans, Iso.refl, Iso.trans, Iso.symm, Functor.mapIso, cokernelEpiComp,
  cokernelIso, cokernelCompIsIso_inv, asIso, coimageIsoImageAux, kernelCompMono]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝² : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this✝¹ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
this✝ : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasKernel f'
⊢ ((((((((𝟙 (Abelian.coimage f) ≫
                      cokernel.desc (kernel.ι f) (NatTrans.app i.inv X ≫ cokernel.π (kernel.ι f ≫ NatTrans.app i.inv X))
                          (_ : kernel.ι f ≫ NatTrans.app i.inv X ≫ cokernel.π (kernel.ι f ≫ NatTrans.app i.inv X) = 0) ≫
                        cokernel.desc (kernel.ι f ≫ NatTrans.app i.inv X)
                            (cokernel.π (NatTrans.app i.hom (kernel f) ≫ kernel.ι f ≫ NatTrans.app i.inv X))
                            (_ :
                              (kernel.ι f ≫ NatTrans.app i.inv X) ≫
                                  cokernel.π (NatTrans.app i.hom (kernel f) ≫ kernel.ι f ≫ NatTrans.app i.inv X) =
                                0) ≫
                          (cokernelIsoOfEq
                                (_ :
                                  (F ⋙ G).map (kernel.ι f) =
                                    NatTrans.app i.hom (kernel f) ≫
                                      (𝟭 C).map (kernel.ι f) ≫ NatTrans.app i.inv X)).inv ≫
                            cokernelComparison (F.map (kernel.ι f)) G) ≫
                    G.map (cokernelIsoOfEq (_ : F.map (kernel.ι f) = kernelComparison f F ≫ kernel.ι (F.map f))).hom) ≫
                  G.map
                    (cokernel.desc (kernelComparison f F ≫ kernel.ι (F.map f)) (cokernel.π (kernel.ι (F.map f)))
                      (_ : (kernelComparison f F ≫ kernel.ι (F.map f)) ≫ cokernel.π (kernel.ι (F.map f)) = 0))) ≫
                𝟙 (G.obj (cokernel (kernel.ι (F.map f))))) ≫
              G.map (Abelian.coimageIsoImage (F.map f)).hom) ≫
            𝟙 (G.obj (Abelian.image (F.map f)))) ≫
          (PreservesKernel.iso G (cokernel.π (F.map f))).hom) ≫
        ((((((((kernelIsoOfEq
                            (_ :
                              G.map (cokernel.π (F.map f)) =
                                cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G)).hom ≫
                        kernel.lift (cokernel.π (G.map (F.map f)))
                          (kernel.ι (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G))
                          (_ :
                            kernel.ι (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G) ≫
                                cokernel.π (G.map (F.map f)) =
                              0)) ≫
                      (kernelIsoOfEq
                          (_ :
                            cokernel.π ((F ⋙ G).map f) =
                              cokernel.π (NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y) ≫
                                (cokernelIsoOfEq
                                    (_ :
                                      NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y =
                                        (F ⋙ G).map f)).hom)).hom) ≫
                    kernel.lift (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                      (kernel.ι
                        (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) ≫
                          (cokernelIsoOfEq
                              (_ : NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y = (F ⋙ G).map f)).hom))
                      (_ :
                        kernel.ι
                              (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) ≫
                                (cokernelIsoOfEq
                                    (_ :
                                      NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y = (F ⋙ G).map f)).hom) ≫
                            cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                          0)) ≫
                  (kernelIsoOfEq
                      (_ :
                        cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                          cokernel.π (f ≫ NatTrans.app i.inv Y) ≫
                            cokernel.desc (f ≫ NatTrans.app i.inv Y)
                              (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                              (_ :
                                (f ≫ NatTrans.app i.inv Y) ≫
                                    cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                                  0))).hom) ≫
                kernel.lift (cokernel.π (f ≫ NatTrans.app i.inv Y))
                  (kernel.ι
                    (cokernel.π (f ≫ NatTrans.app i.inv Y) ≫
                      cokernel.desc (f ≫ NatTrans.app i.inv Y)
                        (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                        (_ :
                          (f ≫ NatTrans.app i.inv Y) ≫ cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                            0)))
                  (_ :
                    kernel.ι
                          (cokernel.π (f ≫ NatTrans.app i.inv Y) ≫
                            cokernel.desc (f ≫ NatTrans.app i.inv Y)
                              (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                              (_ :
                                (f ≫ NatTrans.app i.inv Y) ≫
                                    cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                                  0)) ≫
                        cokernel.π (f ≫ NatTrans.app i.inv Y) =
                      0)) ≫
              (kernelIsoOfEq
                  (_ :
                    cokernel.π (f ≫ NatTrans.app i.inv Y) =
                      inv (NatTrans.app i.inv Y) ≫
                        cokernel.π f ≫
                          cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                            (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0))).hom) ≫
            (kernelIsIsoComp (inv (NatTrans.app i.inv Y))
                (cokernel.π f ≫
                  cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                    (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0))).hom) ≫
          kernel.lift (cokernel.π f)
            (kernel.ι
              (cokernel.π f ≫
                cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                  (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0)))
            (_ :
              kernel.ι
                    (cokernel.π f ≫
                      cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                        (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0)) ≫
                  cokernel.π f =
                0)) ≫
      𝟙 (kernel (cokernel.π f)) =
    Abelian.coimageImageComparison f
[PROOFSTEP]
simpa only [← cancel_mono (Abelian.image.ι f), ← cancel_epi (Abelian.coimage.π f), Category.assoc, Category.id_comp,
  cokernel.π_desc_assoc, π_comp_cokernelIsoOfEq_inv_assoc, PreservesKernel.iso_hom, π_comp_cokernelComparison_assoc, ←
  G.map_comp_assoc, kernel.lift_ι, Abelian.coimage_image_factorisation, lift_comp_kernelIsoOfEq_hom_assoc,
  kernelIsIsoComp_hom, kernel.lift_ι_assoc, kernelIsoOfEq_hom_comp_ι_assoc, kernelComparison_comp_ι_assoc,
  π_comp_cokernelIsoOfEq_hom_assoc, asIso_hom, NatIso.inv_inv_app] using NatIso.naturality_1 i f
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
⊢ Abelian C
[PROOFSTEP]
haveI := hasKernels F G i
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this : HasKernels C
⊢ Abelian C
[PROOFSTEP]
haveI := hasCokernels F G i adj
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
⊢ Abelian C
[PROOFSTEP]
have : ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f) :=
  by
  intro X Y f
  rw [← coimageIsoImage_hom F G i adj f]
  infer_instance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
⊢ ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f)
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ IsIso (Abelian.coimageImageComparison f)
[PROOFSTEP]
rw [← coimageIsoImage_hom F G i adj f]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ IsIso (coimageIsoImage F G i adj f).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝¹ : HasKernels C
this✝ : HasCokernels C
this : ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f)
⊢ Abelian C
[PROOFSTEP]
apply Abelian.ofCoimageImageComparisonIsIso


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
src✝ : Mon_ C := Mon_.trivial C
⊢ (β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
      (Mon_.mk src✝.X src✝.one src✝.mul).mul =
    (Mon_.mk src✝.X src✝.one src✝.mul).mul
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
src✝ : Mon_ C := Mon_.trivial C
⊢ (β_ (𝟙_ C) (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom = (λ_ (𝟙_ C)).hom
[PROOFSTEP]
rw [braiding_leftUnitor, unitors_equal]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
⊢ (β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
      (Mon_.mk src✝.X src✝.one src✝.mul).mul =
    (Mon_.mk src✝.X src✝.one src✝.mul).mul
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
⊢ (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul =
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul
[PROOFSTEP]
have := F.braided
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
⊢ (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul =
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul
[PROOFSTEP]
slice_lhs 1 2 => rw [← this]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map A.mul
[PROOFSTEP]
rw [← this]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map A.mul
[PROOFSTEP]
rw [← this]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map A.mul
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map (β_ A.X A.X).hom) ≫ F.map A.mul =
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul
[PROOFSTEP]
slice_lhs 2 3 => rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map (β_ A.X A.X).hom ≫ F.map A.mul
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
[PROOFSTEP]
rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map (β_ A.X A.X).hom ≫ F.map A.mul
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
[PROOFSTEP]
rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map (β_ A.X A.X).hom ≫ F.map A.mul
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
[PROOFSTEP]
rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
X✝ Y✝ : LaxBraidedFunctor C D
α : X✝ ⟶ Y✝
⊢ ∀ ⦃X Y : CommMon_ C⦄ (f : X ⟶ Y),
    (mapCommMon X✝).map f ≫ (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) Y =
      (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) X ≫ (mapCommMon Y✝).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
X✝¹ Y✝¹ : LaxBraidedFunctor C D
α : X✝¹ ⟶ Y✝¹
X✝ Y✝ : CommMon_ C
f✝ : X✝ ⟶ Y✝
⊢ (mapCommMon X✝¹).map f✝ ≫ (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) Y✝ =
    (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) X✝ ≫ (mapCommMon Y✝¹).map f✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
X✝¹ Y✝¹ : LaxBraidedFunctor C D
α : X✝¹ ⟶ Y✝¹
X✝ Y✝ : CommMon_ C
f✝ : X✝ ⟶ Y✝
⊢ ((mapCommMon X✝¹).map f✝ ≫ (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) Y✝).hom =
    ((fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) X✝ ≫ (mapCommMon Y✝¹).map f✝).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommMon_ C
f : X✝ ⟶ Y✝
x✝² x✝¹ : Discrete PUnit
x✝ : x✝² ⟶ x✝¹
⊢ ((fun A =>
              LaxBraidedFunctor.mk
                (LaxMonoidalFunctor.mk
                  (CategoryTheory.Functor.mk { obj := fun x => A.X, map := fun {X Y} x => 𝟙 ((fun x => A.X) X) }) A.one
                  fun x x => A.mul))
            X✝).map
        x✝ ≫
      (fun x => f.hom) x✝¹ =
    (fun x => f.hom) x✝² ≫
      ((fun A =>
              LaxBraidedFunctor.mk
                (LaxMonoidalFunctor.mk
                  (CategoryTheory.Functor.mk { obj := fun x => A.X, map := fun {X Y} x => 𝟙 ((fun x => A.X) X) }) A.one
                  fun x x => A.mul))
            Y✝).map
        x✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommMon_ C
f : X✝ ⟶ Y✝
x✝² x✝¹ : Discrete PUnit
x✝ : x✝² ⟶ x✝¹
⊢ 𝟙 X✝.X ≫ f.hom = f.hom ≫ 𝟙 Y✝.X
[PROOFSTEP]
rw [Category.id_comp, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
x✝ : Discrete PUnit
⊢ x✝ = (trivial (Discrete PUnit)).toMon_.X
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
⊢ ∀ {X Y : Discrete PUnit} (f : X ⟶ Y),
    ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).map f ≫
        ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) Y).hom =
      ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) X).hom ≫
        ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).map f
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ f
[GOAL]
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
as✝¹ as✝ : PUnit
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).map f ≫
      ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) { as := as✝ }).hom =
    ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) { as := as✝¹ }).hom ≫
      ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
⊢ ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).ε ≫
      ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) (𝟙_ (Discrete PUnit))).hom =
    ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).ε
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
⊢ ∀ (X Y : Discrete PUnit),
    LaxMonoidalFunctor.μ ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).toLaxMonoidalFunctor X Y ≫
        ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) (X ⊗ Y)).hom =
      (((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) X).hom ⊗
          ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) Y).hom) ≫
        LaxMonoidalFunctor.μ ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).toLaxMonoidalFunctor X Y
[PROOFSTEP]
aesop_cat


[GOAL]
⊢ Inhabited RelCat
[PROOFSTEP]
unfold RelCat
[GOAL]
⊢ Inhabited (Type ?u.6)
[PROOFSTEP]
infer_instance


[GOAL]
X✝ Y✝ : Grpd
x✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
X✝ Y✝ : Grpd
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ 𝟙 Y✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {W X Y Z : Grpd} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
W✝ X✝ Y✝ Z✝ : Grpd
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
rfl
[GOAL]
J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (j : J),
    (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
[PROOFSTEP]
intros
[GOAL]
J : Type u
F : J → Grpd
s✝ : Limits.Fan F
j✝ : J
⊢ (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s✝ ≫ Limits.Fan.proj (piLimitFan F) j✝ = Limits.Fan.proj s✝ j✝
[PROOFSTEP]
dsimp only [piLimitFan]
[GOAL]
J : Type u
F : J → Grpd
s✝ : Limits.Fan F
j✝ : J
⊢ (Functor.pi' fun j => Limits.Fan.proj s✝ j) ≫
      Limits.Fan.proj (Limits.Fan.mk (of ((j : J) → ↑(F j))) fun j => Pi.eval (fun j => ↑(F j)) j) j✝ =
    Limits.Fan.proj s✝ j✝
[PROOFSTEP]
simp [hom_to_functor]
[GOAL]
J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (m : s.pt ⟶ (piLimitFan F).pt),
    (∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j) →
      m = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s
[PROOFSTEP]
intro s m w
[GOAL]
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
⊢ m = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s
[PROOFSTEP]
apply Functor.pi_ext
[GOAL]
case h
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
⊢ ∀ (i : J),
    m ⋙ Pi.eval (fun i => ↑(F i)) i =
      (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ⋙ Pi.eval (fun i => ↑(F i)) i
[PROOFSTEP]
intro j
[GOAL]
case h
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
j : J
⊢ m ⋙ Pi.eval (fun i => ↑(F i)) j = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ⋙ Pi.eval (fun i => ↑(F i)) j
[PROOFSTEP]
specialize w j
[GOAL]
case h
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
j : J
w : m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
⊢ m ⋙ Pi.eval (fun i => ↑(F i)) j = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ⋙ Pi.eval (fun i => ↑(F i)) j
[PROOFSTEP]
simpa
[GOAL]
⊢ {J : Type ?u.17117} → (f : J → Grpd) → Limits.Fan f
[PROOFSTEP]
apply piLimitFan
[GOAL]
⊢ {J : Type u} → (f : J → Grpd) → Limits.IsLimit (piLimitFan f)
[PROOFSTEP]
apply piLimitFanIsLimit
[GOAL]
J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i => ↑(f i)) j
[PROOFSTEP]
simp [piIsoPi]
[GOAL]
J : Type u
f : J → Grpd
j : J
⊢ NatTrans.app (piLimitFan f).π { as := j } = Pi.eval (fun i => ↑(f i)) j
[PROOFSTEP]
rfl