ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>X Y : C<VAR>P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>P' : C<VAR>inl' : X ⟶ P'<VAR>inr' : Y ⟶ P'<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>h' : CategoryTheory.IsPushout f g inl' inr'<GOAL>inr ≫ (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom = inr'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>X Y : C<VAR>P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>P' : C<VAR>inl' : X ⟶ P'<VAR>inr' : Y ⟶ P'<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>h' : CategoryTheory.IsPushout f g inl' inr'<GOAL>inl' ≫ (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv = inl
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>X Y : C<VAR>P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>P' : C<VAR>inl' : X ⟶ P'<VAR>inr' : Y ⟶ P'<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>h' : CategoryTheory.IsPushout f g inl' inr'<GOAL>inr' ≫ (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv = inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.inl f g ≫ h.isoPushout.inv = inl
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.inr f g ≫ h.isoPushout.inv = inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>inl ≫ h.isoPushout.hom = CategoryTheory.Limits.pushout.inl f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>inr ≫ h.isoPushout.hom = CategoryTheory.Limits.pushout.inr f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.CommSq f g inl inr<VAR>CategoryTheory.Limits.HasPushout f g<VAR>i : P ≅ CategoryTheory.Limits.pushout f g<VAR>w₁ : inl ≫ i.hom = CategoryTheory.Limits.pushout.inl f g<VAR>w₂ : inr ≫ i.hom = CategoryTheory.Limits.pushout.inr f g<GOAL>CategoryTheory.IsPushout f g inl inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>Z' X' Y' P' : C<VAR>f' : Z' ⟶ X'<VAR>g' : Z' ⟶ Y'<VAR>inl' : X' ⟶ P'<VAR>inr' : Y' ⟶ P'<VAR>e₁ : Z ≅ Z'<VAR>e₂ : X ≅ X'<VAR>e₃ : Y ≅ Y'<VAR>e₄ : P ≅ P'<VAR>commf : f ≫ e₂.hom = e₁.hom ≫ f'<VAR>commg : g ≫ e₃.hom = e₁.hom ≫ g'<VAR>comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'<VAR>comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'<GOAL>CategoryTheory.IsPushout f' g' inl' inr'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<GOAL>CategoryTheory.IsPullback snd fst g f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.IsPullback fst snd f g ↔ CategoryTheory.IsPullback snd fst g f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPullback 0 0 (𝟙 X) 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPullback 0 0 0 (𝟙 X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPullback 0 (𝟙 X) 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPullback (𝟙 X) 0 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁<VAR>t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁<GOAL>CategoryTheory.IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁<VAR>t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂<GOAL>CategoryTheory.IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁<VAR>p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁<VAR>t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁<GOAL>CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)<VAR>p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁<VAR>t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂<GOAL>CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁<VAR>e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁<GOAL>CategoryTheory.IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂<VAR>e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁<GOAL>CategoryTheory.IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>h₁₃ : X₁₁ ⟶ X₁₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)<VAR>t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂<GOAL>CategoryTheory.IsPullback (t.lift h₁₃ (v₁₁ ≫ h₂₁) ⋯) v₁₁ v₁₂ h₂₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₃₁ : X₁₁ ⟶ X₃₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁<VAR>t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁<GOAL>CategoryTheory.IsPullback h₁₁ (t.lift (h₁₁ ≫ v₁₂) v₃₁ ⋯) v₁₂ h₂₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPullback b.fst b.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPullback CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPullback b.inl 0 b.snd 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPullback b.inr 0 b.fst 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPullback 0 0 b.inl b.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPullback 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<GOAL>CategoryTheory.IsPushout g.op f.op snd.op fst.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : Cᵒᵖ<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<GOAL>CategoryTheory.IsPushout g.unop f.unop snd.unop fst.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso snd<VAR>CategoryTheory.IsIso f<VAR>sq : CategoryTheory.CommSq fst snd f g<GOAL>CategoryTheory.IsPullback fst snd f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Z : C<VAR>f : X ⟶ Z<GOAL>CategoryTheory.IsPullback (𝟙 X) f f (𝟙 Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Z : C<VAR>f : X ⟶ Z<GOAL>CategoryTheory.IsPullback f (𝟙 X) (𝟙 Z) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<GOAL>CategoryTheory.IsPushout g f inr inl
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<GOAL>CategoryTheory.IsPushout f g inl inr ↔ CategoryTheory.IsPushout g f inr inl
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPushout 0 (𝟙 X) 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPushout (𝟙 X) 0 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPushout 0 0 (𝟙 X) 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.IsPushout 0 0 0 (𝟙 X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<VAR>t : CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁<GOAL>CategoryTheory.IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<VAR>t : CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂<GOAL>CategoryTheory.IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁<VAR>p : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁<VAR>t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)<VAR>p : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂<VAR>t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<VAR>e : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁<GOAL>CategoryTheory.IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<VAR>e : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂<GOAL>CategoryTheory.IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₂ ⟶ X₃₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>s : CategoryTheory.IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁<VAR>t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>CategoryTheory.IsPushout h₂₁ v₂₁ (t.desc v₁₃ (v₂₁ ≫ h₃₁) ⋯) h₃₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₃ : X₂₁ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : CategoryTheory.IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃<VAR>t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ (t.desc (h₁₂ ≫ v₁₃) h₂₃ ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPushout 0 0 b.inl b.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPushout b.inl 0 b.snd 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPushout b.inr 0 b.fst 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.IsPushout b.fst b.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<GOAL>CategoryTheory.IsPullback inr.op inl.op g.op f.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : Cᵒᵖ<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<GOAL>CategoryTheory.IsPullback inr.unop inl.unop g.unop f.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.IsIso inr<VAR>sq : CategoryTheory.CommSq f g inl inr<GOAL>CategoryTheory.IsPushout f g inl inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>CategoryTheory.IsIso g<VAR>CategoryTheory.IsIso inl<VAR>sq : CategoryTheory.CommSq f g inl inr<GOAL>CategoryTheory.IsPushout f g inl inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X : C<VAR>f : Z ⟶ X<GOAL>CategoryTheory.IsPushout (𝟙 Z) f f (𝟙 X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X : C<VAR>f : Z ⟶ X<GOAL>CategoryTheory.IsPushout f (𝟙 Z) (𝟙 X) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X : C<VAR>f : X ⟶ Z<GOAL>CategoryTheory.IsPushout f (𝟙 X) (𝟙 Z) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X : C<VAR>f : X ⟶ Z<GOAL>CategoryTheory.IsPushout (𝟙 X) f f (𝟙 Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p₁ : CategoryTheory.IsPullback f g h i<VAR>p₂ : CategoryTheory.IsPushout f g h i<GOAL>CategoryTheory.BicartesianSq f g h i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p : CategoryTheory.BicartesianSq f g h i<GOAL>CategoryTheory.BicartesianSq g f i h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.BicartesianSq b.fst b.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>CategoryTheory.BicartesianSq 0 0 b.inl b.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.BicartesianSq CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.BicartesianSq 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F<VAR>s : CategoryTheory.IsPullback f g h i<GOAL>CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F<VAR>s : CategoryTheory.IsPushout f g h i<GOAL>CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F<VAR>e : f ≫ h = g ≫ i<VAR>H : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>CategoryTheory.IsPullback f g h i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F<VAR>F.Faithful<VAR>H : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>CategoryTheory.IsPullback f g h i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F<VAR>CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F<VAR>e : f ≫ h = g ≫ i<GOAL>CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPullback f g h i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F<VAR>e : f ≫ h = g ≫ i<VAR>H : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>CategoryTheory.IsPushout f g h i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F<VAR>F.Faithful<VAR>H : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>CategoryTheory.IsPushout f g h i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F<VAR>CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F<VAR>e : f ≫ h = g ≫ i<GOAL>CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPushout f g h i