[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
