[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ NatTrans.app (ofRightAdjoint i).unit (i.obj ((leftAdjoint i).obj X)) =
    i.map ((leftAdjoint i).map (NatTrans.app (ofRightAdjoint i).unit X))
[PROOFSTEP]
rw [← cancel_mono (i.map ((ofRightAdjoint i).counit.app ((leftAdjoint i).obj X))), ← i.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ NatTrans.app (ofRightAdjoint i).unit (i.obj ((leftAdjoint i).obj X)) ≫
      i.map (NatTrans.app (ofRightAdjoint i).counit ((leftAdjoint i).obj X)) =
    i.map
      ((leftAdjoint i).map (NatTrans.app (ofRightAdjoint i).unit X) ≫
        NatTrans.app (ofRightAdjoint i).counit ((leftAdjoint i).obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
B : D
⊢ IsIso (NatTrans.app (ofRightAdjoint i).unit (i.obj B))
[PROOFSTEP]
have : (ofRightAdjoint i).unit.app (i.obj B) = inv (i.map ((ofRightAdjoint i).counit.app B)) :=
  by
  rw [← comp_hom_eq_id]
  apply (ofRightAdjoint i).right_triangle_components
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
B : D
⊢ NatTrans.app (ofRightAdjoint i).unit (i.obj B) = inv (i.map (NatTrans.app (ofRightAdjoint i).counit B))
[PROOFSTEP]
rw [← comp_hom_eq_id]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
B : D
⊢ NatTrans.app (ofRightAdjoint i).unit (i.obj B) ≫ i.map (NatTrans.app (ofRightAdjoint i).counit B) =
    𝟙 ((𝟭 C).obj (i.obj B))
[PROOFSTEP]
apply (ofRightAdjoint i).right_triangle_components
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
B : D
this : NatTrans.app (ofRightAdjoint i).unit (i.obj B) = inv (i.map (NatTrans.app (ofRightAdjoint i).counit B))
⊢ IsIso (NatTrans.app (ofRightAdjoint i).unit (i.obj B))
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
B : D
this : NatTrans.app (ofRightAdjoint i).unit (i.obj B) = inv (i.map (NatTrans.app (ofRightAdjoint i).counit B))
⊢ IsIso (inv (i.map (NatTrans.app (ofRightAdjoint i).counit B)))
[PROOFSTEP]
exact IsIso.inv_isIso
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ IsIso (NatTrans.app (ofRightAdjoint i).unit A)
[PROOFSTEP]
suffices
  (ofRightAdjoint i).unit.app A =
    h.getIso.inv ≫
      (ofRightAdjoint i).unit.app (i.obj (Functor.essImage.witness h)) ≫ (leftAdjoint i ⋙ i).map h.getIso.hom
  by
  rw [this]
  infer_instance
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
this :
  NatTrans.app (ofRightAdjoint i).unit A =
    (getIso h).inv ≫ NatTrans.app (ofRightAdjoint i).unit (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
⊢ IsIso (NatTrans.app (ofRightAdjoint i).unit A)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
this :
  NatTrans.app (ofRightAdjoint i).unit A =
    (getIso h).inv ≫ NatTrans.app (ofRightAdjoint i).unit (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
⊢ IsIso
    ((getIso h).inv ≫ NatTrans.app (ofRightAdjoint i).unit (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ NatTrans.app (ofRightAdjoint i).unit A =
    (getIso h).inv ≫ NatTrans.app (ofRightAdjoint i).unit (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ NatTrans.app (ofRightAdjoint i).unit A =
    (getIso h).inv ≫ (𝟭 C).map (getIso h).hom ≫ NatTrans.app (ofRightAdjoint i).unit A
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
⊢ A ∈ Functor.essImage i
[PROOFSTEP]
let η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
⊢ A ∈ Functor.essImage i
[PROOFSTEP]
haveI : IsIso (η.app (i.obj ((leftAdjoint i).obj A))) := Functor.essImage.unit_isIso ((i.obj_mem_essImage _))
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
⊢ A ∈ Functor.essImage i
[PROOFSTEP]
have : Epi (η.app A) := by
  refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_
  rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
  apply epi_comp (η.app (i.obj ((leftAdjoint i).obj A)))
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (NatTrans.app η A)
[PROOFSTEP]
refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.app A) ?_
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (retraction (NatTrans.app η A) ≫ NatTrans.app η A)
[PROOFSTEP]
rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (NatTrans.app η ((leftAdjoint i ⋙ i).obj A) ≫ (leftAdjoint i ⋙ i).map (retraction (NatTrans.app η A)))
[PROOFSTEP]
apply epi_comp (η.app (i.obj ((leftAdjoint i).obj A)))
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝ : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
this : Epi (NatTrans.app η A)
⊢ A ∈ Functor.essImage i
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝ : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
this : Epi (NatTrans.app η A)
⊢ A ∈ Functor.essImage i
[PROOFSTEP]
haveI := isIso_of_epi_of_isSplitMono (η.app A)
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} E
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono (NatTrans.app (ofRightAdjoint i).unit A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝¹ : IsIso (NatTrans.app η (i.obj ((leftAdjoint i).obj A)))
this✝ : Epi (NatTrans.app η A)
this : IsIso (NatTrans.app η A)
⊢ A ∈ Functor.essImage i
[PROOFSTEP]
exact mem_essImage_of_unit_isIso A
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A : C
B : D
f : i.obj ((leftAdjoint i).obj A) ⟶ i.obj B
⊢ ↑(unitCompPartialBijectiveAux A B).symm f = NatTrans.app (ofRightAdjoint i).unit A ≫ f
[PROOFSTEP]
simp [unitCompPartialBijectiveAux]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A B : C
hB : B ∈ Functor.essImage i
f : i.obj ((leftAdjoint i).obj A) ⟶ B
⊢ ↑(unitCompPartialBijective A hB).symm f = NatTrans.app (ofRightAdjoint i).unit A ≫ f
[PROOFSTEP]
simp [unitCompPartialBijective, unitCompPartialBijectiveAux_symm_apply]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : B ∈ Functor.essImage i
hB' : B' ∈ Functor.essImage i
f : i.obj ((leftAdjoint i).obj A) ⟶ B
⊢ ↑(unitCompPartialBijective A hB').symm (f ≫ h) = ↑(unitCompPartialBijective A hB).symm f ≫ h
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : B ∈ Functor.essImage i
hB' : B' ∈ Functor.essImage i
f : A ⟶ B
⊢ ↑(unitCompPartialBijective A hB') (f ≫ h) = ↑(unitCompPartialBijective A hB) f ≫ h
[PROOFSTEP]
rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : Functor.EssImageSubcategory i
⊢ ((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).obj X ≅ X
[PROOFSTEP]
refine' Iso.symm (@asIso _ _ X _ ((ofRightAdjoint i).unit.app X.obj) ?_)
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : Functor.EssImageSubcategory i
⊢ IsIso (NatTrans.app (ofRightAdjoint i).unit X.obj)
[PROOFSTEP]
refine @isIso_of_reflects_iso _ _ _ _ _ _ _ i.essImageInclusion ?_ _
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : Functor.EssImageSubcategory i
⊢ IsIso ((Functor.essImageInclusion i).map (NatTrans.app (ofRightAdjoint i).unit X.obj))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : Functor.EssImageSubcategory i
⊢ IsIso (NatTrans.app (ofRightAdjoint i).unit X.obj)
[PROOFSTEP]
exact inferInstance
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : Functor.EssImageSubcategory i
⊢ (Functor.essImageInclusion i).map (equivEssImageOfReflective_counitIso_app X).hom =
    inv (NatTrans.app (ofRightAdjoint i).unit X.obj)
[PROOFSTEP]
simp [equivEssImageOfReflective_counitIso_app, asIso]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : Functor.EssImageSubcategory i
⊢ inv (NatTrans.app (ofRightAdjoint i).unit X.obj) = inv (NatTrans.app (ofRightAdjoint i).unit X.obj)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
⊢ ∀ {X Y : D} (f : X ⟶ Y),
    (𝟭 D).map f ≫ ((fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm) Y).hom =
      ((fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm) X).hom ≫
        (Functor.toEssImage i ⋙ Functor.essImageInclusion i ⋙ leftAdjoint i).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : D
f : X ⟶ Y
⊢ (𝟭 D).map f ≫ ((fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm) Y).hom =
    ((fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm) X).hom ≫
      (Functor.toEssImage i ⋙ Functor.essImageInclusion i ⋙ leftAdjoint i).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : D
f : X ⟶ Y
⊢ f ≫ inv (NatTrans.app (ofRightAdjoint i).counit Y) =
    inv (NatTrans.app (ofRightAdjoint i).counit X) ≫ (leftAdjoint i).map (i.map f)
[PROOFSTEP]
rw [IsIso.comp_inv_eq, Category.assoc, IsIso.eq_inv_comp]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ofRightAdjoint i).counit X ≫ f =
    (leftAdjoint i).map (i.map f) ≫ NatTrans.app (ofRightAdjoint i).counit Y
[PROOFSTEP]
exact ((ofRightAdjoint i).counit.naturality f).symm
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
⊢ ∀ {X Y : Functor.EssImageSubcategory i} (f : X ⟶ Y),
    ((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).map f ≫
        (equivEssImageOfReflective_counitIso_app Y).hom =
      (equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 (Functor.EssImageSubcategory i)).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : Functor.EssImageSubcategory i
f : X ⟶ Y
⊢ ((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).map f ≫
      (equivEssImageOfReflective_counitIso_app Y).hom =
    (equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 (Functor.EssImageSubcategory i)).map f
[PROOFSTEP]
apply (Functor.essImageInclusion i).map_injective
[GOAL]
case a
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : Functor.EssImageSubcategory i
f : X ⟶ Y
⊢ (Functor.essImageInclusion i).map
      (((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).map f ≫
        (equivEssImageOfReflective_counitIso_app Y).hom) =
    (Functor.essImageInclusion i).map
      ((equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 (Functor.EssImageSubcategory i)).map f)
[PROOFSTEP]
have h := ((ofRightAdjoint i).unit.naturality f).symm
[GOAL]
case a
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : Functor.EssImageSubcategory i
f : X ⟶ Y
h :
  NatTrans.app (ofRightAdjoint i).unit X.obj ≫ (leftAdjoint i ⋙ i).map f =
    (𝟭 C).map f ≫ NatTrans.app (ofRightAdjoint i).unit Y.obj
⊢ (Functor.essImageInclusion i).map
      (((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).map f ≫
        (equivEssImageOfReflective_counitIso_app Y).hom) =
    (Functor.essImageInclusion i).map
      ((equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 (Functor.EssImageSubcategory i)).map f)
[PROOFSTEP]
rw [Functor.id_map] at h
[GOAL]
case a
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X Y : Functor.EssImageSubcategory i
f : X ⟶ Y
h :
  NatTrans.app (ofRightAdjoint i).unit X.obj ≫ (leftAdjoint i ⋙ i).map f =
    f ≫ NatTrans.app (ofRightAdjoint i).unit Y.obj
⊢ (Functor.essImageInclusion i).map
      (((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).map f ≫
        (equivEssImageOfReflective_counitIso_app Y).hom) =
    (Functor.essImageInclusion i).map
      ((equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 (Functor.EssImageSubcategory i)).map f)
[PROOFSTEP]
erw [Functor.map_comp, Functor.map_comp, equivEssImageOfReflective_map_counitIso_app_hom,
  equivEssImageOfReflective_map_counitIso_app_hom, IsIso.comp_inv_eq, assoc, ← h, IsIso.inv_hom_id_assoc,
  Functor.comp_map]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : D
⊢ (Functor.toEssImage i).map
        (NatTrans.app (NatIso.ofComponents fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm).hom X) ≫
      NatTrans.app (NatIso.ofComponents equivEssImageOfReflective_counitIso_app).hom ((Functor.toEssImage i).obj X) =
    𝟙 ((Functor.toEssImage i).obj X)
[PROOFSTEP]
apply (Functor.essImageInclusion i).map_injective
[GOAL]
case a
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : D
⊢ (Functor.essImageInclusion i).map
      ((Functor.toEssImage i).map
          (NatTrans.app (NatIso.ofComponents fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm).hom X) ≫
        NatTrans.app (NatIso.ofComponents equivEssImageOfReflective_counitIso_app).hom ((Functor.toEssImage i).obj X)) =
    (Functor.essImageInclusion i).map (𝟙 ((Functor.toEssImage i).obj X))
[PROOFSTEP]
erw [Functor.map_comp, equivEssImageOfReflective_map_counitIso_app_hom]
[GOAL]
case a
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
i : D ⥤ C
inst✝ : Reflective i
X : D
⊢ (Functor.essImageInclusion i).map
        ((Functor.toEssImage i).map
          (NatTrans.app (NatIso.ofComponents fun X => (asIso (NatTrans.app (ofRightAdjoint i).counit X)).symm).hom X)) ≫
      inv
        (NatTrans.app (ofRightAdjoint i).unit
          ((𝟭 (Functor.EssImageSubcategory i)).obj ((Functor.toEssImage i).obj X)).obj) =
    (Functor.essImageInclusion i).map (𝟙 ((Functor.toEssImage i).obj X))
[PROOFSTEP]
aesop_cat


[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ { l //
    Cofork.π
            (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
          l =
        Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ (NatTrans.app adj₁.counit X)
                      (_ :
                        F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                          NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π
                (Cofork.ofπ (NatTrans.app adj₁.counit X)
                  (_ :
                    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
              m =
            Cofork.π s →
          m = l }
[PROOFSTEP]
refine' ⟨(RegularEpi.desc' (adj₁.counit.app X) s.π _).1, _, _⟩
[GOAL]
case refine'_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← cancel_epi (adj₁.counit.app (RegularEpi.W (adj₁.counit.app X)))]
[GOAL]
case refine'_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.left ≫ Cofork.π s =
    NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← adj₁.counit_naturality_assoc RegularEpi.left]
[GOAL]
case refine'_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ F.map (U.map RegularEpi.left) ≫ NatTrans.app adj₁.counit ((U ⋙ F).obj X) ≫ Cofork.π s =
    NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
dsimp only [Functor.comp_obj]
[GOAL]
case refine'_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ F.map (U.map RegularEpi.left) ≫ NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ Cofork.π s =
    NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp, F.map_comp_assoc, s.condition, ←
  adj₁.counit_naturality_assoc RegularEpi.right]
[GOAL]
case refine'_2
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ Cofork.π
        (Cofork.ofπ (NatTrans.app adj₁.counit X)
          (_ :
            F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
              NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
      ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
          (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s)) =
    Cofork.π s
[PROOFSTEP]
apply (RegularEpi.desc' (adj₁.counit.app X) s.π _).2
[GOAL]
case refine'_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj
              (Cofork.ofπ (NatTrans.app adj₁.counit X)
                  (_ :
                    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
          WalkingParallelPair.one ⟶
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
    Cofork.π
            (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
          m =
        Cofork.π s →
      m =
        ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
            (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm :
  Cofork.π
        (Cofork.ofπ (NatTrans.app adj₁.counit X)
          (_ :
            F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
              NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
      m =
    Cofork.π s
⊢ m =
    ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
        (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
[PROOFSTEP]
rw [← cancel_epi (adj₁.counit.app X)]
[GOAL]
case refine'_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm :
  Cofork.π
        (Cofork.ofπ (NatTrans.app adj₁.counit X)
          (_ :
            F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
              NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
      m =
    Cofork.π s
⊢ NatTrans.app adj₁.counit X ≫ m =
    NatTrans.app adj₁.counit X ≫
      ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
          (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
[PROOFSTEP]
apply hm.trans (RegularEpi.desc' (adj₁.counit.app X) s.π _).2.symm
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (NatTrans.app adj₁.unit (U.obj X)) ≫ F'.map (U.map (NatTrans.app adj₁.counit X)) =
    𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
[PROOFSTEP]
rw [← F'.map_comp, adj₁.right_triangle_components]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
[PROOFSTEP]
apply F'.map_id
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (NatTrans.app adj₁.unit (U.obj X)) ≫ otherMap R F' adj₁ adj₂ X = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
[PROOFSTEP]
dsimp [otherMap]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (NatTrans.app adj₁.unit (U.obj X)) ≫
      F'.map
          (U.map
            (F.map (NatTrans.app adj₂.unit (U.toPrefunctor.1 X)) ≫
              NatTrans.app adj₁.counit (R.obj (F'.obj (U.toPrefunctor.1 X))))) ≫
        NatTrans.app adj₂.counit (F'.obj (U.toPrefunctor.1 X)) =
    𝟙 (F'.obj (U.obj X))
[PROOFSTEP]
rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc, adj₁.right_triangle_components, comp_id,
  adj₂.left_triangle_components]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ { f // F'.map (U.map (NatTrans.app adj₁.counit X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f } ≃
    { g // U.map (F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ g }
[PROOFSTEP]
apply (adj₂.homEquiv _ _).subtypeEquiv _
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ ∀ (a : F'.obj (U.obj X) ⟶ Y),
    F'.map (U.map (NatTrans.app adj₁.counit X)) ≫ a = otherMap R F' adj₁ adj₂ X ≫ a ↔
      U.map (F.map (↑(Adjunction.homEquiv adj₂ (U.obj X) Y) a) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
        U.map (NatTrans.app adj₁.counit X) ≫ ↑(Adjunction.homEquiv adj₂ (U.obj X) Y) a
[PROOFSTEP]
intro f
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ F'.map (U.map (NatTrans.app adj₁.counit X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f ↔
    U.map (F.map (↑(Adjunction.homEquiv adj₂ (U.obj X) Y) f) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
      U.map (NatTrans.app adj₁.counit X) ≫ ↑(Adjunction.homEquiv adj₂ (U.obj X) Y) f
[PROOFSTEP]
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left, otherMap, assoc,
  adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality, adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit,
  adj₂.right_triangle_components, comp_id, Functor.comp_map, ← U.map_comp, assoc, ← adj₁.counit_naturality,
  adj₂.homEquiv_unit, adj₂.homEquiv_unit, F.map_comp, assoc]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map
        (F.map (NatTrans.app adj₂.unit (U.toPrefunctor.1 X)) ≫
          F.map (U.map (R.map f)) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
      U.map (NatTrans.app adj₁.counit X) ≫ NatTrans.app adj₂.unit (U.obj ((𝟭 B).obj X)) ≫ (R ⋙ U).map f ↔
    U.map (F.map (NatTrans.app adj₂.unit (U.obj X)) ≫ F.map ((R ⋙ U).map f) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
      U.map (NatTrans.app adj₁.counit X) ≫ NatTrans.app adj₂.unit (U.obj X) ≫ (R ⋙ U).map f
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ { g // U.map (F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ g } ≃
    { z // F.map (U.map (NatTrans.app adj₁.counit X)) ≫ z = NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ z }
[PROOFSTEP]
apply (adj₁.homEquiv _ _).symm.subtypeEquiv
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ ∀ (a : U.obj X ⟶ U.obj (R.obj Y)),
    U.map (F.map a ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ a ↔
      F.map (U.map (NatTrans.app adj₁.counit X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm a =
        NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm a
[PROOFSTEP]
intro g
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ U.map (F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ g ↔
    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm g =
      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm g
[PROOFSTEP]
rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit, adj₁.homEquiv_counit, adj₁.homEquiv_counit,
  F.map_comp, assoc, U.map_comp, F.map_comp, assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ F.map g ≫ NatTrans.app adj₁.counit (R.obj Y) =
      F.map (U.map (NatTrans.app adj₁.counit X)) ≫ F.map g ≫ NatTrans.app adj₁.counit ((𝟭 B).obj (R.obj Y)) ↔
    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ F.map g ≫ NatTrans.app adj₁.counit (R.obj Y) =
      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)
[PROOFSTEP]
apply eq_comm
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
⊢ B ⥤ A
[PROOFSTEP]
refine' Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ Y X) _
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
⊢ ∀ (X : B) (Y Y' : A) (g : Y ⟶ Y') (h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y') (h ≫ g) =
      ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y) h ≫ R.map g
[PROOFSTEP]
intro X Y Y' g h
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y') (h ≫ g) =
    ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y) h ≫ R.map g
[PROOFSTEP]
rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply, Equiv.symm_apply_eq, Subtype.ext_iff]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ ↑{
        val :=
          F.map
              (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
                ↑(↑(Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                        Y')
                    (h ≫ g))) ≫
            NatTrans.app adj₁.counit (R.obj Y'),
        property :=
          (_ :
            (fun b => F.map (U.map (NatTrans.app adj₁.counit X)) ≫ b = NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ b)
              (F.map
                  (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
                    ↑(↑(Cofork.IsColimit.homIso
                            (colimit.isColimit
                              (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                            Y')
                        (h ≫ g))) ≫
                NatTrans.app adj₁.counit (R.obj Y'))) } =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y'))
        (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  (fun b =>
                      F.map (U.map (NatTrans.app adj₁.counit X)) ≫ b = NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ b)
                    (F.map
                        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                          ↑(↑(Cofork.IsColimit.homIso
                                  (colimit.isColimit
                                    (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                      (otherMap R F' adj₁ adj₂ X)))
                                  Y)
                              h)) ≫
                      NatTrans.app adj₁.counit (R.obj Y))) } ≫
          R.map g))
[PROOFSTEP]
dsimp
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
          ↑(↑(Cofork.IsColimit.homIso
                  (colimit.isColimit
                    (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                  Y')
              (h ≫ g))) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y'))
        (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) } ≫
          R.map g))
[PROOFSTEP]
rw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
          (↑(↑(Cofork.IsColimit.homIso
                    (colimit.isColimit
                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                    Y)
                h) ≫
            g)) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y))
          (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) })) ≫
      R.map g
[PROOFSTEP]
erw [adj₂.homEquiv_naturality_right]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
            ↑(↑(Cofork.IsColimit.homIso
                    (colimit.isColimit
                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                    Y)
                h) ≫
          (R ⋙ U).map g) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y))
          (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) })) ≫
      R.map g
[PROOFSTEP]
simp_rw [Functor.comp_map]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
            ↑(↑(Cofork.IsColimit.homIso
                    (colimit.isColimit
                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                    Y)
                h) ≫
          U.map (R.map g)) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y))
          (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) })) ≫
      R.map g
[PROOFSTEP]
simp
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
⊢ IsRightAdjoint R
[PROOFSTEP]
let R' : A ⥤ _ := R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
⊢ IsRightAdjoint R
[PROOFSTEP]
rsuffices : IsRightAdjoint R'
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint R'
⊢ IsRightAdjoint R
[PROOFSTEP]
let this : IsRightAdjoint (R' ⋙ (Monad.comparison (Adjunction.ofRightAdjoint U)).inv) := by infer_instance
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint R'
⊢ IsRightAdjoint (R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U)))
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint R'
this : IsRightAdjoint (R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U))) := inferInstance
⊢ IsRightAdjoint R
[PROOFSTEP]
let this : R' ⋙ (Monad.comparison (Adjunction.ofRightAdjoint U)).inv ≅ R :=
  (isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm : _) ≪≫ R.rightUnitor
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝¹ : IsRightAdjoint R'
this✝ : IsRightAdjoint (R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U))) := inferInstance
this : R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U)) ≅ R :=
  isoWhiskerLeft R (Functor.asEquivalence (Monad.comparison (Adjunction.ofRightAdjoint U))).unitIso.symm ≪≫
    Functor.rightUnitor R
⊢ IsRightAdjoint R
[PROOFSTEP]
exact Adjunction.rightAdjointOfNatIso this
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
⊢ IsRightAdjoint R'
[PROOFSTEP]
let this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.ofRightAdjoint U).toMonad) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm : _)
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
⊢ IsRightAdjoint R'
[PROOFSTEP]
let this : ∀ X, RegularEpi ((Monad.adj (Adjunction.ofRightAdjoint U).toMonad).counit.app X) :=
  by
  intro X
  simp only [Monad.adj_counit]
  exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
⊢ (X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) →
    RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X)
[PROOFSTEP]
intro X
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))
⊢ RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X)
[PROOFSTEP]
simp only [Monad.adj_counit]
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))
⊢ RegularEpi (Monad.Algebra.Hom.mk X.a)
[PROOFSTEP]
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
[GOAL]
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
this : (X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) →
  RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X) :=
  fun X =>
    Eq.mpr
      (_ :
        RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X) =
          RegularEpi (Monad.Algebra.Hom.mk X.a))
      (RegularEpi.mk
        ((Monad.free (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).obj
          ((Adjunction.toMonad (Adjunction.ofRightAdjoint U)).toFunctor.obj X.A))
        (Monad.FreeCoequalizer.topMap X) (Monad.FreeCoequalizer.bottomMap X) (Monad.beckAlgebraCoequalizer X))
⊢ IsRightAdjoint R'
[PROOFSTEP]
exact adjointTriangleLift R' (Monad.adj _)


[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }.map (f ≫ g) =
    { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }.map f ≫
      { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }.map g
[PROOFSTEP]
simp [comp_rightAdjointMate]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      (fun X => η_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        Y =
    (fun X => η_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        X ≫
      (F ⊗ Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ D) ≫ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (F.map f ⊗ F.map (inv f)ᘁ)
[PROOFSTEP]
rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id, ← Category.assoc, coevaluation_comp_rightAdjointMate,
  Category.assoc, ← comp_tensor_id, IsIso.inv_hom_id, tensor_id, Category.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ } ⊗ F).map f ≫
      (fun X => ε_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        Y =
    (fun X => ε_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        X ≫
      (𝟙_ (C ⥤ D)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map (inv f)ᘁ ⊗ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ ≫ 𝟙 (𝟙_ D)
[PROOFSTEP]
rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc, rightAdjointMate_comp_evaluation, ←
  Category.assoc, ← id_tensor_comp, IsIso.hom_inv_id, tensor_id, Category.id_comp]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }.map (f ≫ g) =
    { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }.map f ≫
      { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }.map g
[PROOFSTEP]
simp [comp_leftAdjointMate]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      (fun X => η_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        Y =
    (fun X => η_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        X ≫
      (Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) } ⊗ F).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ D) ≫ η_ (ᘁ(F.obj Y)) (F.obj Y) = η_ (ᘁ(F.obj X)) (F.obj X) ≫ ((ᘁF.map (inv f)) ⊗ F.map f)
[PROOFSTEP]
rw [Functor.map_inv, Category.id_comp, ← tensor_id_comp_id_tensor, ← Category.assoc, coevaluation_comp_leftAdjointMate,
  Category.assoc, ← id_tensor_comp, IsIso.inv_hom_id, tensor_id, Category.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F ⊗ Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).map f ≫
      (fun X => ε_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        Y =
    (fun X => ε_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        X ≫
      (𝟙_ (C ⥤ D)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ ᘁF.map (inv f)) ≫ ε_ (ᘁ(F.obj Y)) (F.obj Y) = ε_ (ᘁ(F.obj X)) (F.obj X) ≫ 𝟙 (𝟙_ D)
[PROOFSTEP]
rw [Category.comp_id, Functor.map_inv, ← tensor_id_comp_id_tensor, Category.assoc, leftAdjointMate_comp_evaluation, ←
  Category.assoc, ← comp_tensor_id, IsIso.hom_inv_id, tensor_id, Category.id_comp]


[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
e : C ≌ D
inst✝ : WellPowered C
X : D
⊢ EssentiallySmall (MonoOver ((Equivalence.symm e).functor.obj X))
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
⊢ (yoneda.map (NatTrans.app h.unit X) ≫
      NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f)) =
    𝟙 (yoneda.obj ((𝟭 C).obj X))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((𝟭 C).obj X)).obj x
⊢ NatTrans.app
      (yoneda.map (NatTrans.app h.unit X) ≫
        NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f))
      x a✝ =
    NatTrans.app (𝟙 (yoneda.obj ((𝟭 C).obj X))) x a✝
[PROOFSTEP]
apply L.map_injective
[GOAL]
case w.h.h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((𝟭 C).obj X)).obj x
⊢ L.map
      (NatTrans.app
        (yoneda.map (NatTrans.app h.unit X) ≫
          NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f))
        x a✝) =
    L.map (NatTrans.app (𝟙 (yoneda.obj ((𝟭 C).obj X))) x a✝)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
⊢ (NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f)) ≫
      yoneda.map (NatTrans.app h.unit X) =
    𝟙 (yoneda.obj ((L ⋙ R).obj X))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ NatTrans.app
      ((NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f)) ≫
        yoneda.map (NatTrans.app h.unit X))
      x a✝ =
    NatTrans.app (𝟙 (yoneda.obj ((L ⋙ R).obj X))) x a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ L.preimage (↑(Adjunction.homEquiv h x.unop (L.obj X)).symm a✝) ≫ NatTrans.app h.unit X = a✝
[PROOFSTEP]
simp only [Adjunction.homEquiv_counit, preimage_comp, preimage_map, Category.assoc]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ a✝ ≫ L.preimage (NatTrans.app h.counit (L.obj X)) ≫ NatTrans.app h.unit X = a✝
[PROOFSTEP]
rw [← h.unit_naturality]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ a✝ ≫ NatTrans.app h.unit (R.obj (L.obj X)) ≫ R.map (L.map (L.preimage (NatTrans.app h.counit (L.obj X)))) = a✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X : D
⊢ (coyoneda.map (NatTrans.app h.counit X).op ≫
      NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f)) =
    𝟙 (coyoneda.obj (op ((𝟭 D).obj X)))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((𝟭 D).obj X))).obj x
⊢ NatTrans.app
      (coyoneda.map (NatTrans.app h.counit X).op ≫
        NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f))
      x a✝ =
    NatTrans.app (𝟙 (coyoneda.obj (op ((𝟭 D).obj X)))) x a✝
[PROOFSTEP]
apply R.map_injective
[GOAL]
case w.h.h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((𝟭 D).obj X))).obj x
⊢ R.map
      (NatTrans.app
        (coyoneda.map (NatTrans.app h.counit X).op ≫
          NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f))
        x a✝) =
    R.map (NatTrans.app (𝟙 (coyoneda.obj (op ((𝟭 D).obj X)))) x a✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X : D
⊢ (NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f)) ≫
      coyoneda.map (NatTrans.app h.counit X).op =
    𝟙 (coyoneda.obj (op ((R ⋙ L).obj X)))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ NatTrans.app
      ((NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f)) ≫
        coyoneda.map (NatTrans.app h.counit X).op)
      x a✝ =
    NatTrans.app (𝟙 (coyoneda.obj (op ((R ⋙ L).obj X)))) x a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ NatTrans.app h.counit X ≫ R.preimage (↑(Adjunction.homEquiv h (R.obj X) x) a✝) = a✝
[PROOFSTEP]
simp only [Adjunction.homEquiv_unit, preimage_comp, preimage_map]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ NatTrans.app h.counit X ≫ R.preimage (NatTrans.app h.unit (R.obj X)) ≫ a✝ = a✝
[PROOFSTEP]
rw [← h.counit_naturality]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ L.map (R.map (R.preimage (NatTrans.app h.unit (R.obj X)) ≫ a✝)) ≫ NatTrans.app h.counit x = a✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : L.map f = L.map g
⊢ f = g
[PROOFSTEP]
rw [← (h.homEquiv X (L.obj Y)).apply_eq_iff_eq] at H
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map f) = ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map g)
⊢ f = g
[PROOFSTEP]
simpa using H =≫ inv (h.unit.app Y)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.counit
X Y : D
f g : X ⟶ Y
H : R.map f = R.map g
⊢ f = g
[PROOFSTEP]
rw [← (h.homEquiv (R.obj X) Y).symm.apply_eq_iff_eq] at H
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.counit
X Y : D
f g : X ⟶ Y
H : ↑(Adjunction.homEquiv h (R.obj X) Y).symm (R.map f) = ↑(Adjunction.homEquiv h (R.obj X) Y).symm (R.map g)
⊢ f = g
[PROOFSTEP]
simpa using inv (h.counit.app X) ≫= H
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
⊢ IsIso (whiskerLeft L h.counit)
[PROOFSTEP]
have := h.left_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerRight h.unit L ≫ whiskerLeft L h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerLeft L h.counit)
[PROOFSTEP]
rw [← IsIso.eq_inv_comp] at this
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerLeft L h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerLeft L h.counit)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerLeft L h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
⊢ IsIso (whiskerRight h.counit R)
[PROOFSTEP]
have := h.right_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerLeft R h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerRight h.counit R)
[PROOFSTEP]
rw [← IsIso.eq_inv_comp] at this
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerRight h.counit R = inv (whiskerLeft R h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerRight h.counit R)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerRight h.counit R = inv (whiskerLeft R h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (inv (whiskerLeft R h.unit) ≫ 𝟙 (R ⋙ 𝟭 C))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
⊢ IsIso (whiskerLeft R h.unit)
[PROOFSTEP]
have := h.right_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerLeft R h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerLeft R h.unit)
[PROOFSTEP]
rw [← IsIso.eq_comp_inv] at this
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerLeft R h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
⊢ IsIso (whiskerLeft R h.unit)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerLeft R h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
⊢ IsIso (𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
⊢ IsIso (whiskerRight h.unit L)
[PROOFSTEP]
have := h.left_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerRight h.unit L ≫ whiskerLeft L h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerRight h.unit L)
[PROOFSTEP]
rw [← IsIso.eq_comp_inv] at this
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (whiskerLeft L h.counit)
⊢ IsIso (whiskerRight h.unit L)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (whiskerLeft L h.counit)
⊢ IsIso (𝟙 (𝟭 C ⋙ L) ≫ inv (whiskerLeft L h.counit))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ ↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X' Y).symm
      (f ≫ g) =
    L.map f ≫
      ↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X Y).symm
        g
[PROOFSTEP]
apply iD.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ iD.map
      (↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X' Y).symm
        (f ≫ g)) =
    iD.map
      (L.map f ≫
        ↑((fun X Y =>
                  Trans.trans
                    (Trans.trans
                      (Trans.trans
                        (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                        (homEquiv adj (iC.obj X) (iD.obj Y)))
                      (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                    (equivOfFullyFaithful iC).symm)
                X Y).symm
          g)
[PROOFSTEP]
simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ ↑((fun X Y =>
            Trans.trans
              (Trans.trans
                (Trans.trans
                  (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                  (homEquiv adj (iC.obj X) (iD.obj Y)))
                (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
              (equivOfFullyFaithful iC).symm)
          X Y)
      (f ≫ g) =
    ↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X Y')
        f ≫
      R.map g
[PROOFSTEP]
apply iC.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ iC.map
      (↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X Y)
        (f ≫ g)) =
    iC.map
      (↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X Y')
          f ≫
        R.map g)
[PROOFSTEP]
suffices : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
[GOAL]
case a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
this : R'.map (iD.map g) ≫ NatTrans.app comm2.hom Y = NatTrans.app comm2.hom Y' ≫ iC.map (R.map g)
⊢ iC.map
      (↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X Y)
        (f ≫ g)) =
    iC.map
      (↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X Y')
          f ≫
        R.map g)
[PROOFSTEP]
simp [Trans.trans, this]
[GOAL]
case this
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ R'.map (iD.map g) ≫ NatTrans.app comm2.hom Y = NatTrans.app comm2.hom Y' ≫ iC.map (R.map g)
[PROOFSTEP]
apply comm2.hom.naturality g


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : Factors f h
u : Y ⟶ f.obj.left
hu : u ≫ arrow f = h
⊢ (u ≫ ((forget X).map e.hom).left) ≫ arrow g = h
[PROOFSTEP]
simp [hu]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : Factors g h
u : Y ⟶ g.obj.left
hu : u ≫ arrow g = h
⊢ (u ≫ ((forget X).map e.inv).left) ≫ arrow f = h
[PROOFSTEP]
simp [hu]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ Y
⊢ ∀ (a b : MonoOver Y), Setoid.r a b → (fun P => MonoOver.Factors P f) a = (fun P => MonoOver.Factors P f) b
[PROOFSTEP]
rintro P Q ⟨h⟩
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) P = (fun P => MonoOver.Factors P f) Q
[PROOFSTEP]
apply propext
[GOAL]
case intro.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) P ↔ (fun P => MonoOver.Factors P f) Q
[PROOFSTEP]
constructor
[GOAL]
case intro.a.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) P → (fun P => MonoOver.Factors P f) Q
[PROOFSTEP]
rintro ⟨i, w⟩
[GOAL]
case intro.a.mp.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ P.obj.left
w : i ≫ MonoOver.arrow P = f
⊢ MonoOver.Factors Q f
[PROOFSTEP]
exact ⟨i ≫ h.hom.left, by erw [Category.assoc, Over.w h.hom, w]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ P.obj.left
w : i ≫ MonoOver.arrow P = f
⊢ (i ≫ h.hom.left) ≫ MonoOver.arrow Q = f
[PROOFSTEP]
erw [Category.assoc, Over.w h.hom, w]
[GOAL]
case intro.a.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) Q → (fun P => MonoOver.Factors P f) P
[PROOFSTEP]
rintro ⟨i, w⟩
[GOAL]
case intro.a.mpr.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ Q.obj.left
w : i ≫ MonoOver.arrow Q = f
⊢ MonoOver.Factors P f
[PROOFSTEP]
exact ⟨i ≫ h.inv.left, by erw [Category.assoc, Over.w h.inv, w]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ Q.obj.left
w : i ≫ MonoOver.arrow Q = f
⊢ (i ≫ h.inv.left) ≫ MonoOver.arrow P = f
[PROOFSTEP]
erw [Category.assoc, Over.w h.inv, w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
⊢ 𝟙 X ≫ MonoOver.arrow (MonoOver.mk' f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
P : Subobject X
⊢ 𝟙 (underlying.obj P) ≫ MonoOver.arrow (representative.obj P) = arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ Factors P (f ≫ g)
[PROOFSTEP]
induction' P using Quotient.ind' with P
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Factors P✝ g
P : MonoOver Z
h : Factors (Quotient.mk'' P) g
⊢ Factors (Quotient.mk'' P) (f ≫ g)
[PROOFSTEP]
obtain ⟨g, rfl⟩ := h
[GOAL]
case h.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ Factors (Quotient.mk'' P) (f ≫ g ≫ MonoOver.arrow P)
[PROOFSTEP]
exact ⟨f ≫ g, by simp⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ (f ≫ g) ≫ MonoOver.arrow P = f ≫ g ≫ MonoOver.arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
⊢ 0 ≫ MonoOver.arrow (representative.obj P) = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ Factors P f → Factors Q f
[PROOFSTEP]
simp only [factors_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ MonoOver.Factors (representative.obj P) f → MonoOver.Factors (representative.obj Q) f
[PROOFSTEP]
exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
x✝ : MonoOver.Factors (representative.obj P) f
u : Z ⟶ (representative.obj P).obj.left
hu : u ≫ MonoOver.arrow (representative.obj P) = f
⊢ (u ≫ ofLE P Q h) ≫ MonoOver.arrow (representative.obj Q) = f
[PROOFSTEP]
simp [← hu]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h = 𝟙 (underlying.obj P)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h ≫ arrow P = 𝟙 (underlying.obj P) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
⊢ factorThru (mk f) f (_ : Factors (mk f) f) = (underlyingIso f).inv
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
⊢ factorThru (mk f) f (_ : Factors (mk f) f) ≫ arrow (mk f) = (underlyingIso f).inv ≫ arrow (mk f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : Factors P (f ≫ arrow P)
⊢ factorThru P (f ≫ arrow P) h = f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : Factors P (f ≫ arrow P)
⊢ factorThru P (f ≫ arrow P) h ≫ arrow P = f ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 ↔ f = 0
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 → f = 0
[PROOFSTEP]
intro w
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h = 0
⊢ f = 0
[PROOFSTEP]
replace w := w =≫ P.arrow
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h ≫ arrow P = 0 ≫ arrow P
⊢ f = 0
[PROOFSTEP]
simpa using w
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ f = 0 → factorThru P f h = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h = 0
[PROOFSTEP]
ext
[GOAL]
case mpr.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h ≫ arrow P = 0 ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ f ≫ factorThru P g h = factorThru P (f ≫ g) (_ : Factors P (f ≫ g))
[PROOFSTEP]
apply (cancel_mono P.arrow).mp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ (f ≫ factorThru P g h) ≫ arrow P = factorThru P (f ≫ g) (_ : Factors P (f ≫ g)) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : Factors P f
⊢ factorThru Q f (_ : Factors Q f) = factorThru P f w ≫ ofLE P Q h
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : Factors P f
⊢ factorThru Q f (_ : Factors Q f) ≫ arrow Q = (factorThru P f w ≫ ofLE P Q h) ≫ arrow Q
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
wf : Factors P f
wg : Factors P g
⊢ (factorThru P f wf + factorThru P g wg) ≫ MonoOver.arrow (representative.obj P) = f + g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
wg : Factors P g
⊢ factorThru P (f + g) w = factorThru P f wf + factorThru P g wg
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
wg : Factors P g
⊢ factorThru P (f + g) w ≫ arrow P = (factorThru P f wf + factorThru P g wg) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ (factorThru P (f + g) w - factorThru P g wg) ≫ MonoOver.arrow (representative.obj P) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ factorThru P (f + g) w - factorThru P g wg = factorThru P f (_ : Factors P f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ (factorThru P (f + g) w - factorThru P g wg) ≫ arrow P = factorThru P f (_ : Factors P f) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
⊢ (factorThru P (f + g) w - factorThru P f wf) ≫ MonoOver.arrow (representative.obj P) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
⊢ factorThru P (f + g) w - factorThru P f wf = factorThru P g (_ : Factors P g)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
⊢ (factorThru P (f + g) w - factorThru P f wf) ≫ arrow P = factorThru P g (_ : Factors P g) ≫ arrow P
[PROOFSTEP]
simp