J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
⊢ SolutionSetCondition G
intro A
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x => (Adjunction.ofRightAdjoint G).unit.app A) i ≫ G.map g = h
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
refine'
  ⟨PUnit, fun _ => (leftAdjoint G).obj A, fun _ => (Adjunction.ofRightAdjoint G).unit.app A, _⟩
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x => (Adjunction.ofRightAdjoint G).unit.app A) i ≫ G.map g = h
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x => (Adjunction.ofRightAdjoint G).unit.app A) i ≫ G.map g = h
intro B h
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x => (Adjunction.ofRightAdjoint G).unit.app A) PUnit.unit ≫
      G.map (↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint G) A B).symm h) =
    h
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x => (Adjunction.ofRightAdjoint G).unit.app A) i ≫ G.map g = h
refine' ⟨PUnit.unit, ((Adjunction.ofRightAdjoint G).homEquiv _ _).symm h, _⟩
no goals
J : Type v
C : Type u
inst✝² : Category C
D : Type u
inst✝¹ : Category D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x => (Adjunction.ofRightAdjoint G).unit.app A) PUnit.unit ≫
      G.map (↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint G) A B).symm h) =
    h
rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]