ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<VAR>hf : f.FullyFaithful<VAR>X : C<VAR>e : f.obj X ≅ f.obj X<GOAL>((hf.autMulEquivOfFullyFaithful X).symm e).inv = hf.preimage e.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<VAR>hf : f.FullyFaithful<VAR>X : C<VAR>e : f.obj X ≅ f.obj X<GOAL>((hf.autMulEquivOfFullyFaithful X).symm e).hom = hf.preimage e.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<GOAL>CategoryTheory.IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>hA : CategoryTheory.IsSubterminal A<VAR>T : C<VAR>hT : CategoryTheory.Limits.IsTerminal T<GOAL>CategoryTheory.Mono (hT.from A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>hA : CategoryTheory.IsSubterminal A<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A T : C<VAR>hT : CategoryTheory.Limits.IsTerminal T<VAR>CategoryTheory.Mono (hT.from A)<GOAL>CategoryTheory.IsSubterminal A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)<GOAL>CategoryTheory.IsSubterminal A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : C<VAR>hT : CategoryTheory.Limits.IsTerminal T<GOAL>CategoryTheory.IsSubterminal T
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.IsSubterminal (⊤_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>hA : CategoryTheory.IsSubterminal A<VAR>CategoryTheory.Limits.HasBinaryProduct A A<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.diag A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>CategoryTheory.Limits.HasBinaryProduct A A<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.diag A)<GOAL>CategoryTheory.IsSubterminal A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>hA : CategoryTheory.IsSubterminal A<VAR>CategoryTheory.Limits.HasBinaryProduct A A<GOAL>hA.isoDiag.inv = CategoryTheory.Limits.diag A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>hA : CategoryTheory.IsSubterminal A<VAR>CategoryTheory.Limits.HasBinaryProduct A A<GOAL>hA.isoDiag.hom = CategoryTheory.inv (CategoryTheory.Limits.diag A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.FullSubcategory fun A => CategoryTheory.IsSubterminal A<GOAL>(CategoryTheory.subterminalInclusion C).obj self = self.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), (CategoryTheory.subterminalInclusion C).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>∀ {X Y : CategoryTheory.Subterminals C} (f : X ⟶ Y), (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.map f = CategoryTheory.MonoOver.homMk f ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>X : CategoryTheory.Subterminals C<GOAL>((CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.obj X).obj = CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>∀ {X Y : CategoryTheory.MonoOver (⊤_ C)} (f : X ⟶ Y), (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.map f = f.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>X : CategoryTheory.MonoOver (⊤_ C)<GOAL>((CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.obj X).obj = X.obj.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>(CategoryTheory.subterminalsEquivMonoOverTerminal C).unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>(CategoryTheory.subterminalsEquivMonoOverTerminal C).counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl (({ obj := fun X => { obj := X.obj.left, property := ⋯ }, map := fun {X Y} f => f.left, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun X => { obj := CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj), property := ⋯ }, map := fun {X Y} f => CategoryTheory.MonoOver.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }).obj X).obj.left) ⋯) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>(CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.comp ((CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))) = CategoryTheory.subterminalInclusion C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>(CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.comp (CategoryTheory.subterminalInclusion C) = (CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X : C<GOAL>(CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inl X)) = Sum.inl X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X : D<GOAL>(CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inr X)) = Sum.inr (Sum.inl X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X : E<GOAL>(CategoryTheory.sum.associator C D E).obj (Sum.inr X) = Sum.inr (Sum.inr X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X Y : C<VAR>f : Sum.inl (Sum.inl X) ⟶ Sum.inl (Sum.inl Y)<GOAL>(CategoryTheory.sum.associator C D E).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X Y : D<VAR>f : Sum.inl (Sum.inr X) ⟶ Sum.inl (Sum.inr Y)<GOAL>(CategoryTheory.sum.associator C D E).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X Y : E<VAR>f : Sum.inr X ⟶ Sum.inr Y<GOAL>(CategoryTheory.sum.associator C D E).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X : C<GOAL>(CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inl X) = Sum.inl (Sum.inl X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X : D<GOAL>(CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inr (Sum.inl X)) = Sum.inl (Sum.inr X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X : E<GOAL>(CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inr (Sum.inr X)) = Sum.inr X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X Y : C<VAR>f : Sum.inl X ⟶ Sum.inl Y<GOAL>(CategoryTheory.sum.inverseAssociator C D E).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X Y : D<VAR>f : Sum.inr (Sum.inl X) ⟶ Sum.inr (Sum.inl Y)<GOAL>(CategoryTheory.sum.inverseAssociator C D E).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>E : Type u<VAR>CategoryTheory.Category.{v, u} E<VAR>X Y : E<VAR>f : Sum.inr (Sum.inr X) ⟶ Sum.inr (Sum.inr Y)<GOAL>(CategoryTheory.sum.inverseAssociator C D E).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>x y : F.Elements<VAR>h₁ : x.fst = y.fst<VAR>h₂ : F.map (CategoryTheory.eqToHom h₁) x.snd = y.snd<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>x y : F.Elements<VAR>f : x.fst ⟶ y.fst<VAR>hf : F.map f x.snd = y.snd<GOAL>↑(CategoryTheory.CategoryOfElements.homMk x y f hf) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>x y : F.Elements<VAR>f g : x ⟶ y<VAR>w : ↑f = ↑g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>p q r : F.Elements<VAR>f : p ⟶ q<VAR>g : q ⟶ r<GOAL>↑(CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ↑f ↑g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>p : F.Elements<GOAL>↑(CategoryTheory.CategoryStruct.id p) = CategoryTheory.CategoryStruct.id p.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>p q : F.Elements<VAR>f : p ⟶ q<GOAL>F.map (↑f) p.snd = q.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X : F.Elements<GOAL>(CategoryTheory.CategoryOfElements.π F).obj X = X.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : F.Elements} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.π F).map f = ↑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>α : F₁ ⟶ F₂<VAR>t : F₁.Elements<GOAL>((CategoryTheory.CategoryOfElements.map α).obj t).fst = t.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>α : F₁ ⟶ F₂<VAR>t : F₁.Elements<GOAL>((CategoryTheory.CategoryOfElements.map α).obj t).snd = α.app t.fst t.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>α : F₁ ⟶ F₂<VAR>t₁ t₂ : F₁.Elements<VAR>k : t₁ ⟶ t₂<GOAL>↑((CategoryTheory.CategoryOfElements.map α).map k) = ↑k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>α : F₁ ⟶ F₂<GOAL>(CategoryTheory.CategoryOfElements.map α).comp (CategoryTheory.CategoryOfElements.π F₂) = CategoryTheory.CategoryOfElements.π F₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X : F.Elements<GOAL>(CategoryTheory.CategoryOfElements.toStructuredArrow F).obj X = { left := { as := PUnit.unit }, right := X.fst, hom := fun x => X.snd }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y : F.Elements<VAR>f : X ⟶ Y<GOAL>((CategoryTheory.CategoryOfElements.toStructuredArrow F).map f).right = ↑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.StructuredArrow PUnit.{w + 1} F<GOAL>(CategoryTheory.CategoryOfElements.fromStructuredArrow F).obj X = ⟨X.right, X.hom PUnit.unit⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.CategoryOfElements.fromStructuredArrow F).map f = ⟨f.right, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X : F.Elements<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).functor.obj X = CategoryTheory.StructuredArrow.mk fun x => X.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).counitIso.inv = { app := fun X => (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯).inv, naturality := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F).leftUnitor.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯) ⋯).inv (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) ((CategoryTheory.CategoryOfElements.fromStructuredArrow F).associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯).inv ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).leftUnitor.hom)))))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y : F.Elements<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).functor.map f = CategoryTheory.StructuredArrow.homMk ↑f ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso.inv = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯).hom ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) ((CategoryTheory.CategoryOfElements.fromStructuredArrow F).associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯) ⋯).hom (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F).leftUnitor.hom) (CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯).inv)))))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.StructuredArrow PUnit.{w + 1} F<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).inverse.obj X = ⟨X.right, X.hom PUnit.unit⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<GOAL>(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).counitIso.hom = { app := fun X => (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯).hom, naturality := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).inverse.map f = ⟨f.right, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>∀ {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk (↑f.unop).unop ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : F.Elementsᵒᵖ<GOAL>(CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm (Opposite.unop X).snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ<GOAL>((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj X).fst = Opposite.op (Opposite.unop X).left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ<GOAL>((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj X).snd = CategoryTheory.yonedaEquiv.toFun (Opposite.unop X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<GOAL>↑((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).map f) = f.unop.left.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : C<VAR>f : CategoryTheory.yoneda.obj X ⟶ F<GOAL>(CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj (Opposite.op (CategoryTheory.CostructuredArrow.mk f)) = ⟨Opposite.op X, CategoryTheory.yonedaEquiv.toFun f⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>(CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id F.Elements
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>(CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso.inv = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>∀ {X Y : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse.map f = ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).map f.op).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse.obj X = Opposite.op ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj (Opposite.op X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso.hom = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>∀ {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor.map f = CategoryTheory.CostructuredArrow.homMk (↑f.unop).unop ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : F.Elementsᵒᵖ<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor.obj X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm (Opposite.unop X).snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso.inv = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.leftUnitor.hom) (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)))))))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>α : F₁ ⟶ F₂<GOAL>(CategoryTheory.CategoryOfElements.map α).op.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F₂) = (CategoryTheory.CategoryOfElements.toCostructuredArrow F₁).comp (CategoryTheory.CostructuredArrow.map α)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : F.Elementsᵒᵖ<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj F).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X).1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : F.Elementsᵒᵖ<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj F).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X).1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ F).inv.app X = CategoryTheory.CategoryStruct.id X.left