ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A B : G.Coalgebra<VAR>h : A.A ≅ B.A<VAR>w : CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a := by aesop_cat<GOAL>(CategoryTheory.Comonad.Coalgebra.isoMk h w).inv.f = h.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<GOAL>∀ {X Y : G.Coalgebra} (f : X ⟶ Y), G.forget.map f = f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A : G.Coalgebra<GOAL>G.forget.obj A = A.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (G.cofree.map f).f = G.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X : C<GOAL>(G.cofree.obj X).A = G.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X : C<GOAL>(G.cofree.obj X).a = G.δ.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<GOAL>G.adj.counit = { app := fun Y => G.ε.app Y, naturality := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<GOAL>G.adj.unit = { app := fun X => { f := X.a, h := ⋯ }, naturality := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A B : G.Coalgebra<VAR>f : A ⟶ B<VAR>CategoryTheory.IsIso f.f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X Y : G.Coalgebra<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.Epi f.f<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X Y : G.Coalgebra<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.Mono f.f<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Monad C<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.map (self.η.app X)) (self.μ.app X) = CategoryTheory.CategoryStruct.id (self.obj ((CategoryTheory.Functor.id C).obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Monad C<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.η.app (self.obj X)) (self.μ.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (self.obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Monad C<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.map (self.μ.app X)) (self.μ.app X) = CategoryTheory.CategoryStruct.comp (self.μ.app (self.obj X)) (self.μ.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Comonad C<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.map (self.ε.app X)) = CategoryTheory.CategoryStruct.id (self.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Comonad C<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.map (self.δ.app X)) = CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.δ.app (self.obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Comonad C<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.ε.app (self.obj X)) = CategoryTheory.CategoryStruct.id (self.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>self : CategoryTheory.MonadHom T₁ T₂<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (T₁.η.app X) (self.app X) = T₂.η.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>self : CategoryTheory.MonadHom T₁ T₂<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (self.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T₁.map (self.app X)) (self.app (T₂.obj X))) (T₂.μ.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>self : CategoryTheory.ComonadHom M N<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (M.δ.app X) (CategoryTheory.CategoryStruct.comp (self.app (M.obj X)) (N.map (self.app X)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>self : CategoryTheory.ComonadHom M N<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.app X) (N.ε.app X) = M.ε.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>f g : T₁ ⟶ T₂<VAR>h : f.app = g.app<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Comonad C<VAR>f g : T₁ ⟶ T₂<VAR>h : f.app = g.app<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<GOAL>(CategoryTheory.CategoryStruct.id T).toNatTrans = CategoryTheory.CategoryStruct.id T.toFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ T₃ : CategoryTheory.Monad C<VAR>f : T₁ ⟶ T₂<VAR>g : T₂ ⟶ T₃<GOAL>(CategoryTheory.CategoryStruct.comp f g).toNatTrans = CategoryTheory.CategoryStruct.comp f.toNatTrans g.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<GOAL>(CategoryTheory.CategoryStruct.id T).toNatTrans = CategoryTheory.CategoryStruct.id T.toFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ T₃ : CategoryTheory.Comonad C<VAR>f : T₁ ⟶ T₂<VAR>g : T₂ ⟶ T₃<GOAL>(CategoryTheory.CategoryStruct.comp f g).toNatTrans = CategoryTheory.CategoryStruct.comp f.toNatTrans g.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Monad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X := by aesop_cat<VAR>f_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X) := by aesop_cat<GOAL>(CategoryTheory.MonadIso.mk f f_η f_μ).hom.toNatTrans = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Monad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X := by aesop_cat<VAR>f_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X) := by aesop_cat<GOAL>(CategoryTheory.MonadIso.mk f f_η f_μ).inv.toNatTrans = f.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X := by aesop_cat<VAR>f_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (M.δ.app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X))) := by aesop_cat<GOAL>(CategoryTheory.ComonadIso.mk f f_ε f_δ).hom.toNatTrans = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X := by aesop_cat<VAR>f_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (M.δ.app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X))) := by aesop_cat<GOAL>(CategoryTheory.ComonadIso.mk f f_ε f_δ).inv.toNatTrans = f.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.Monad C} (f : X ⟶ Y), (CategoryTheory.monadToFunctor C).map f = f.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<GOAL>(CategoryTheory.monadToFunctor C).obj T = T.toFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Monad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X<VAR>f_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X)<GOAL>(CategoryTheory.monadToFunctor C).mapIso (CategoryTheory.MonadIso.mk f f_η f_μ) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<GOAL>(CategoryTheory.comonadToFunctor C).obj G = G.toFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.Comonad C} (f : X ⟶ Y), (CategoryTheory.comonadToFunctor C).map f = f.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X<VAR>f_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (M.δ.app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))<GOAL>(CategoryTheory.comonadToFunctor C).mapIso (CategoryTheory.ComonadIso.mk f f_ε f_δ) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Monad C<VAR>h : M ≅ N<GOAL>(CategoryTheory.MonadIso.toNatIso h).inv = h.inv.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Monad C<VAR>h : M ≅ N<GOAL>(CategoryTheory.MonadIso.toNatIso h).hom = h.hom.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>h : M ≅ N<GOAL>(CategoryTheory.ComonadIso.toNatIso h).inv = h.inv.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>M N : CategoryTheory.Comonad C<VAR>h : M ≅ N<GOAL>(CategoryTheory.ComonadIso.toNatIso h).hom = h.hom.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Monad.id C).obj X = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Monad.id C).η.app X = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Monad.id C).μ.app X = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Monad.id C).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Comonad.id C).δ.app X = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Comonad.id C).ε.app X = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Comonad.id C).obj X = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Comonad.id C).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : CategoryTheory.MorphismProperty C<GOAL>P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>⊤ = fun x x_1 x => True
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W W' : CategoryTheory.MorphismProperty C<VAR>h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f<GOAL>W = W'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>⊤ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.op.unop = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty Cᵒᵖ<GOAL>P.unop.op = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>P.inverseImage F f ↔ P (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty C<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : P f<GOAL>P.map F (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ⥤ D<GOAL>Monotone fun x => x.map F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>self : P.RespectsIso<VAR>X Y Z : C<VAR>e : Y ≅ Z<VAR>f : X ⟶ Y<VAR>hf : P f<GOAL>P (f ≫ e.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>self : P.RespectsIso<VAR>X Y Z : C<VAR>e : X ≅ Y<VAR>f : Y ⟶ Z<VAR>hf : P f<GOAL>P (e.hom ≫ f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P ≤ P.isoClosure
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>Monotone CategoryTheory.MorphismProperty.isoClosure
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.RespectsIso<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>P (f ≫ g) ↔ P g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.RespectsIso<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>P (f ≫ g) ↔ P f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.RespectsIso<VAR>f g : CategoryTheory.Arrow C<VAR>e : f ≅ g<GOAL>P f.hom ↔ P g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.RespectsIso<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g<GOAL>P f ↔ P g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : ∀ (f g : CategoryTheory.Arrow C), (f ≅ g) → P f.hom → P g.hom<GOAL>P.RespectsIso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.isoClosure = P ↔ P.RespectsIso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.RespectsIso<GOAL>P.isoClosure = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.isoClosure.isoClosure = P.isoClosure
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : CategoryTheory.MorphismProperty C<VAR>Q.RespectsIso<GOAL>P.isoClosure ≤ Q ↔ P ≤ Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty C<VAR>F : C ⥤ D<VAR>Q : CategoryTheory.MorphismProperty D<VAR>Q.RespectsIso<GOAL>P.map F ≤ Q ↔ P ≤ Q.inverseImage F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty C<VAR>F : C ⥤ D<GOAL>P.isoClosure.map F = P.map F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.map (𝟭 C) = P.isoClosure
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.RespectsIso<GOAL>P.map (𝟭 C) = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>P : CategoryTheory.MorphismProperty C<VAR>F : C ⥤ D<VAR>E : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} E<VAR>G : D ⥤ E<GOAL>(P.map F).map G = P.map (F ⋙ G)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty C<VAR>F G : C ⥤ D<VAR>e : F ≅ G<GOAL>P.map F = P.map G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty D<VAR>F : C ⥤ D<GOAL>(P.inverseImage F).map F ≤ P.isoClosure
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty D<VAR>P.RespectsIso<VAR>E : C ≌ D<GOAL>P.inverseImage E.functor = P.map E.inverse
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Q : CategoryTheory.MorphismProperty C<VAR>Q.RespectsIso<VAR>E : C ≌ D<GOAL>Q.inverseImage E.inverse = Q.map E.functor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty D<VAR>P.RespectsIso<VAR>F : C ⥤ D<VAR>F.IsEquivalence<GOAL>(P.inverseImage F).map F = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.RespectsIso<VAR>F : C ⥤ D<VAR>F.IsEquivalence<GOAL>(P.map F).inverseImage F = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MorphismProperty.isomorphisms C f ↔ CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MorphismProperty.monomorphisms C f ↔ CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MorphismProperty.epimorphisms C f ↔ CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.IsIso f<GOAL>CategoryTheory.MorphismProperty.isomorphisms C f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.Mono f<GOAL>CategoryTheory.MorphismProperty.monomorphisms C f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.Epi f<GOAL>CategoryTheory.MorphismProperty.epimorphisms C f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>CategoryTheory.IsIso (α.app X) ↔ CategoryTheory.IsIso (α.app Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>P Q : CategoryTheory.MorphismProperty C<VAR>F : CategoryTheory.Functor C D<VAR>hQ : Q.IsInvertedBy F<VAR>h : P ≤ Q<GOAL>P.IsInvertedBy F
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} C₃<VAR>W : CategoryTheory.MorphismProperty C₁<VAR>F : CategoryTheory.Functor C₁ C₂<VAR>hF : W.IsInvertedBy F<VAR>G : CategoryTheory.Functor C₂ C₃<GOAL>W.IsInvertedBy (F.comp G)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L : CategoryTheory.Functor C D<VAR>h : W.IsInvertedBy L<GOAL>W.op.IsInvertedBy L.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L : CategoryTheory.Functor Cᵒᵖ D<VAR>h : W.op.IsInvertedBy L<GOAL>W.IsInvertedBy L.rightOp
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L : CategoryTheory.Functor C Dᵒᵖ<VAR>h : W.IsInvertedBy L<GOAL>W.op.IsInvertedBy L.leftOp
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>h : W.op.IsInvertedBy L<GOAL>W.IsInvertedBy L.unop
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>CategoryTheory.Category.{u_7, u_3} E₁<VAR>CategoryTheory.Category.{u_8, u_4} E₂<VAR>F₁ : CategoryTheory.Functor C₁ E₁<VAR>F₂ : CategoryTheory.Functor C₂ E₂<VAR>h₁ : W₁.IsInvertedBy F₁<VAR>h₂ : W₂.IsInvertedBy F₂<GOAL>(W₁.prod W₂).IsInvertedBy (F₁.prod F₂)
<VAR>J : Type w<VAR>C : J → Type u<VAR>D : J → Type u'<VAR>(j : J) → CategoryTheory.Category.{v, u} (C j)<VAR>(j : J) → CategoryTheory.Category.{v', u'} (D j)<VAR>W : (j : J) → CategoryTheory.MorphismProperty (C j)<VAR>F : (j : J) → CategoryTheory.Functor (C j) (D j)<VAR>hF : ∀ (j : J), (W j).IsInvertedBy (F j)<GOAL>(CategoryTheory.MorphismProperty.pi W).IsInvertedBy (CategoryTheory.Functor.pi F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>F₁ F₂ : W.FunctorsInverting D<VAR>h : F₁.obj = F₂.obj<GOAL>F₁ = F₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>F₁ F₂ : W.FunctorsInverting D<VAR>α β : F₁ ⟶ F₂<VAR>h : α.app = β.app<GOAL>α = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<GOAL>W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>F : CategoryTheory.Functor C D<GOAL>W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} C₃<VAR>W : CategoryTheory.MorphismProperty C₁<VAR>F : CategoryTheory.Functor C₁ C₂<VAR>G : CategoryTheory.Functor C₂ C₃<VAR>G.ReflectsIsomorphisms<GOAL>W.IsInvertedBy (F.comp G) ↔ W.IsInvertedBy F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>F : CategoryTheory.Functor C D<GOAL>W.IsInvertedBy F ↔ W ≤ (CategoryTheory.MorphismProperty.isomorphisms D).inverseImage F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>F : CategoryTheory.Functor C D<GOAL>W.IsInvertedBy F ↔ W.map F ≤ CategoryTheory.MorphismProperty.isomorphisms D
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} C₃<VAR>W : CategoryTheory.MorphismProperty C₁<VAR>F : CategoryTheory.Functor C₁ C₂<VAR>G : CategoryTheory.Functor C₂ C₃<GOAL>(W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F.comp G)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : C} (x : X ⟶ Y), ⋯ = ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ (x : C), ((CategoryTheory.Functor.star C).obj x).as = PUnit.unit
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1})<VAR>X : C<GOAL>⋯ = ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1})<GOAL>F = G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Functor.equiv.inverse = CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{w + 1})
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Functor.equiv.unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Discrete.natIso fun i => CategoryTheory.Iso.refl (((CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C)).obj X).obj i)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C<GOAL>CategoryTheory.Functor.equiv.functor.obj F = F.obj { as := PUnit.unit }