ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>f : J → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>D : Type t<VAR>CategoryTheory.Category.{r, t} D<VAR>CategoryTheory.ConcreteCategory D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F<VAR>CategoryTheory.Limits.HasProduct fun j => F.obj (f j)<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget D)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun b => F.obj (f b)) (CategoryTheory.forget D)<VAR>x y : (CategoryTheory.forget D).obj (F.obj (∏ᶜ f))<VAR>h : ∀ (i : J), (F.map (CategoryTheory.Limits.Pi.π f i)) x = (F.map (CategoryTheory.Limits.Pi.π f i)) y<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)<VAR>X : C<VAR>h : Nonempty (CategoryTheory.Limits.IsInitial X)<GOAL>IsEmpty ((CategoryTheory.forget C).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)<VAR>X : C<VAR>h : IsEmpty ((CategoryTheory.forget C).obj X)<GOAL>Nonempty (CategoryTheory.Limits.IsInitial X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)<VAR>X : C<GOAL>Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ((CategoryTheory.forget C).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (X₁ ⨯ X₂)<GOAL>((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).1 = CategoryTheory.Limits.prod.fst x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (X₁ ⨯ X₂)<GOAL>((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).2 = CategoryTheory.Limits.prod.snd x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj X₁ × (CategoryTheory.forget C).obj X₂<GOAL>CategoryTheory.Limits.prod.fst ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) = x.1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj X₁ × (CategoryTheory.forget C).obj X₂<GOAL>CategoryTheory.Limits.prod.snd ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) = x.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ S : C<VAR>f₁ : X₁ ⟶ S<VAR>f₂ : X₂ ⟶ S<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.pullback f₁ f₂)<GOAL>∃ x₁ x₂, ∃ (h : f₁ x₁ = f₂ x₂), x = CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ S : C<VAR>f₁ : X₁ ⟶ S<VAR>f₂ : X₂ ⟶ S<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)<VAR>x₁ : (CategoryTheory.forget C).obj X₁<VAR>x₂ : (CategoryTheory.forget C).obj X₂<VAR>h : f₁ x₁ = f₂ x₂<GOAL>(CategoryTheory.Limits.pullback.fst f₁ f₂) (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) = x₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X₁ X₂ S : C<VAR>f₁ : X₁ ⟶ S<VAR>f₂ : X₂ ⟶ S<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)<VAR>x₁ : (CategoryTheory.forget C).obj X₁<VAR>x₂ : (CategoryTheory.forget C).obj X₂<VAR>h : f₁ x₁ = f₂ x₂<GOAL>(CategoryTheory.Limits.pullback.snd f₁ f₂) (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) = x₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B X f<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f) (CategoryTheory.forget C)<VAR>x y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f)<VAR>h₀ : (CategoryTheory.Limits.WidePullback.base f) x = (CategoryTheory.Limits.WidePullback.base f) y<VAR>h : ∀ (j : ι), (CategoryTheory.Limits.WidePullback.π f j) x = (CategoryTheory.Limits.WidePullback.π f j) y<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>Nonempty ι<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B X f<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f) (CategoryTheory.forget C)<VAR>x y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f)<VAR>h : ∀ (j : ι), (CategoryTheory.Limits.WidePullback.π f j) x = (CategoryTheory.Limits.WidePullback.π f j) y<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)<VAR>x y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I)<VAR>h : ∀ (t : I.L), (CategoryTheory.Limits.Multiequalizer.ι I t) x = (CategoryTheory.Limits.Multiequalizer.ι I t) y<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasMultiequalizer I<VAR>CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I)<VAR>i : I.L<GOAL>↑((CategoryTheory.Limits.Concrete.multiequalizerEquiv I) x) i = (CategoryTheory.Limits.Multiequalizer.ι I i) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>CategoryTheory.Limits.HasWidePushout B X f<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePushout B X f)<GOAL>(∃ y, (CategoryTheory.Limits.WidePushout.head f) y = x) ∨ ∃ i y, (CategoryTheory.Limits.WidePushout.ι f i) y = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>Nonempty α<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>CategoryTheory.Limits.HasWidePushout B X f<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePushout B X f)<GOAL>∃ i y, (CategoryTheory.Limits.WidePushout.ι f i) y = x
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.ConcreteCategory C<VAR>M N K : C<VAR>f : M ⟶ N<VAR>CategoryTheory.Limits.HasCokernel f<VAR>g h : CategoryTheory.Limits.cokernel f ⟶ K<VAR>w : ∀ (n : (CategoryTheory.forget C).obj N), g ((CategoryTheory.Limits.cokernel.π f) n) = h ((CategoryTheory.Limits.cokernel.π f) n)<GOAL>g = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.IsPullback ↔ Nonempty (CategoryTheory.Limits.IsLimit sq.pullbackCone)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.IsPushout ↔ Nonempty (CategoryTheory.Limits.IsColimit sq.pushoutCocone)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<VAR>h : CategoryTheory.Limits.IsLimit sq.pullbackCone<GOAL>sq.IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<VAR>h : CategoryTheory.Limits.IsColimit sq.pushoutCocone<GOAL>sq.IsPushout
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>h : sq₁.IsPullback<VAR>e : sq₁ ≅ sq₂<GOAL>sq₂.IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.IsPullback ↔ sq₂.IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>h : sq₁.IsPushout<VAR>e : sq₁ ≅ sq₂<GOAL>sq₂.IsPushout
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.IsPushout ↔ sq₂.IsPushout
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<VAR>h : sq.IsPushout<GOAL>sq.op.IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<VAR>h : sq.IsPushout<GOAL>sq.unop.IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<VAR>h : sq.IsPullback<GOAL>sq.op.IsPushout
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<VAR>h : sq.IsPullback<GOAL>sq.unop.IsPushout
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pullbackConeOfLeftIso f g).fst = g ≫ CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pullbackConeOfLeftIso f g).snd = 𝟙 (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app none = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.left = g ≫ CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.right = 𝟙 (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt).obj CategoryTheory.Limits.WalkingCospan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Limits.HasPullback f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g) ≫ CategoryTheory.Limits.pullback.fst f g = g ≫ CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pullbackConeOfRightIso f g).pt = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pullbackConeOfRightIso f g).fst = 𝟙 (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pullbackConeOfRightIso f g).snd = f ≫ CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app none = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.left = 𝟙 (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt).obj CategoryTheory.Limits.WalkingCospan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.right = f ≫ CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>CategoryTheory.Limits.HasPullback f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>CategoryTheory.inv (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g = f ≫ CategoryTheory.inv g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).pt = Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).inl = CategoryTheory.inv f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).inr = 𝟙 Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app none = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app CategoryTheory.Limits.WalkingSpan.left = CategoryTheory.inv f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app CategoryTheory.Limits.WalkingSpan.right = 𝟙 ((CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Limits.HasPushout f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Limits.pushout.inl f g ≫ CategoryTheory.inv (CategoryTheory.Limits.pushout.inr f g) = CategoryTheory.inv f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).pt = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).inl = 𝟙 Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).inr = CategoryTheory.inv g ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app none = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app CategoryTheory.Limits.WalkingSpan.left = 𝟙 ((CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app CategoryTheory.Limits.WalkingSpan.right = CategoryTheory.inv g ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>CategoryTheory.Limits.HasPushout f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>CategoryTheory.Limits.pushout.inr f g ≫ CategoryTheory.inv (CategoryTheory.Limits.pushout.inl f g) = CategoryTheory.inv g ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x), CategoryTheory.FunctorToTypes.prod.fst.app x a = a.1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x), CategoryTheory.FunctorToTypes.prod.snd.app x a = a.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>τ₁ : F ⟶ F₁<VAR>τ₂ : F ⟶ F₂<VAR>x : C<VAR>y : F.obj x<GOAL>(CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂).app x y = (τ₁.app x y, τ₂.app x y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>τ₁ : F ⟶ F₁<VAR>τ₂ : F ⟶ F₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂) CategoryTheory.FunctorToTypes.prod.fst = τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>τ₁ : F ⟶ F₁<VAR>τ₂ : F ⟶ F₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂) CategoryTheory.FunctorToTypes.prod.snd = τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<GOAL>(CategoryTheory.FunctorToTypes.binaryProductCone F G).pt.obj a = (F.obj a × G.obj a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : C} (f : X ⟶ Y) (a : F.obj X × G.obj X), (CategoryTheory.FunctorToTypes.binaryProductCone F G).pt.map f a = (F.map f a.1, G.map f a.2)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair), (CategoryTheory.FunctorToTypes.binaryProductCone F G).π.app x = match x.as with | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.FunctorToTypes.prod.fst | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.FunctorToTypes.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>s : CategoryTheory.Limits.BinaryFan F G<GOAL>(CategoryTheory.FunctorToTypes.binaryProductLimit F G).lift s = CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).hom CategoryTheory.FunctorToTypes.prod.fst = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).hom CategoryTheory.FunctorToTypes.prod.snd = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).inv CategoryTheory.Limits.prod.fst = CategoryTheory.FunctorToTypes.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z : (CategoryTheory.FunctorToTypes.prod F G).obj a<GOAL>CategoryTheory.Limits.prod.fst.app a ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a z) = z.1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).inv CategoryTheory.Limits.prod.snd = CategoryTheory.FunctorToTypes.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z : (CategoryTheory.FunctorToTypes.prod F G).obj a<GOAL>CategoryTheory.Limits.prod.snd.app a ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a z) = z.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>x : F.obj a<VAR>y : G.obj a<GOAL>CategoryTheory.Limits.prod.fst.app a (CategoryTheory.FunctorToTypes.prodMk x y) = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>x : F.obj a<VAR>y : G.obj a<GOAL>CategoryTheory.Limits.prod.snd.app a (CategoryTheory.FunctorToTypes.prodMk x y) = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z w : (CategoryTheory.FunctorToTypes.prod F G).obj a<VAR>h1 : z.1 = w.1<VAR>h2 : z.2 = w.2<GOAL>z = w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z : F.obj a × G.obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryProductEquiv F G a).symm z = CategoryTheory.FunctorToTypes.prodMk z.1 z.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z : (F ⨯ G).obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryProductEquiv F G a) z = (((CategoryTheory.FunctorToTypes.binaryProductIso F G).hom.app a z).1, ((CategoryTheory.FunctorToTypes.binaryProductIso F G).hom.app a z).2)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z w : (F ⨯ G).obj a<VAR>h1 : CategoryTheory.Limits.prod.fst.app a z = CategoryTheory.Limits.prod.fst.app a w<VAR>h2 : CategoryTheory.Limits.prod.snd.app a z = CategoryTheory.Limits.prod.snd.app a w<GOAL>z = w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ (x : C) (x_1 : F.obj x), CategoryTheory.FunctorToTypes.coprod.inl.app x x_1 = Sum.inl x_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ (x : C) (x_1 : G.obj x), CategoryTheory.FunctorToTypes.coprod.inr.app x x_1 = Sum.inr x_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>τ₁ : F₁ ⟶ F<VAR>τ₂ : F₂ ⟶ F<VAR>a : C<VAR>x : (CategoryTheory.FunctorToTypes.coprod F₁ F₂).obj a<GOAL>(CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂).app a x = Sum.casesOn (motive := fun t => x = t → F.obj a) x (fun x_1 h => τ₁.app a x_1) (fun x_1 h => τ₂.app a x_1) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>τ₁ : F₁ ⟶ F<VAR>τ₂ : F₂ ⟶ F<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inl (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) = τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F₁ F₂ : CategoryTheory.Functor C (Type w)<VAR>τ₁ : F₁ ⟶ F<VAR>τ₂ : F₂ ⟶ F<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inr (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) = τ₂