ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.59971, u_1} C<VAR>inst✝¹ : Category.{?u.59975, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>{ obj := fun X => X, map := fun {X Y} f => Hom.mk (ofHom W f) }.map (f ≫ g) = Hom.comp ({ obj := fun X => X, map := fun {X Y} f => Hom.mk (ofHom W f) }.map f) ({ obj := fun X => X, map := fun {X Y} f => Hom.mk (ofHom W f) }.map g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.59971, u_1} C<VAR>inst✝¹ : Category.{?u.59975, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>{ obj := fun X => X, map := fun {X Y} f => Hom.mk (ofHom W f) }.map (f ≫ g) = Hom.mk ((ofHom W f).comp₀ (ofHom W g) (ofHom W g))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>finrank ℝ ↥(s.altitude i).direction = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>finrank ℝ ↥((vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<VAR>h : finrank ℝ ↥(vectorSpan ℝ (s.points '' ↑(univ.erase i))) + finrank ℝ ↥((vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))<GOAL>finrank ℝ ↥((vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<VAR>h : finrank ℝ ↥(vectorSpan ℝ (s.points '' ↑(univ.erase i))) + finrank ℝ ↥((vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))<VAR>hc : (univ.erase i).card = n + 1<GOAL>finrank ℝ ↥((vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<VAR>h : finrank ℝ ↥(vectorSpan ℝ (s.points '' ↑(univ.erase i))) + finrank ℝ ↥((vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))<VAR>hc : (univ.erase i).card = n + 1<GOAL>finrank ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank ℝ ↥(vectorSpan ℝ (s.points '' ↑(univ.erase i))) + 1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<GOAL>-h ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<GOAL>⁅f, e⁆ = -h
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<GOAL>⁅-h, f⁆ = 2 • f
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<GOAL>⁅-h, e⁆ = -(2 • e)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>((toFunBilinear R A) a) p = p.sum fun n r => (monomial n) (a * (algebraMap R A) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>∑ x ∈ p.support, a • ((algebraMap R A[X]) (p.coeff x) * X ^ x) = ∑ x ∈ p.support, (monomial x) (a * (algebraMap R A) (p.coeff x))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>p : R[X]<VAR>i : ℕ<GOAL>a • ((algebraMap R A[X]) (p.coeff i) * X ^ i) = (monomial i) (a * (algebraMap R A) (p.coeff i))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>1 ≤ ⌈a⌉ ↔ 0 < a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : CliffordAlgebra 0<GOAL>reverse x = x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Zero α<VAR>inst✝ : One α<VAR>i j : l ⊕ m<GOAL>fromBlocks 1 0 0 1 i j = 1 i j
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : OplaxNatTrans F G<VAR>θ : OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<GOAL>f ◁ θ.naturality (𝟙 a) ≫ f ◁ θ.app a ◁ H.mapId a = f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<GOAL>IsAtom s ↔ ∃ a, s = {a}
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>∑ m ∈ range (n + 1), n.choose m = 2 ^ n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>this : ∑ m ∈ range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(n.choose m) = (1 + 1) ^ n<GOAL>∑ m ∈ range (n + 1), n.choose m = 2 ^ n
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : D<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : D<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) univ x‖ ≤ ‖B‖ * ∑ x_1 ∈ Finset.range (n + 1), ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>lt : cs.length (w * cs.simple i) < cs.length w<GOAL>cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>gt : cs.length (w * cs.simple i) > cs.length w<GOAL>cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : IsPeriodicPt f (n + m) x<VAR>hm : IsPeriodicPt f n x<GOAL>IsPeriodicPt f m x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : IsPeriodicPt f (m + n) x<VAR>hm : IsPeriodicPt f n x<GOAL>IsPeriodicPt f m x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<GOAL>Filter.map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s)
<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>U : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>P (f.appLE U V e) ↔ P (f.appLE U V ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<VAR>hm' : ∀ (a : α), f a ≤ m<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<VAR>hm' : ∀ (a : α), f a ≤ m<VAR>a₀ : α<GOAL>∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<VAR>hm' : ∀ (a : α), f a ≤ m<VAR>a₀ : α<VAR>h : ∀ (a : α), ∃ a', f a < f a'<GOAL>∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<VAR>hm' : ∀ (a : α), f a ≤ m<VAR>a₀ : α<VAR>h : ∀ (a : α), ∃ a', f a < f a'<GOAL>∃ a, f a₀ < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<VAR>hm' : ∀ (a : α), f a ≤ m<VAR>a₀ : α<VAR>h : ∀ (a : α), ∃ a', f a < f a'<GOAL>∀ (n : β), f a₀ ≤ n → (∃ a, n < f a) → ∃ a, succ n < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Nonempty α<VAR>inst✝³ : Preorder β<VAR>f : α → β<VAR>inst✝² : NoMaxOrder α<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>hf : StrictMono f<VAR>m : β<VAR>hm : m ∈ upperBounds (range f)<VAR>hm' : ∀ (a : α), f a ≤ m<VAR>a₀ : α<VAR>h : ∀ (a : α), ∃ a', f a < f a'<VAR>b : β<VAR>a✝ : f a₀ ≤ b<VAR>a : α<VAR>hba : b < f a<GOAL>∃ a, succ b < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : NonAssocSemiring S<VAR>inst✝¹ : FunLike F ℕ R<VAR>inst✝ : RingHomClass F ℕ R<VAR>f g : F<GOAL>f 1 = g 1
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h₁ : g' =ᶠ[𝓝 x] g<GOAL>g' =ᶠ[𝓝[univ] x] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β → α → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => ∫⁻ (a : β) in s, f a b ∂κ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β → α → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => ∫⁻ (a : β), f a b ∂(κ.restrict hs) b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>Δ₁ Δ₂ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ₁<VAR>p : Δ₁ ⟶ Δ₂<VAR>inst✝ : Epi p.unop<GOAL>(s.ι (unop A.fst).len ≫ X.map A.e.op) ≫ X.map p = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>Δ₁ Δ₂ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ₁<VAR>p : Δ₁ ⟶ Δ₂<VAR>inst✝ : Epi p.unop<GOAL>s.ι (unop A.fst).len ≫ X.map (A.e.op ≫ p) = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<GOAL>map m (comap m f) = f ⊓ 𝓟 (range m)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<GOAL>f ⊓ 𝓟 (range m) ≤ map m (comap m f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t✝ : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>t' t : Set β<VAR>ht : t ∈ f<VAR>sub : m ⁻¹' t ⊆ m ⁻¹' t'<GOAL>t' ∈ f ⊓ 𝓟 (range m)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t✝ : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>t' t : Set β<VAR>ht : t ∈ f<VAR>sub : m ⁻¹' t ⊆ m ⁻¹' t'<GOAL>t ⊆ {x | x ∈ range m → x ∈ t'}
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂ : Epi (app' φ 2 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<GOAL>Epi (app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂ : Epi (app' φ 2 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<GOAL>∀ ⦃A : C⦄ (y : A ⟶ R₂.obj' 1 ⋯), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂ : Epi (app' φ 2 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂ : Epi (app' φ 2 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝¹ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝ : Epi π₂<VAR>f₁ : A₂ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).f<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝¹ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝ : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝¹ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝ : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝² : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝¹ : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝ : Epi π₃<VAR>g₀ : A₃ ⟶ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>h₅ : π₃ ≫ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) = g₀ ≫ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).f<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝² : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝¹ : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝ : Epi π₃<VAR>g₀ : A₃ ⟶ R₂.obj 0<VAR>h₅ : π₃ ≫ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ φ.app 1) = g₀ ≫ R₂.map (homOfLE ⋯)<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝² : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝¹ : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝ : Epi π₃<VAR>g₀ : A₃ ⟶ R₂.obj 0<VAR>h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝³ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝² : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝¹ : Epi π₃<VAR>g₀ : A₃ ⟶ R₂.obj 0<VAR>h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)<VAR>A₄ : C<VAR>π₄ : A₄ ⟶ A₃<VAR>w✝ : Epi π₄<VAR>f₀ : A₄ ⟶ R₁.obj' 0 ⋯<VAR>h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯