Mathlib: build an adjunction with rightAdjointOfEquiv when only one naturality is easy

If you have a bijection e X Y : (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y) assembled as a chain of Equivs (FullyFaithful.homEquiv, Iso.homCongr, adj.homEquiv, and Equiv.ofBijective from a universal property), use Adjunction.adjunctionOfEquivRight e he. It only requires naturality in X, in the forward direction: e X' Y (F.map f ≫ g) = f ≫ e X Y g. It defines the right adjoint functor itself, with obj := G_obj definitionally. When one step of the chain is (Equiv.ofBijective φ _).symm, prove naturality by applying the uniqueness/ext lemma behind φ. This turns the goal into a statement about forward maps, where homEquiv_naturality_left and NatIso naturality apply. To prove the right adjoint is fully faithful, show the counit is an iso: simp [defs, Adjunction.homEquiv_counit] computes the image of counit.app under the faithful inclusion. Then use adj.fullyFaithfulROfIsIsoCounit.full/.faithful. Combined with Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint, this gives Serre-quotient statements for free.