ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (α : Type u_4) → [inst : Fintype α] → Prop<VAR>hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α<VAR>hstep : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>hn : card α = n<GOAL>P α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (α : Type u_4) → [inst : Fintype α] → Prop<VAR>hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α<VAR>hstep : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>hn : card α = n<VAR>hsing : Subsingleton α<GOAL>P α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (α : Type u_4) → [inst : Fintype α] → Prop<VAR>hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α<VAR>hstep : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>hn : card α = n<VAR>hnontriv : Nontrivial α<GOAL>P α
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<GOAL>Multiset.map Subtype.val (factors' a) = Multiset.map Associates.mk (factors a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : f ≤ᶠ[ae μ] 0<GOAL>∫ (a : α), f a ∂μ ≤ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf✝ : f ≤ᶠ[ae μ] 0<VAR>hf : 0 ≤ᶠ[ae μ] -f<GOAL>∫ (a : α), f a ∂μ ≤ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf✝ : f ≤ᶠ[ae μ] 0<VAR>hf : 0 ≤ᶠ[ae μ] -f<VAR>this : 0 ≤ ∫ (a : α), -f a ∂μ<GOAL>∫ (a : α), f a ∂μ ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>A : Set α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>A : Set α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>H : μ A = ⊤<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>A : Set α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>H : μ A ≠ ⊤<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s : ι → M<VAR>indep : Set ι → Prop := fun I => LinearIndependent (ι := ↑I) R (s ∘ Subtype.val)<VAR>X : Type u' := { I // indep I }<VAR>r : X → X → Prop := fun I J => ↑I ⊆ ↑J<VAR>key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, ↑I)<GOAL>∃ I, (LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun (x : ↑J) => s ↑x) → I = J
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s : ι → M<VAR>indep : Set ι → Prop := fun I => LinearIndependent (ι := ↑I) R (s ∘ Subtype.val)<VAR>X : Type u' := { I // indep I }<VAR>r : X → X → Prop := fun I J => ↑I ⊆ ↑J<VAR>key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, ↑I)<VAR>trans : Transitive r<GOAL>∃ I, (LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun (x : ↑J) => s ↑x) → I = J
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s : ι → M<VAR>indep : Set ι → Prop := fun I => LinearIndependent (ι := ↑I) R (s ∘ Subtype.val)<VAR>X : Type u' := { I // indep I }<VAR>r : X → X → Prop := fun I J => ↑I ⊆ ↑J<VAR>key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, ↑I)<VAR>trans : Transitive r<VAR>I : Set ι<VAR>hli : indep I<VAR>hmax : ∀ (a : X), r ⟨I, hli⟩ a → r a ⟨I, hli⟩<GOAL>∃ I, (LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun (x : ↑J) => s ↑x) → I = J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>IsFiniteMeasure (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<GOAL>IsFiniteMeasure (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>IsFiniteMeasure (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))<GOAL>IsFiniteMeasure (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>s.toJordanDecomposition = JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<GOAL>s.toJordanDecomposition = JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))<GOAL>s.toJordanDecomposition = JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))<GOAL>s = (JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(t + μ.withDensityᵥ f) i = ↑((t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure - (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure) i
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : ¬IsIso f<GOAL>Nat.card ↑(F.obj X) < Nat.card ↑(F.obj Y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : ¬IsIso f<VAR>hlt : ¬Nat.card ↑(F.obj X) < Nat.card ↑(F.obj Y)<GOAL>False
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : ¬IsIso f<VAR>hlt : ¬Nat.card ↑(F.obj X) < Nat.card ↑(F.obj Y)<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : ¬IsIso f<VAR>hlt : ¬Nat.card ↑(F.obj X) < Nat.card ↑(F.obj Y)<GOAL>Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : ¬IsIso f<VAR>hlt : Nat.card ↑(F.obj Y) ≤ Nat.card ↑(F.obj X)<GOAL>Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<GOAL>Small.{max v w, u} (FullSubcategory (CofilteredClosure f))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<GOAL>∀ (b : FullSubcategory (CofilteredClosure f)), ∃ a, CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a = b.obj
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<VAR>j : C<VAR>h : CofilteredClosure f j<GOAL>∃ a, CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := j, property := h }.obj
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>a : α<GOAL>Icc ⊥ a = Iic a
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hD : M.Dep D<GOAL>D.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hD : M.Dep D<GOAL>D ≠ ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J X : Set α<VAR>e f : α<VAR>hD : M.Dep ∅<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a✝ : M<VAR>inst✝ : DecidableEq M<VAR>a : M<VAR>h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1<GOAL>l.prod = (map id l).prod
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I✝ : MultispanIndex C<VAR>K : Multicofork I✝<VAR>I : MultispanIndex C<VAR>P : C<VAR>π : (b : I.R) → I.right b ⟶ P<VAR>w : ∀ (a : I.L), I.fst a ≫ π (I.fstFrom a) = I.snd a ≫ π (I.sndFrom a)<GOAL>∀ ⦃X Y : WalkingMultispan I.fstFrom I.sndFrom⦄ (f : X ⟶ Y), I.multispan.map f ≫ (fun x => match x with | WalkingMultispan.left a => I.fst a ≫ π (I.fstFrom a) | WalkingMultispan.right b => π b) Y = (fun x => match x with | WalkingMultispan.left a => I.fst a ≫ π (I.fstFrom a) | WalkingMultispan.right b => π b) X ≫ ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj P).map f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I✝ : MultispanIndex C<VAR>K : Multicofork I✝<VAR>I : MultispanIndex C<VAR>P : C<VAR>π : (b : I.R) → I.right b ⟶ P<VAR>w : ∀ (a : I.L), I.fst a ≫ π (I.fstFrom a) = I.snd a ≫ π (I.sndFrom a)<VAR>a✝ : I.L<GOAL>I.snd a✝ ≫ π (I.sndFrom a✝) = I.fst a✝ ≫ π (I.fstFrom a✝)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>x✝ : ∀ i ∈ [], Tendsto (f i) x (𝓝 (a i))<GOAL>Tendsto (fun b => (List.map (fun c => f c b) []).prod) x (𝓝 (List.map a []).prod)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f✝ : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>f : ι<VAR>l : List ι<VAR>h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))<GOAL>Tendsto (fun b => (List.map (fun c => f✝ c b) (f :: l)).prod) x (𝓝 (List.map a (f :: l)).prod)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f✝ : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>f : ι<VAR>l : List ι<VAR>h : ∀ i ∈ f :: l, Tendsto (f✝ i) x (𝓝 (a i))<GOAL>Tendsto (fun b => f✝ f b * (List.map (fun c => f✝ c b) l).prod) x (𝓝 (a f * (List.map a l).prod))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsColimit t.toCocone<GOAL>t.fst = ht.desc (BinaryCofan.mk (𝟙 X) 0)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsColimit t.toCocone<GOAL>∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(blimsup u f fun x => False) = ⊥
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u : U<GOAL>(Function.support fun g' => A ((B.coeff g') u)).IsPWO
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u : U<GOAL>(Function.support fun g' => A ((B.coeff g') u)) ⊆ Function.support ((of R).symm (B u)).coeff
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u : U<GOAL>∀ (x : Γ'), ¬A (((of R).symm (B u)).coeff x) = 0 → ¬((of R).symm (B u)).coeff x = 0
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u : U<VAR>g' : Γ'<VAR>hg' : ¬A (((of R).symm (B u)).coeff g') = 0<VAR>hAB : ((of R).symm (B u)).coeff g' = 0<GOAL>A 0 = 0
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₁ : γ₁<GOAL>inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔ (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ ∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : F<VAR>x : E<GOAL>iteratedFDeriv 𝕜 n (fun x => c) x = 0 x
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>p : LocallyConstant ↑C ℤ<GOAL>p ∈ range C ↔ p ∈ ⋃ e, smaller C ↑e
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>p : LocallyConstant ↑C ℤ<GOAL>(∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p) ↔ ∃ a, ∃ (h : a < o), ∃ x, (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x => ord I x < a) a_1), eval (π C fun x => ord I x < a) ⟨a_1, ⋯⟩ = x) ∧ (πs C a) x = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>p : ℕ → Prop<VAR>u : ℕ → α<GOAL>blimsup u atTop p = ⨅ i, ⨆ j, ⨆ (_ : p j ∧ i ≤ j), u j
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<GOAL>IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>h : s ×ˢ t = ∅<GOAL>IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>h : (s ×ˢ t).Nonempty<GOAL>IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>r c : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hfg : f =o[l] g<VAR>hg : 0 ≤ᶠ[l] g<GOAL>(fun x => √(f x)) =o[l] fun x => √(g x)
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>(fun f => f.toFun) 0 x ≤ (fun f => f.toFun) (const α ‖f‖ - f) x
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>f x ≤ ‖f‖
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxz : x < z<VAR>hxz' : x ≠ z<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)