ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.NormalMonoCategory C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι 0 ⋯)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.NormalEpiCategory C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0<GOAL>CategoryTheory.Mono f
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Limits.HasEqualizers A<VAR>CategoryTheory.Limits.HasImages A<VAR>CategoryTheory.StrongEpiCategory B<VAR>CategoryTheory.Limits.HasImages B<VAR>L : CategoryTheory.Functor A B<VAR>{X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L<VAR>{X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.PreservesImage.iso L f).hom = CategoryTheory.Limits.image.lift (CategoryTheory.Limits.MonoFactorisation.mk (L.obj (CategoryTheory.Limits.image f)) (L.map (CategoryTheory.Limits.image.ι f)) (L.map (CategoryTheory.Limits.factorThruImage f)) ⋯)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Limits.HasEqualizers A<VAR>CategoryTheory.Limits.HasImages A<VAR>CategoryTheory.StrongEpiCategory B<VAR>CategoryTheory.Limits.HasImages B<VAR>L : CategoryTheory.Functor A B<VAR>{X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L<VAR>{X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.PreservesImage.iso L f).inv = (CategoryTheory.Limits.StrongEpiMonoFactorisation.mk (CategoryTheory.Limits.MonoFactorisation.mk (L.obj (CategoryTheory.Limits.image f)) (L.map (CategoryTheory.Limits.image.ι f)) (L.map (CategoryTheory.Limits.factorThruImage f)) ⋯)).toMonoIsImage.lift (CategoryTheory.Limits.Image.monoFactorisation (L.map f))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Limits.HasEqualizers A<VAR>CategoryTheory.Limits.HasImages A<VAR>CategoryTheory.StrongEpiCategory B<VAR>CategoryTheory.Limits.HasImages B<VAR>L : CategoryTheory.Functor A B<VAR>{X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L<VAR>{X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.PreservesImage.iso L f).hom = L.map (CategoryTheory.Limits.factorThruImage f)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Limits.HasEqualizers A<VAR>CategoryTheory.Limits.HasImages A<VAR>CategoryTheory.StrongEpiCategory B<VAR>CategoryTheory.Limits.HasImages B<VAR>L : CategoryTheory.Functor A B<VAR>{X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L<VAR>{X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (L.map (CategoryTheory.Limits.image.ι f)) = CategoryTheory.Limits.image.ι (L.map f)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Limits.HasEqualizers A<VAR>CategoryTheory.Limits.HasImages A<VAR>CategoryTheory.StrongEpiCategory B<VAR>CategoryTheory.Limits.HasImages B<VAR>L : CategoryTheory.Functor A B<VAR>{X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L<VAR>{X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.Limits.image.ι (L.map f)) = L.map (CategoryTheory.Limits.image.ι f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>self : F.PreservesZeroMorphisms<VAR>X Y : C<GOAL>F.map 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>X Y : C<GOAL>F.map 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>X : C<VAR>hX : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Limits.IsZero (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>F.Faithful<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : F.map f = 0<GOAL>f = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>F.Faithful<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.map f = 0 ↔ f = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F₁ F₂ : C ⥤ D<VAR>F₁.PreservesZeroMorphisms<VAR>e : F₁ ≅ F₂<GOAL>F₂.PreservesZeroMorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<GOAL>F.mapZeroObject.hom = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<GOAL>F.mapZeroObject.inv = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>i : F.obj 0 ≅ 0<GOAL>F.PreservesZeroMorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Limits.MonoFactorisation f<GOAL>CategoryTheory.Mono self.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Limits.MonoFactorisation f<GOAL>self.e ≫ self.m = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hI : F.I = F'.I<VAR>hm : F.m = CategoryTheory.eqToHom hI ≫ F'.m<GOAL>F = F'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>Y' : C<VAR>g : Y ⟶ Y'<VAR>CategoryTheory.Mono g<GOAL>(F.compMono g).I = F.I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>Y' : C<VAR>g : Y ⟶ Y'<VAR>CategoryTheory.Mono g<GOAL>(F.compMono g).e = F.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>Y' : C<VAR>g : Y ⟶ Y'<VAR>CategoryTheory.Mono g<GOAL>(F.compMono g).m = F.m ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Y' : C<VAR>g : Y ⟶ Y'<VAR>CategoryTheory.IsIso g<VAR>F : CategoryTheory.Limits.MonoFactorisation (f ≫ g)<GOAL>F.ofCompIso.e = F.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Y' : C<VAR>g : Y ⟶ Y'<VAR>CategoryTheory.IsIso g<VAR>F : CategoryTheory.Limits.MonoFactorisation (f ≫ g)<GOAL>F.ofCompIso.m = F.m ≫ CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Y' : C<VAR>g : Y ⟶ Y'<VAR>CategoryTheory.IsIso g<VAR>F : CategoryTheory.Limits.MonoFactorisation (f ≫ g)<GOAL>F.ofCompIso.I = F.I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>X' : C<VAR>g : X' ⟶ X<GOAL>(F.isoComp g).e = g ≫ F.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>X' : C<VAR>g : X' ⟶ X<GOAL>(F.isoComp g).I = F.I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>X' : C<VAR>g : X' ⟶ X<GOAL>(F.isoComp g).m = F.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<VAR>g : X' ⟶ X<VAR>CategoryTheory.IsIso g<VAR>F : CategoryTheory.Limits.MonoFactorisation (g ≫ f)<GOAL>(CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).e = CategoryTheory.inv g ≫ F.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<VAR>g : X' ⟶ X<VAR>CategoryTheory.IsIso g<VAR>F : CategoryTheory.Limits.MonoFactorisation (g ≫ f)<GOAL>(CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).I = F.I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<VAR>g : X' ⟶ X<VAR>CategoryTheory.IsIso g<VAR>F : CategoryTheory.Limits.MonoFactorisation (g ≫ f)<GOAL>(CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).m = F.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>F : CategoryTheory.Limits.MonoFactorisation f.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(F.ofArrowIso sq).e = CategoryTheory.inv sq.left ≫ F.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>F : CategoryTheory.Limits.MonoFactorisation f.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(F.ofArrowIso sq).m = F.m ≫ sq.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>F : CategoryTheory.Limits.MonoFactorisation f.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(F.ofArrowIso sq).I = F.I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>self : CategoryTheory.Limits.IsImage F<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>self.lift F' ≫ F'.m = F.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>F.e ≫ hF.lift F' = F'.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>(CategoryTheory.Limits.IsImage.self f).lift F' = F'.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>(hF.isoExt hF').inv = hF'.lift F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>(hF.isoExt hF').hom = hF.lift F'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>(hF.isoExt hF').hom ≫ F'.m = F.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>(hF.isoExt hF').inv ≫ F.m = F'.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>F.e ≫ (hF.isoExt hF').hom = F'.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>F'.e ≫ (hF.isoExt hF').inv = F.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>F : CategoryTheory.Limits.MonoFactorisation f.hom<VAR>hF : CategoryTheory.Limits.IsImage F<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<VAR>F' : CategoryTheory.Limits.MonoFactorisation g.hom<GOAL>(hF.ofArrowIso sq).lift F' = hF.lift (F'.ofArrowIso (CategoryTheory.inv sq))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>F : CategoryTheory.Limits.ImageFactorisation f.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(F.ofArrowIso sq).F = F.F.ofArrowIso sq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>F : CategoryTheory.Limits.ImageFactorisation f.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(F.ofArrowIso sq).isImage = F.isImage.ofArrowIso sq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Limits.HasImage f<GOAL>Nonempty (CategoryTheory.Limits.ImageFactorisation f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.ImageFactorisation f<GOAL>CategoryTheory.Limits.HasImage f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>h : CategoryTheory.Limits.HasImage f.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>CategoryTheory.Limits.HasImage g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>(CategoryTheory.Limits.Image.monoFactorisation f).m = CategoryTheory.Limits.image.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>(CategoryTheory.Limits.Image.monoFactorisation f).e = CategoryTheory.Limits.factorThruImage f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>CategoryTheory.Limits.factorThruImage f ≫ CategoryTheory.Limits.image.ι f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>CategoryTheory.Limits.image.lift F' ≫ F'.m = CategoryTheory.Limits.image.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>CategoryTheory.Limits.factorThruImage f ≫ CategoryTheory.Limits.image.lift F' = F'.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>F : CategoryTheory.Limits.MonoFactorisation f<GOAL>(CategoryTheory.Limits.Image.isImage f).lift F = CategoryTheory.Limits.image.lift F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>F : CategoryTheory.Limits.MonoFactorisation f<VAR>hF : CategoryTheory.Limits.IsImage F<GOAL>hF.lift (CategoryTheory.Limits.Image.monoFactorisation f) ≫ CategoryTheory.Limits.image.ι f = F.m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<VAR>l : CategoryTheory.Limits.image f ⟶ F'.I<VAR>w : l ≫ F'.m = CategoryTheory.Limits.image.ι f<GOAL>l = CategoryTheory.Limits.image.lift F'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasImages C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.HasImage f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Limits.imageMonoIsoSource f).inv ≫ CategoryTheory.Limits.image.ι f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Limits.imageMonoIsoSource f).hom ≫ f = CategoryTheory.Limits.image.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>W : C<VAR>g h : CategoryTheory.Limits.image f ⟶ W<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)<VAR>w : CategoryTheory.Limits.factorThruImage f ≫ g = CategoryTheory.Limits.factorThruImage f ≫ h<GOAL>g = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>E : CategoryTheory.Epi f<GOAL>CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)<VAR>CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f f' : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Limits.HasImage f'<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>h : f = f'<GOAL>CategoryTheory.Limits.image.ι f = (CategoryTheory.Limits.image.eqToIso h).hom ≫ CategoryTheory.Limits.image.ι f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage g<VAR>CategoryTheory.Limits.HasImage (f ≫ g)<GOAL>CategoryTheory.Limits.image.preComp f g ≫ CategoryTheory.Limits.image.ι g = CategoryTheory.Limits.image.ι (f ≫ g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage g<VAR>CategoryTheory.Limits.HasImage (f ≫ g)<GOAL>CategoryTheory.Limits.factorThruImage (f ≫ g) ≫ CategoryTheory.Limits.image.preComp f g = f ≫ CategoryTheory.Limits.factorThruImage g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>W : C<VAR>h : Z ⟶ W<VAR>CategoryTheory.Limits.HasImage (g ≫ h)<VAR>CategoryTheory.Limits.HasImage (f ≫ g ≫ h)<VAR>CategoryTheory.Limits.HasImage h<VAR>CategoryTheory.Limits.HasImage ((f ≫ g) ≫ h)<GOAL>CategoryTheory.Limits.image.preComp f (g ≫ h) ≫ CategoryTheory.Limits.image.preComp g h = CategoryTheory.Limits.image.eqToHom ⋯ ≫ CategoryTheory.Limits.image.preComp (f ≫ g) h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.image.compIso f g).hom ≫ CategoryTheory.Limits.image.ι (f ≫ g) = CategoryTheory.Limits.image.ι f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.image.compIso f g).inv ≫ CategoryTheory.Limits.image.ι f = CategoryTheory.Limits.image.ι (f ≫ g) ≫ CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>self : CategoryTheory.Limits.ImageMap sq<GOAL>self.map ≫ CategoryTheory.Limits.image.ι g.hom = CategoryTheory.Limits.image.ι f.hom ≫ sq.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>m : CategoryTheory.Limits.ImageMap sq<GOAL>CategoryTheory.Limits.factorThruImage f.hom ≫ m.map = sq.left ≫ CategoryTheory.Limits.factorThruImage g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>self : CategoryTheory.Limits.HasImageMap sq<GOAL>Nonempty (CategoryTheory.Limits.ImageMap sq)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>m : CategoryTheory.Limits.ImageMap sq<GOAL>CategoryTheory.Limits.HasImageMap sq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>F : CategoryTheory.Limits.MonoFactorisation f.hom<VAR>F' : CategoryTheory.Limits.MonoFactorisation g.hom<VAR>hF' : CategoryTheory.Limits.IsImage F'<VAR>map : F.I ⟶ F'.I<VAR>map_ι : map ≫ F'.m = F.m ≫ sq.right<GOAL>CategoryTheory.Limits.HasImageMap sq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom<VAR>map_ι : map ≫ CategoryTheory.Limits.image.ι g.hom = CategoryTheory.Limits.image.ι f.hom ≫ sq.right := by aesop_cat<VAR>map' : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom<VAR>map_ι' : map' ≫ CategoryTheory.Limits.image.ι g.hom = CategoryTheory.Limits.image.ι f.hom ≫ sq.right<GOAL>map = map'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>F G : CategoryTheory.Limits.ImageMap sq<GOAL>F.map = G.map
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom<VAR>map_ι : map ≫ CategoryTheory.Limits.image.ι g.hom = CategoryTheory.Limits.image.ι f.hom ≫ sq.right := by aesop_cat<VAR>map' : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom<VAR>map_ι' : map' ≫ CategoryTheory.Limits.image.ι g.hom = CategoryTheory.Limits.image.ι f.hom ≫ sq.right<GOAL>(map = map') = True
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.Limits.HasImageMap sq<GOAL>CategoryTheory.Limits.factorThruImage f.hom ≫ CategoryTheory.Limits.image.map sq = sq.left ≫ CategoryTheory.Limits.factorThruImage g.hom