ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt<VAR>fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i<VAR>uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E<VAR>E : CategoryTheory.Limits.Multifork I<GOAL>(CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>hK : CategoryTheory.Limits.IsLimit K<VAR>T : C<VAR>f g : T ⟶ K.pt<VAR>h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp f (K.ι a) = CategoryTheory.CategoryStruct.comp g (K.ι a)<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>hK : CategoryTheory.Limits.IsLimit K<VAR>T : C<VAR>k : (a : I.L) → T ⟶ I.left a<VAR>hk : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)<VAR>a : I.L<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (K.ι a) = k a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) I.fstPiMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) I.sndPiMap
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>K : CategoryTheory.Limits.Multifork I<GOAL>K.toPiFork.pt = K.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>K.toPiFork.ι = CategoryTheory.Limits.Pi.lift K.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>K.toPiFork.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) I.fstPiMap
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap<GOAL>(CategoryTheory.Limits.Multifork.ofPiFork I c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap<VAR>a : I.L<GOAL>(CategoryTheory.Limits.Multifork.ofPiFork I c).ι a = CategoryTheory.CategoryStruct.comp c.ι (CategoryTheory.Limits.Pi.π I.left a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap<VAR>a : I.R<GOAL>(CategoryTheory.Limits.Multifork.ofPiFork I c).π.app (CategoryTheory.Limits.WalkingMulticospan.right a) = CategoryTheory.CategoryStruct.comp c.ι (CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right a))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>K : CategoryTheory.Limits.Multifork I<GOAL>I.toPiForkFunctor.obj K = K.toPiFork
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>K₁ K₂ : CategoryTheory.Limits.Multifork I<VAR>f : K₁ ⟶ K₂<GOAL>(I.toPiForkFunctor.map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>K₁ K₂ : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap<VAR>f : K₁ ⟶ K₂<GOAL>(I.ofPiForkFunctor.map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap<GOAL>I.ofPiForkFunctor.obj c = CategoryTheory.Limits.Multifork.ofPiFork I c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>I.multiforkEquivPiFork.functor = I.toPiForkFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>I.multiforkEquivPiFork.counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl ((I.ofPiForkFunctor.comp I.toPiForkFunctor).obj K).pt) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>I.multiforkEquivPiFork.inverse = I.ofPiForkFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>I.multiforkEquivPiFork.unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>b : I.R<GOAL>K.ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = K.π b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>a : I.L<GOAL>K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>a : I.L<GOAL>K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K₁ K₂ : CategoryTheory.Limits.Multicofork I<VAR>f : K₁ ⟶ K₂<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp (K₁.π b) f.hom = K₂.π b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>P : C<VAR>π : (b : I.R) → I.right b ⟶ P<VAR>w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))<GOAL>(CategoryTheory.Limits.Multicofork.ofπ I P π w).pt = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>P : C<VAR>π : (b : I.R) → I.right b ⟶ P<VAR>w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))<VAR>x : CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom<GOAL>(CategoryTheory.Limits.Multicofork.ofπ I P π w).ι.app x = match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) | CategoryTheory.Limits.WalkingMultispan.right b => π b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>a : I.L<GOAL>CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt<VAR>fac : ∀ (E : CategoryTheory.Limits.Multicofork I) (i : I.R), CategoryTheory.CategoryStruct.comp (K.π i) (desc E) = E.π i<VAR>uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (K.π i) m = E.π i) → m = desc E<VAR>E : CategoryTheory.Limits.Multicofork I<GOAL>(CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq).desc E = desc E
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<GOAL>CategoryTheory.CategoryStruct.comp I.fstSigmaMap (CategoryTheory.Limits.Sigma.desc K.π) = CategoryTheory.CategoryStruct.comp I.sndSigmaMap (CategoryTheory.Limits.Sigma.desc K.π)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>K : CategoryTheory.Limits.Multicofork I<GOAL>K.toSigmaCofork.pt = K.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>K : CategoryTheory.Limits.Multicofork I<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<GOAL>K.toSigmaCofork.π = CategoryTheory.Limits.Sigma.desc K.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap<GOAL>(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap<VAR>a : I.L<GOAL>(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left a) (CategoryTheory.CategoryStruct.comp I.fstSigmaMap c.π)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap<VAR>b : I.R<GOAL>(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap<VAR>b : I.R<GOAL>(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).π b = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>K : CategoryTheory.Limits.Multicofork I<GOAL>I.toSigmaCoforkFunctor.obj K = K.toSigmaCofork
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>K₁ K₂ : CategoryTheory.Limits.Multicofork I<VAR>f : K₁ ⟶ K₂<GOAL>(I.toSigmaCoforkFunctor.map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>K₁ K₂ : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap<VAR>f : K₁ ⟶ K₂<GOAL>(I.ofSigmaCoforkFunctor.map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap<GOAL>I.ofSigmaCoforkFunctor.obj c = CategoryTheory.Limits.Multicofork.ofSigmaCofork I c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<GOAL>I.multicoforkEquivSigmaCofork.inverse = I.ofSigmaCoforkFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<GOAL>I.multicoforkEquivSigmaCofork.functor = I.toSigmaCoforkFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<GOAL>I.multicoforkEquivSigmaCofork.counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl ((I.ofSigmaCoforkFunctor.comp I.toSigmaCoforkFunctor).obj K).pt) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<GOAL>I.multicoforkEquivSigmaCofork.unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multicofork I)).obj K).pt) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>a : I.L<GOAL>(CategoryTheory.Limits.Multiequalizer.multifork I).ι a = CategoryTheory.Limits.Multiequalizer.ι I a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>a : I.L<GOAL>(CategoryTheory.Limits.Multiequalizer.multifork I).π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.Limits.Multiequalizer.ι I a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.sndTo b)) (I.snd b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>W : C<VAR>k : (a : I.L) → W ⟶ I.left a<VAR>h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)<VAR>a : I.L<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h) (CategoryTheory.Limits.Multiequalizer.ι I a) = k a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>W : C<VAR>i j : W ⟶ CategoryTheory.Limits.multiequalizer I<VAR>h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) = CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)<GOAL>i = j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>a : I.L<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.Limits.Pi.π I.left a) = CategoryTheory.Limits.Multiequalizer.ι I a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>b : I.R<GOAL>(CategoryTheory.Limits.Multicoequalizer.multicofork I).π b = CategoryTheory.Limits.Multicoequalizer.π I b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>b : I.R<GOAL>(CategoryTheory.Limits.Multicoequalizer.multicofork I).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>b : I.R<GOAL>CategoryTheory.Limits.colimit.ι I.multispan (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>a : I.L<GOAL>CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicoequalizer.π I (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicoequalizer.π I (I.sndFrom a))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>W : C<VAR>k : (b : I.R) → I.right b ⟶ W<VAR>h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.Limits.Multicoequalizer.desc I W k h) = k b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>W : C<VAR>i j : CategoryTheory.Limits.multicoequalizer I ⟶ W<VAR>h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j<GOAL>i = j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasMulticoequalizer I<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) = CategoryTheory.Limits.Multicoequalizer.π I b
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.kernelOpUnop f).hom = (CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.kernelOpUnop f).inv = CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.cokernelOpUnop f).inv = (CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.cokernelOpUnop f).hom = CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.kernelUnopOp g).inv = CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.kernelUnopOp g).hom = (CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.cokernelUnopOp g).inv = (CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.cokernelUnopOp g).hom = CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.cokernel.π f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelOpUnop f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.kernel.ι f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.kernelOpUnop f).inv)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.kernelOpOp f).inv = CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.kernelOpOp f).hom = (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.cokernelOpOp f).hom = CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.cokernelOpOp f).inv = (CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.kernelUnopUnop g).hom = (CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.kernelUnopUnop g).inv = CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.Limits.kernel.ι g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) (CategoryTheory.kernelUnopOp g).inv)