mk' — Mathlib

Lean4
/-- Construct an adjunction from the data of a `CoreHomEquivUnitCounit`, i.e. a hom set
equivalence, unit and counit natural transformations together with proofs of the equalities
`homEquiv_unit` and `homEquiv_counit` relating them to each other.
-/
@[simps]
def mk' (adj : CoreHomEquivUnitCounit F G) : F ⊣ G
    where
  unit := adj.unit
  counit := adj.counit
  left_triangle_components
    X := by
    rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]
    simp
  right_triangle_components
    Y := by
    rw [← adj.homEquiv_unit, ← (adj.homEquiv _ _).eq_symm_apply, adj.homEquiv_counit]
    simp
Похожие утверждения