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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
⊢ A ∈ Functor.essImage i
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
⊢ A ∈ Functor.essImage i
let η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ A ∈ Functor.essImage i
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
⊢ A ∈ Functor.essImage i
haveI : IsIso (η.app (i.obj ((leftAdjoint i).obj A))) :=
  Functor.essImage.unit_isIso ((i.obj_mem_essImage _))
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝ : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
this : Epi (η.app A)
⊢ A ∈ Functor.essImage i
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ A ∈ Functor.essImage i
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)))
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝ : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
this : Epi (η.app A)
⊢ A ∈ Functor.essImage i
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝ : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
this : Epi (η.app A)
⊢ A ∈ Functor.essImage i
skip
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝¹ : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
this✝ : Epi (η.app A)
this : IsIso (η.app A)
⊢ A ∈ Functor.essImage i
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝ : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
this : Epi (η.app A)
⊢ A ∈ Functor.essImage i
haveI := isIso_of_epi_of_isSplitMono (η.app A)
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this✝¹ : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
this✝ : Epi (η.app A)
this : IsIso (η.app A)
⊢ A ∈ Functor.essImage i
exact mem_essImage_of_unit_isIso 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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (retraction (η.app A) ≫ η.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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (η.app A)
refine @epi_of_epi _ _ _ _ _ (retraction (η.app A)) (η.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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (η.app ((leftAdjoint i ⋙ i).obj A) ≫ (leftAdjoint i ⋙ i).map (retraction (η.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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (retraction (η.app A) ≫ η.app A)
rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]
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
inst✝ : IsSplitMono ((ofRightAdjoint i).unit.app A)
η : 𝟭 C ⟶ leftAdjoint i ⋙ i := (ofRightAdjoint i).unit
this : IsIso (η.app (i.obj ((leftAdjoint i).obj A)))
⊢ Epi (η.app ((leftAdjoint i ⋙ i).obj A) ≫ (leftAdjoint i ⋙ i).map (retraction (η.app A)))
apply epi_comp (η.app (i.obj ((leftAdjoint i).obj A)))