ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g h : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>CategoryTheory.Limits.HasCoproduct h<VAR>p : α → β<VAR>q : (a : α) → f a ⟶ g (p a)<VAR>q' : (b : β) → g b ⟶ h b<GOAL>CategoryTheory.Limits.Sigma.map' p q ≫ CategoryTheory.Limits.Sigma.map q' = CategoryTheory.Limits.Sigma.map' p fun a => q a ≫ q' (p a)
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : α → C<VAR>h : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>CategoryTheory.Limits.HasCoproduct h<VAR>p : α → β<VAR>q : (a : α) → f a ⟶ g a<VAR>q' : (a : α) → g a ⟶ h (p a)<GOAL>CategoryTheory.Limits.Sigma.map q ≫ CategoryTheory.Limits.Sigma.map' p q' = CategoryTheory.Limits.Sigma.map' p fun a => q a ≫ q' a
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>p p' : α → β<VAR>q : (a : α) → f a ⟶ g (p a)<VAR>q' : (a : α) → f a ⟶ g (p' a)<VAR>hp : p = p'<VAR>hq : ∀ (a : α), q a ≫ CategoryTheory.eqToHom ⋯ = q' a<GOAL>CategoryTheory.Limits.Sigma.map' p q = CategoryTheory.Limits.Sigma.map' p' q'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u_1<VAR>K : Type u_2<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<GOAL>(CategoryTheory.Limits.Pi.whiskerEquiv e w).hom = CategoryTheory.Limits.Pi.map' ⇑e.symm fun k => (w (e.symm k)).inv ≫ CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u_1<VAR>K : Type u_2<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<GOAL>(CategoryTheory.Limits.Pi.whiskerEquiv e w).inv = CategoryTheory.Limits.Pi.map' ⇑e fun j => (w j).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u_1<VAR>K : Type u_2<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<GOAL>(CategoryTheory.Limits.Sigma.whiskerEquiv e w).inv = CategoryTheory.Limits.Sigma.map' ⇑e.symm fun k => CategoryTheory.eqToHom ⋯ ≫ (w (e.symm k)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u_1<VAR>K : Type u_2<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<GOAL>(CategoryTheory.Limits.Sigma.whiskerEquiv e w).hom = CategoryTheory.Limits.Sigma.map' ⇑e fun j => (w j).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>f : ι → Type u_2<VAR>g : (i : ι) → f i → C<VAR>∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)<VAR>CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i<GOAL>(CategoryTheory.Limits.piPiIso f g).inv = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.Limits.Pi.π (fun p => g p.fst p.snd) ⟨i, x⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>f : ι → Type u_2<VAR>g : (i : ι) → f i → C<VAR>∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)<VAR>CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i<GOAL>(CategoryTheory.Limits.piPiIso f g).hom = CategoryTheory.Limits.Pi.lift fun x => match x with | ⟨i, x⟩ => CategoryTheory.Limits.Pi.π (fun i => ∏ᶜ g i) i ≫ CategoryTheory.Limits.Pi.π (g i) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>f : ι → Type u_2<VAR>g : (i : ι) → f i → C<VAR>∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)<VAR>CategoryTheory.Limits.HasCoproduct fun i => ∐ g i<GOAL>(CategoryTheory.Limits.sigmaSigmaIso f g).hom = CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.Limits.Sigma.ι (fun p => g p.fst p.snd) ⟨i, x⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>f : ι → Type u_2<VAR>g : (i : ι) → f i → C<VAR>∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)<VAR>CategoryTheory.Limits.HasCoproduct fun i => ∐ g i<GOAL>(CategoryTheory.Limits.sigmaSigmaIso f g).inv = CategoryTheory.Limits.Sigma.desc fun x => match x with | ⟨i, x⟩ => CategoryTheory.Limits.Sigma.ι (g i) x ≫ CategoryTheory.Limits.Sigma.ι (fun i => ∐ g i) i
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct fun b => G.obj (f b)<VAR>b : β<GOAL>CategoryTheory.Limits.piComparison G f ≫ CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b = G.map (CategoryTheory.Limits.Pi.π f b)
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct fun b => G.obj (f b)<VAR>P : C<VAR>g : (j : β) → P ⟶ f j<GOAL>G.map (CategoryTheory.Limits.Pi.lift g) ≫ CategoryTheory.Limits.piComparison G f = CategoryTheory.Limits.Pi.lift fun j => G.map (g j)
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)<VAR>b : β<GOAL>CategoryTheory.Limits.Sigma.ι (fun b => G.obj (f b)) b ≫ CategoryTheory.Limits.sigmaComparison G f = G.map (CategoryTheory.Limits.Sigma.ι f b)
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)<VAR>P : C<VAR>g : (j : β) → f j ⟶ P<GOAL>CategoryTheory.Limits.sigmaComparison G f ≫ G.map (CategoryTheory.Limits.Sigma.desc g) = CategoryTheory.Limits.Sigma.desc fun j => G.map (g j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<GOAL>CategoryTheory.Limits.HasProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasCoproducts C<GOAL>CategoryTheory.Limits.HasCoproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f<VAR>lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f)<GOAL>CategoryTheory.Limits.HasProducts C
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.limitConeOfUnique f).cone.pt = f default
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.limitConeOfUnique f).cone.π = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)<GOAL>(CategoryTheory.Limits.limitConeOfUnique f).isLimit.lift s = s.π.app default
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.productUniqueIso f).hom = CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor f) default
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.productUniqueIso f).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Discrete.functor f) (CategoryTheory.Limits.limitConeOfUnique f).cone
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.pt = f default
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.ι = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<VAR>s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)<GOAL>(CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.coproductUniqueIso f).inv = CategoryTheory.Limits.colimit.ι (CategoryTheory.Discrete.functor f) default
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Unique β<VAR>f : β → C<GOAL>(CategoryTheory.Limits.coproductUniqueIso f).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Discrete.functor f) (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)<VAR>b : β<GOAL>(CategoryTheory.Limits.Pi.reindex ε f).hom ≫ CategoryTheory.Limits.Pi.π f (ε b) = CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)<VAR>b : β<GOAL>(CategoryTheory.Limits.Pi.reindex ε f).inv ≫ CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b = CategoryTheory.Limits.Pi.π f (ε b)
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)<VAR>b : β<GOAL>CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b ≫ (CategoryTheory.Limits.Sigma.reindex ε f).hom = CategoryTheory.Limits.Sigma.ι f (ε b)
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)<VAR>b : β<GOAL>CategoryTheory.Limits.Sigma.ι f (ε b) ≫ (CategoryTheory.Limits.Sigma.reindex ε f).inv = CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.π.app CategoryTheory.Limits.WalkingCospan.left = c.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.π.app CategoryTheory.Limits.WalkingCospan.right = c.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.π.app CategoryTheory.Limits.WalkingCospan.one = t.fst ≫ 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>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).pt = W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<VAR>j : CategoryTheory.Limits.WalkingCospan<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app j = Option.casesOn j (fst ≫ f) fun j' => CategoryTheory.Limits.WalkingPair.casesOn j' fst snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.left = fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.right = snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.one = fst ≫ 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>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).fst = fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>W : C<VAR>fst : W ⟶ X<VAR>snd : W ⟶ Y<VAR>eq : fst ≫ f = snd ≫ g<GOAL>(CategoryTheory.Limits.PullbackCone.mk fst snd eq).snd = snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.fst ≫ f = t.snd ≫ 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>t : CategoryTheory.Limits.PullbackCone f g<VAR>W : C<VAR>k l : W ⟶ t.pt<VAR>h₀ : k ≫ t.fst = l ≫ t.fst<VAR>h₁ : k ≫ t.snd = l ≫ t.snd<VAR>j : CategoryTheory.Limits.WalkingCospan<GOAL>k ≫ t.π.app j = l ≫ t.π.app j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.eta.hom.hom = 𝟙 t.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>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.eta.inv.hom = 𝟙 t.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>t : CategoryTheory.Limits.PullbackCone f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>W : C<VAR>k l : W ⟶ t.pt<VAR>h₀ : k ≫ t.fst = l ≫ t.fst<VAR>h₁ : k ≫ t.snd = l ≫ t.snd<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w ≫ t.fst = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w ≫ t.snd = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.flip.pt = t.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>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.flip.fst = t.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<GOAL>t.flip.snd = t.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>t : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)<GOAL>(CategoryTheory.Limits.Cone.ofPullbackCone t).pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>t : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)<GOAL>(CategoryTheory.Limits.Cone.ofPullbackCone t).π = t.π ≫ (CategoryTheory.Limits.diagramIsoCospan F).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.PullbackCone.ofCone t).π = t.π ≫ (CategoryTheory.Limits.diagramIsoCospan F).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.PullbackCone.ofCone t).pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.PullbackCone.isoMk t).hom.hom = 𝟙 t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.PullbackCone.isoMk t).inv.hom = 𝟙 t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.ι.app CategoryTheory.Limits.WalkingSpan.left = c.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.ι.app CategoryTheory.Limits.WalkingSpan.right = c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>t.ι.app CategoryTheory.Limits.WalkingSpan.zero = f ≫ t.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<VAR>j : CategoryTheory.Limits.WalkingSpan<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app j = Option.casesOn j (f ≫ inl) fun j' => CategoryTheory.Limits.WalkingPair.casesOn j' inl inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).pt = W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.left = inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.right = inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.zero = f ≫ inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).inl = inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>W : C<VAR>inl : Y ⟶ W<VAR>inr : Z ⟶ W<VAR>eq : f ≫ inl = g ≫ inr<GOAL>(CategoryTheory.Limits.PushoutCocone.mk inl inr eq).inr = inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>f ≫ t.inl = g ≫ t.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>W : C<VAR>k l : t.pt ⟶ W<VAR>h₀ : t.inl ≫ k = t.inl ≫ l<VAR>h₁ : t.inr ≫ k = t.inr ≫ l<VAR>j : CategoryTheory.Limits.WalkingSpan<GOAL>t.ι.app j ≫ k = t.ι.app j ≫ l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>t.eta.inv.hom = 𝟙 t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>t.eta.hom.hom = 𝟙 t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>k l : t.pt ⟶ W<VAR>h₀ : t.inl ≫ k = t.inl ≫ l<VAR>h₁ : t.inr ≫ k = t.inr ≫ l<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>t.inl ≫ CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>t.inr ≫ CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>t.flip.pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>t.flip.inl = t.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<GOAL>t.flip.inr = t.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>t : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)<GOAL>(CategoryTheory.Limits.Cocone.ofPushoutCocone t).ι = (CategoryTheory.Limits.diagramIsoSpan F).hom ≫ t.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>t : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)<GOAL>(CategoryTheory.Limits.Cocone.ofPushoutCocone t).pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.PushoutCocone.ofCocone t).pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.PushoutCocone.ofCocone t).ι = (CategoryTheory.Limits.diagramIsoSpan F).inv ≫ t.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.PushoutCocone.isoMk t).hom.hom = 𝟙 t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.PushoutCocone.isoMk t).inv.hom = 𝟙 t.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.NormalMono f<GOAL>CategoryTheory.CategoryStruct.comp f CategoryTheory.NormalMono.g = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.NormalEpi f<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsKernelPair f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>S : C<VAR>k : CategoryTheory.IsKernelPair f a b<VAR>p q : S ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f<GOAL>CategoryTheory.CategoryStruct.comp (k.lift p q w) a = p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>S : C<VAR>k : CategoryTheory.IsKernelPair f a b<VAR>p q : S ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f<GOAL>CategoryTheory.CategoryStruct.comp (k.lift p q w) b = q