C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ (ofRightAdjoint i).unit.app A =
    (getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ IsIso ((ofRightAdjoint i).unit.app A)
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
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ (ofRightAdjoint i).unit.app A = (getIso h).inv ≫ (𝟭 C).map (getIso h).hom ≫ (ofRightAdjoint i).unit.app A
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ (ofRightAdjoint i).unit.app A =
    (getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
rw [← NatTrans.naturality]
no goals
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
⊢ (ofRightAdjoint i).unit.app A = (getIso h).inv ≫ (𝟭 C).map (getIso h).hom ≫ (ofRightAdjoint i).unit.app A
simp
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
this :
  (ofRightAdjoint i).unit.app A =
    (getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
⊢ IsIso ((getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom)
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
this :
  (ofRightAdjoint i).unit.app A =
    (getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
⊢ IsIso ((ofRightAdjoint i).unit.app A)
rw [this]
no goals
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category C
inst✝² : Category D
inst✝¹ : Category E
i : D ⥤ C
inst✝ : Reflective i
A : C
h : A ∈ essImage i
this :
  (ofRightAdjoint i).unit.app A =
    (getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom
⊢ IsIso ((getIso h).inv ≫ (ofRightAdjoint i).unit.app (i.obj (witness h)) ≫ (leftAdjoint i ⋙ i).map (getIso h).hom)
infer_instance