ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>m : ℕ<VAR>l : List ℕ<VAR>n : ℕ<GOAL>lower' (raise' (m :: l) n) n = m :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<GOAL>f.support.Nonempty ↔ f ≠ 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(unop X✝).hom.op ≫ (F.map f.unop.left).op = (unop Y✝).hom.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>((unop Y✝).hom ≫ 𝟙 d).op = (unop Y✝).hom.op
<VAR>p q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>q : ℚ≥0<GOAL>↑q.den * q = ↑q.num
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>h : m.gcd n = 1<GOAL>addOrderOf ↑(↑m / ↑n * p) = n
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>h : m.gcd n = 1<GOAL>addOrderOf ↑(↑m / ↑n * p) = m.gcd n * addOrderOf ↑(↑m / ↑n * p)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝² : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₁<VAR>x : E<VAR>h : x ≠ 0<GOAL>‖coord 𝕜 x h‖ = ‖x‖⁻¹
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝² : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₁<VAR>x : E<VAR>h : x ≠ 0<VAR>hx : 0 < ‖x‖<GOAL>‖coord 𝕜 x h‖ = ‖x‖⁻¹
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝² : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₁<VAR>x : E<VAR>h : x ≠ 0<VAR>hx : 0 < ‖x‖<VAR>this : Nontrivial ↥(Submodule.span 𝕜 {x})<GOAL>‖coord 𝕜 x h‖ = ‖x‖⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) (s ×ˢ univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q<VAR>h_dir_prod : Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q<VAR>h_dir_prod : Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q<GOAL>∫⁻ (b : β) in s, ⨆ i, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic ↑i) ∂ν a = ⨆ i, (κ a) (s ×ˢ Iic ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q<VAR>h_dir_prod : Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q<GOAL>⨆ b, ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, a_1)) (Iic ↑b) ∂ν a = ⨆ i, (κ a) (s ×ˢ Iic ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q<VAR>h_dir_prod : Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q<GOAL>∀ (b : ℚ), AEMeasurable (fun b_1 => ((IsCondKernelCDF.toKernel f hf) (a, b_1)) (Iic ↑b)) ((ν a).restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q<VAR>h_dir_prod : Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q<GOAL>Directed (fun x x_1 => x ≤ x_1) fun i b => ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic ↑i)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : s ∈ 𝓝 x<GOAL>HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>a : α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t<GOAL>s.sdiff t ⊓ upperClosure t = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>a✝ : α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t<VAR>a : α<VAR>ha : a ∈ (⇑toDual ∘ SetLike.coe) s<GOAL>a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>a b : α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : DecidableEq α<VAR>f : α → β<VAR>inj : Injective f<VAR>inst✝ : Decidable (a < b)<GOAL>compare (f a) (f b) = compareOfLessAndEq a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>a b : α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : DecidableEq α<VAR>f : α → β<VAR>inj : Injective f<VAR>inst✝ : Decidable (a < b)<VAR>h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)<GOAL>compare (f a) (f b) = compareOfLessAndEq a b
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<GOAL>(X * p).coeff (n + 1) = p.coeff n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as : Multiset α<VAR>b : β<VAR>bs : Multiset β<GOAL>Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as : Multiset α<VAR>b : β<VAR>bs : Multiset β<GOAL>(∃ b_1 bs', flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as : Multiset α<VAR>b : β<VAR>bs : Multiset β<VAR>a : α<VAR>as' : Multiset α<GOAL>flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
<VAR>α✝ : Type u_1<VAR>l : List α✝<VAR>a : α✝<GOAL>l.Disjoint [a] ↔ ¬a ∈ l
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q = (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>((α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>A B : V<VAR>f : A ⟶ B<GOAL>(HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A).hom ≫ f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B).inv = f
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x y : α<GOAL>y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x y : α<GOAL>(∃ a < (p.cycleOf x).support.card, (p ^ a) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f p : R[X]<GOAL>(X * p).reverse = p.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<GOAL>(fun a => f a ⊔ g a) ∈ measurableLE μ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<GOAL>(fun a => max (f a) (g a)) ∈ measurableLE μ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ ≤ ν A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})<GOAL>∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ ≤ ν A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})<VAR>h₂ : MeasurableSet (A ∩ {a | g a < f a})<GOAL>∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ ≤ ν A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})<VAR>h₂ : MeasurableSet (A ∩ {a | g a < f a})<GOAL>∫⁻ (x : α) in A ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x | g x < f x}, f x ∂μ ≤ ν A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})<VAR>h₂ : MeasurableSet (A ∩ {a | g a < f a})<GOAL>ν (A ∩ {a | f a ≤ g a}) + ν (A ∩ {a | g a < f a}) = ν A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ measurableLE μ ν<VAR>hg : g ∈ measurableLE μ ν<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})<VAR>h₂ : MeasurableSet (A ∩ {a | g a < f a})<GOAL>ν (A ∩ {a | f a ≤ g a}) + ν (A \ {a | f a ≤ g a}) = ν A
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>y : S<GOAL>(y𝖣(algebraMap R S) x) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>y : S<GOAL>y • single ((algebraMap R S) x) 1 ∈ kerTotal R S
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<GOAL>(CauchySeq fun s => ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<GOAL>(∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : D<GOAL>L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (L.map (h.unit.app (R.obj X)))) = L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X))))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : D<GOAL>L.map (h.unit.app (R.obj X) ≫ R.map (L.map (h.unit.app (R.obj X)))) = L.map (h.unit.app (R.obj X)) ≫ L.map (h.unit.app (R.obj (L.obj (R.obj X))))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : D<GOAL>L.map (h.unit.app (R.obj X)) ≫ L.map (R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : D<GOAL>L.map (h.unit.app (R.obj X) ≫ R.map (h.counit.app X)) = 𝟙 (L.obj (R.obj X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>h : Presheaf.IsLocallySurjective (coherentTopology C) f<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<GOAL>Presheaf.imageSieve f y ∈ (regularTopology C).sieves U✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>h : Presheaf.imageSieve f y ∈ (coherentTopology C).sieves U✝<GOAL>Presheaf.imageSieve f y ∈ (regularTopology C).sieves U✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>h : ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<GOAL>Presheaf.imageSieve f y ∈ (regularTopology C).sieves U✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<GOAL>Presheaf.imageSieve f y ∈ (regularTopology C).sieves U✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<GOAL>∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<VAR>x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) := (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫ (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm<VAR>this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G<GOAL>(f.app (op (∐ Z))) (i'.hom x) = (G.map (Sigma.desc π).op) y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<VAR>x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) := (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫ (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm<VAR>this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G<GOAL>∀ (j : (Discrete α)ᵒᵖ), ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app j) ((f.app (op (∐ Z))) (i'.hom x)) = ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app j) ((G.map (Sigma.desc π).op) y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<VAR>x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) := (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫ (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm<VAR>this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G<VAR>a : α<GOAL>((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app (op { as := a })) ((f.app (op (∐ Z))) (i'.hom x)) = ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app (op { as := a })) ((G.map (Sigma.desc π).op) y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<VAR>x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) := (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫ (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm<VAR>this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G<VAR>a : α<GOAL>(f.app (op (Z a))) ((F.map (Sigma.ι Z a).op) (F.map (opCoproductIsoProduct Z).inv ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x)))) = (G.map (Sigma.ι Z a).op) ((G.map (Sigma.desc π).op) y)