ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∑' (n : ℕ), κ.compProdFun (η.seq n) a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hs : MeasurableSet s<VAR>n : ℕ<GOAL>Measurable fun a => κ.compProdFun (η.seq n) a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hs : MeasurableSet s<VAR>n : ℕ<GOAL>Measurable fun a => ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hs : MeasurableSet s<VAR>n : ℕ<VAR>h_meas : Measurable (Function.uncurry fun a b => ((η.seq n) (a, b)) {c | (b, c) ∈ s})<GOAL>Measurable fun a => ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : UniqueDiffWithinAt 𝕜 s x<VAR>m : Fin 1 → E<GOAL>(iteratedFDerivWithin 𝕜 1 f s x) m = (fderivWithin 𝕜 f s x) (m 0)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : UniqueDiffWithinAt 𝕜 s x<VAR>m : Fin 1 → E<GOAL>(((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderivWithin 𝕜 f s x)) (m 0)) (tail m) = (fderivWithin 𝕜 f s x) (m 0)
<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>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>U V : Opens M<VAR>hUV : U ≤ V<VAR>x : ↑↑U<GOAL>LiftPropAt Q (id ∘ inclusion hUV) x
<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>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>U V : Opens M<VAR>hUV : U ≤ V<VAR>x : ↑↑U<GOAL>LiftPropAt Q id (inclusion hUV x)
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<VAR>this : Encodable ↑S<GOAL>⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝ : DecidableEq m<VAR>f : α → β<VAR>i✝ : m<VAR>j✝ : n<GOAL>(M.updateRow i b).map f i✝ j✝ = (M.map f).updateRow i (f ∘ b) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝ : DecidableEq m<VAR>f : α → β<VAR>i✝ : m<VAR>j✝ : n<GOAL>f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<GOAL>(1 + X • M.map ⇑C).det.coeff 1 = M.trace
<VAR>X✝ : CondensedSet<VAR>X : TopCat<GOAL>Continuous fun x => x.toFun PUnit.unit
<VAR>X✝ : CondensedSet<VAR>X : TopCat<GOAL>Continuous ((fun x => x.toFun PUnit.unit) ∘ CondensedSet.coinducingCoprod X.toCondensedSet)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.27949, u_3} E<VAR>inst✝⁴ : Category.{?u.27953, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>a : A<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.27949, u_3} E<VAR>inst✝⁴ : Category.{?u.27953, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>a : A<VAR>X : C<GOAL>(isoWhiskerLeft (F.functor a) (shiftFunctorZero D A)).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.24226, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X✝ Y✝ : (HomologicalComplex V c)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>i j : ι<VAR>x✝ : c.symm.Rel i j<GOAL>(fun i => (f.unop.f i).op) i ≫ ((fun X => (unop X).op) Y✝).d i j = ((fun X => (unop X).op) X✝).d i j ≫ (fun i => (f.unop.f i).op) j
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<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>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M'<VAR>h : Surjective ⇑f<GOAL>lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥(LinearMap.ker f))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<GOAL>QuotientAddGroup.mk '' Ico a (a + p) = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>hab : a ≠ b<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>cons a s ha \ cons b s hb = {a}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>ht : t ∈ 𝓝[s] x<GOAL>MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x
<VAR>F : Type u_1<VAR>inst✝ : CommSemiring F<VAR>q : ℕ<VAR>f✝ : F[X]<VAR>hf✝ : HasSeparableContraction q f✝<VAR>f : F[X]<VAR>hf : HasSeparableContraction 1 f<GOAL>hf.degree = f.natDegree
<VAR>F : Type u_1<VAR>inst✝ : CommSemiring F<VAR>q : ℕ<VAR>f✝ : F[X]<VAR>hf✝ : HasSeparableContraction q f✝<VAR>f : F[X]<VAR>hf : HasSeparableContraction 1 f<VAR>a : ℕ<VAR>ha : hf.degree * 1 ^ a = f.natDegree<GOAL>hf.degree = f.natDegree
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>s : Set Γ₀<GOAL>IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>β : OreLocalization S X → Prop<VAR>c : ∀ (r : X) (s : ↥S), β (r /ₒ s)<GOAL>∀ (q : OreLocalization S X), β q
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>β : OreLocalization S X → Prop<VAR>c : ∀ (r : X) (s : ↥S), β (r /ₒ s)<GOAL>∀ (a : X × ↥S), β ⟦a⟧
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<GOAL>(x, y) ∈ filter (fun x => match x with | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y) (A ×ˢ A) → (x, y) ∈ ((P.nonUniforms G (ε / 8)).biUnion fun x => match x with | (U, V) => U ×ˢ V) ∪ P.parts.biUnion offDiag ∪ (P.sparsePairs G (ε / 4)).biUnion fun x => match x with | (U, V) => G.interedges U V
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<GOAL>x ∈ A → y ∈ A → G.Adj x y → (G.Adj x y → ∀ x_1 ∈ P.parts, ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4) → (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨ (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨ ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<VAR>hx : x ∈ A<VAR>hy : y ∈ A<VAR>h : G.Adj x y<VAR>h' : ∀ x_1 ∈ P.parts, ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4<GOAL>(∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨ (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨ ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<VAR>hx✝ : x ∈ A<VAR>hy : y ∈ A<VAR>h : G.Adj x y<VAR>h' : ∀ x_1 ∈ P.parts, ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>hx : x ∈ U<GOAL>(∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨ (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨ ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<VAR>hx✝ : x ∈ A<VAR>hy✝ : y ∈ A<VAR>h : G.Adj x y<VAR>h' : ∀ x_1 ∈ P.parts, ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>hx : x ∈ U<VAR>V : Finset α<VAR>hV : V ∈ P.parts<VAR>hy : y ∈ V<GOAL>(∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨ (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨ ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<VAR>hx✝ : x ∈ A<VAR>hy✝ : y ∈ A<VAR>h : G.Adj x y<VAR>h' : ∀ x_1 ∈ P.parts, ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>hx : x ∈ U<VAR>hV : U ∈ P.parts<VAR>hy : y ∈ U<GOAL>(∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨ (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨ ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>x y : α<VAR>hx✝ : x ∈ A<VAR>hy✝ : y ∈ A<VAR>h : G.Adj x y<VAR>h' : ∀ x_1 ∈ P.parts, ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>hx : x ∈ U<VAR>V : Finset α<VAR>hV : V ∈ P.parts<VAR>hy : y ∈ V<VAR>hUV : U ≠ V<GOAL>(∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨ (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨ ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c * c = c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c * c ≤ c
<VAR>c✝ : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<GOAL>⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
<VAR>c✝ : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<GOAL>⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
<VAR>c✝ : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<VAR>this✝ : LinearOrder α := linearOrderOfSTO r<VAR>this : IsWellOrder α fun x x_1 => x < x_1<VAR>g : α × α → α := fun p => max p.1 p.2<VAR>f : α × α ↪ Ordinal.{u_1} × α × α := { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p), inj' := ⋯ }<VAR>s : α × α → α × α → Prop := ⇑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)<GOAL>⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
<VAR>c✝ : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<VAR>this✝¹ : LinearOrder α := linearOrderOfSTO r<VAR>this✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>g : α × α → α := fun p => max p.1 p.2<VAR>f : α × α ↪ Ordinal.{u_1} × α × α := { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p), inj' := ⋯ }<VAR>s : α × α → α × α → Prop := ⇑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)<VAR>this : IsWellOrder (α × α) s<GOAL>⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧
<VAR>c✝ : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<VAR>this✝¹ : LinearOrder α := linearOrderOfSTO r<VAR>this✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>g : α × α → α := fun p => max p.1 p.2<VAR>f : α × α ↪ Ordinal.{u_1} × α × α := { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p), inj' := ⋯ }<VAR>s : α × α → α × α → Prop := ⇑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)<VAR>this : IsWellOrder (α × α) s<GOAL>type s ≤ type r
<VAR>c✝ : Cardinal.{u_1}<VAR>h✝ : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<VAR>this✝¹ : LinearOrder α := linearOrderOfSTO r<VAR>this✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>g : α × α → α := fun p => max p.1 p.2<VAR>f : α × α ↪ Ordinal.{u_1} × α × α := { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p), inj' := ⋯ }<VAR>s : α × α → α × α → Prop := ⇑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)<VAR>this : IsWellOrder (α × α) s<VAR>o : Ordinal.{u_1}<VAR>h : o < type s<GOAL>o < type r
<VAR>c✝ : Cardinal.{u_1}<VAR>h✝ : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<VAR>this✝¹ : LinearOrder α := linearOrderOfSTO r<VAR>this✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>g : α × α → α := fun p => max p.1 p.2<VAR>f : α × α ↪ Ordinal.{u_1} × α × α := { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p), inj' := ⋯ }<VAR>s : α × α → α × α → Prop := ⇑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)<VAR>this : IsWellOrder (α × α) s<VAR>p : α × α<VAR>h : typein s p < type s<GOAL>typein s p < type r
<VAR>c✝ : Cardinal.{u_1}<VAR>h✝ : ℵ₀ ≤ c✝<VAR>c : Cardinal.{u_1}<VAR>x✝ : ∀ y < c, Acc (fun x x_1 => x < x_1) y<VAR>α : Type u_1<VAR>IH : ∀ y < ⟦α⟧, ℵ₀ ≤ y → y * y ≤ y<VAR>ol : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>e : (#α).ord = type r<VAR>this✝¹ : LinearOrder α := linearOrderOfSTO r<VAR>this✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>g : α × α → α := fun p => max p.1 p.2<VAR>f : α × α ↪ Ordinal.{u_1} × α × α := { toFun := fun p => (typein (fun x x_1 => x < x_1) (g p), p), inj' := ⋯ }<VAR>s : α × α → α × α → Prop := ⇑f ⁻¹'o Prod.Lex (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)<VAR>this : IsWellOrder (α × α) s<VAR>p : α × α<VAR>h : typein s p < type s<GOAL>(typein s p).card < #α
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsStronglyCartesian f φ<GOAL>map p f φ ⋯ φ = 𝟙 a
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsStronglyCartesian (p.map φ) φ<GOAL>map p (p.map φ) φ ⋯ φ = 𝟙 a✝
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsStronglyCartesian (p.map φ) φ<GOAL>𝟙 a✝ = map p (p.map φ) φ ⋯ φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsStronglyCartesian (p.map φ) φ<GOAL>𝟙 a✝ ≫ φ = φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<GOAL>∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R ↥M₁<VAR>N' : Submodule R ↥N₁<VAR>left✝¹ : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<GOAL>∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R ↥M₁<VAR>N' : Submodule R ↥N₁<VAR>left✝¹ : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<VAR>hM : Submodule.map M₁.subtype M' ≤ M₁<GOAL>∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R ↥M₁<VAR>N' : Submodule R ↥N₁<VAR>left✝¹ : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<VAR>hM : Submodule.map M₁.subtype M' ≤ M₁<VAR>hN : Submodule.map N₁.subtype N' ≤ N₁<GOAL>∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))