ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ✝ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f : α × β → γ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>τ : Measure γ<VAR>hf : Measurable f<VAR>inst✝ : SFinite ν<VAR>h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y => f (x, y)) ν τ<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>h2s : τ s = 0<GOAL>∫⁻ (x : α), ν (Prod.mk x ⁻¹' (f ⁻¹' s)) ∂μ = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ✝ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f : α × β → γ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>τ : Measure γ<VAR>hf : Measurable f<VAR>inst✝ : SFinite ν<VAR>h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y => f (x, y)) ν τ<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>h2s : τ s = 0<GOAL>∫⁻ (x : α), ν ((fun x_1 => f (x, x_1)) ⁻¹' s) ∂μ = 0
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>hi : ∀ J ∈ π₁, πi₁ J = πi₂ J<VAR>J : Box ι<GOAL>J ∈ π₁.biUnion πi₁ ↔ J ∈ π₁.biUnion πi₂
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>hi : ∀ J ∈ π₁, πi₁ J = πi₂ J<VAR>J : Box ι<GOAL>(∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set (Set β)<GOAL>f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : ℝ → α<GOAL>Tendsto (fun x => f (rexp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : ℝ → α<GOAL>Tendsto (fun x => f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>x : R<VAR>x✝ : ∃ p ∈ I, p.degree ≤ ↑0 ∧ p.leadingCoeff = x<VAR>p : R[X]<VAR>hpI : p ∈ I<VAR>hpdeg : p.degree ≤ ↑0<VAR>hpx : p.leadingCoeff = x<GOAL>C x ∈ I
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>hxy : JoinedIn F x y<VAR>hyz : JoinedIn F y z<GOAL>JoinedIn F x z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>hxy : JoinedIn F x y<VAR>hyz : JoinedIn F y z<VAR>hx : x ∈ F<VAR>hy : y ∈ F<GOAL>JoinedIn F x z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>hxy : JoinedIn F x y<VAR>hyz : JoinedIn F y z<VAR>hx✝ : x ∈ F<VAR>hy✝ hx : y ∈ F<VAR>hy : z ∈ F<GOAL>JoinedIn F x z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>hx✝¹ : x ∈ F<VAR>hy✝¹ : y ∈ F<VAR>hy✝ : z ∈ F<VAR>hxy : Joined ⟨x, ⋯⟩ ⟨y, ⋯⟩<VAR>hyz : Joined ⟨y, ⋯⟩ ⟨z, ⋯⟩<VAR>hx✝ : x ∈ F<VAR>hx : y ∈ F<VAR>hy : z ∈ F<GOAL>Joined ⟨x, ⋯⟩ ⟨z, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>([a] ++ l).sublists = do let x ← l.sublists [x, a :: x]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>(do let x ← l.sublists map (fun x_1 => x_1 ++ x) [a].sublists) = do let x ← l.sublists [x, a :: x]
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>this : ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<GOAL>∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs✝ : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>r : Set ↑s<VAR>hr : r.Countable<VAR>hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<GOAL>∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs✝ : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>r : Set ↑s<VAR>hr : r.Countable<VAR>hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<GOAL>s ⊆ ⋃ x ∈ r, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs✝ : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>r : Set ↑s<VAR>hr : r.Countable<VAR>hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<GOAL>⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs✝ : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>r : Set ↑s<VAR>hr : r.Countable<VAR>hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<GOAL>∀ i ∈ r, (fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs✝ : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>r : Set ↑s<VAR>hr : r.Countable<VAR>hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<VAR>i : ↑s<VAR>hi : i ∈ r<GOAL>(fun x => interior (U ↑x ⋯)) i ⊆ ⋃ x ∈ r, U ↑x ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs✝ : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>r : Set ↑s<VAR>hr : r.Countable<VAR>hs : s ⊆ ⋃ i ∈ r, (fun x => interior (U ↑x ⋯)) i<VAR>i : ↑s<VAR>hi : i ∈ r<GOAL>U ↑i ⋯ ⊆ ⋃ x ∈ r, U ↑x ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<GOAL>mrange (id M) = ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Periodic f T<VAR>t s : ℝ<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂<GOAL>∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in t..t + T, f x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m n : ℕ<GOAL>orderOf (x ^ n) ∣ orderOf x
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>i j : ℕ<GOAL>i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>i j : ℕ<VAR>hi : i + j = n ∧ j ≤ k<GOAL>k - j + (n - k) = i
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>i j : ℕ<GOAL>(∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s : Set α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<GOAL>variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s : Set α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<VAR>h : x ≤ y<GOAL>variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s : Set α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<VAR>h : y ≤ x<GOAL>variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesRightHomologyOf S<VAR>inst✝ : (S.map F).HasHomology<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesRightHomologyOf S<VAR>inst✝ : (S.map F).HasHomology<VAR>this : S.HasHomology<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesRightHomologyOf S<VAR>inst✝ : (S.map F).HasHomology<VAR>this : S.HasHomology<VAR>h : 𝟙 S.rightHomologyData.H = 0<GOAL>(S.map F).Exact
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<GOAL>{x | ∃ y, y ⋖ x}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>e_1✝ : α = αᵒᵈ<VAR>x✝¹ x✝ : α<GOAL>x✝ ⋖ x✝¹ ↔ x✝¹ ⋖ x✝
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J : Box ι<VAR>i : ι<VAR>inst✝ : Finite ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<GOAL>∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J : Box ι<VAR>i : ι<VAR>inst✝ : Finite ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<VAR>s : Finset (ι × ℝ)<VAR>hs : ∀ π ∈ {π₁, π₂}, π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion<GOAL>∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J : Box ι<VAR>i : ι<VAR>inst✝ : Finite ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<VAR>s : Finset (ι × ℝ)<VAR>hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion<GOAL>∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J : Box ι<VAR>i : ι<VAR>inst✝ : Finite ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<VAR>s : Finset (ι × ℝ)<VAR>h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion<VAR>h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion<GOAL>∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J✝ : Box ι<VAR>i : ι<VAR>inst✝ : Finite ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<VAR>s : Finset (ι × ℝ)<VAR>h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion<VAR>h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion<VAR>J : Box ι<VAR>hJ : J ∈ π₁.boxes<GOAL>↑J ≤ I₀
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J✝ : Box ι<VAR>i : ι<VAR>inst✝ : Finite ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<VAR>s : Finset (ι × ℝ)<VAR>h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion<VAR>h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion<VAR>J : Box ι<VAR>hJ : J ∈ π₂.boxes<GOAL>↑J ≤ I₀
<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>e : G ≃L[𝕜] E<GOAL>ContDiff 𝕜 n (f ∘ ⇑e) ↔ ContDiff 𝕜 n f
<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>e : G ≃L[𝕜] E<GOAL>ContDiffOn 𝕜 n (f ∘ ⇑e) (?m.449353 ⁻¹' univ) ↔ ContDiffOn 𝕜 n f univ
<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>e : G ≃L[𝕜] E<GOAL>Type ?u.449349
<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>e : G ≃L[𝕜] E<GOAL>G → ?m.449352
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : UniformInducing g<GOAL>UniformInducing (g ∘ f) ↔ UniformInducing f
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c✝ : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m✝ : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<VAR>c : 𝕜'<VAR>m : (i : ι) → E i<GOAL>‖(c • f) m‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c✝ : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m✝ : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<VAR>c : 𝕜'<VAR>m : (i : ι) → E i<GOAL>‖c‖ * ‖f m‖ ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>h : t.WellFoundedOn r'<VAR>hle : r ≤ r'<VAR>hst : s ⊆ t<GOAL>s.WellFoundedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>h : WellFounded fun a b => r' a b ∧ a ∈ t ∧ b ∈ t<VAR>hle : r ≤ r'<VAR>hst : s ⊆ t<GOAL>WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
<VAR>p n k : ℕ<VAR>h : n < p<VAR>hnk : ¬n < k<GOAL>(n.choose k).factorization p = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<GOAL>¬Module.Finite R R[X]
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<GOAL>¬∃ S, S.Finite ∧ Submodule.span R S = ⊤
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>s : Set R[X]<VAR>hs : s.Finite<VAR>contra : Submodule.span R s = ⊤<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>s : Set R[X]<VAR>hs : s.Finite<VAR>contra : Submodule.span R s = ⊤<VAR>n : ℕ<VAR>hn : Submodule.span R s ≤ degreeLE R ↑n<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>s : Set R[X]<VAR>hs : s.Finite<VAR>contra : Submodule.span R s = ⊤<VAR>n : ℕ<VAR>hn : Submodule.span R s ≤ degreeLE R ↑n<VAR>this : X ^ (n + 1) ∈ degreeLE R ↑n<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>s : Set R[X]<VAR>hs : s.Finite<VAR>contra : Submodule.span R s = ⊤<VAR>n : ℕ<VAR>hn : Submodule.span R s ≤ degreeLE R ↑n<VAR>this : 1 = 0<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : (𝓤 α).IsCountablyGenerated<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : (𝓤 α).IsCountablyGenerated<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)<VAR>U' : ℕ → Set (α × α)<VAR>hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : (𝓤 α).IsCountablyGenerated<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)<VAR>U' : ℕ → Set (α × α)<VAR>hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s<VAR>Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : (𝓤 α).IsCountablyGenerated<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)<VAR>U' : ℕ → Set (α × α)<VAR>hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s<VAR>Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α<VAR>f✝ : Filter α<VAR>hf : Cauchy f✝<VAR>N m n : ℕ<VAR>hm : N ≤ m<VAR>hn : N ≤ n<GOAL>(SequentiallyComplete.seq hf Hmem m, SequentiallyComplete.seq hf Hmem n) ∈ U N
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : (𝓤 α).IsCountablyGenerated<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)<VAR>U' : ℕ → Set (α × α)<VAR>hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s<VAR>Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α<VAR>f✝ : Filter α<VAR>hf : Cauchy f✝<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ n, U n ∩ U' n ⊆ s
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ : 𝕜<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : 𝕜<VAR>hx : x ∈ s<GOAL>UniqueDiffOn 𝕜 (insert x s)
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>g : γ → δ<VAR>f' : α' → β → δ<VAR>g' : α → α'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b<GOAL>image2 f' (g' '' s) ((fun b => b) '' t) = image2 f' (g' '' s) t
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>π : Prepartition I<VAR>h : π.IsPartition<GOAL>π.compl = ⊥
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>h : finrank ℚ K = 1<GOAL>NrRealPlaces K = 1
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>h : finrank ℚ K = 1<VAR>this : NrRealPlaces K + 2 * NrComplexPlaces K = finrank ℚ K<GOAL>NrRealPlaces K = 1
<VAR>k : ℕ<VAR>hk : 1 < k<GOAL>riemannZeta ↑k = ∑' (n : ℕ), 1 / ↑n ^ k
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : AffineSpace V2 P2<VAR>inst✝⁷ : AddCommGroup V3<VAR>inst✝⁶ : AffineSpace V3 P3<VAR>inst✝⁵ : Module k V1<VAR>inst✝⁴ : Module k V2<VAR>inst✝³ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommGroup (φv i)<VAR>inst✝¹ : (i : ι) → Module k (φv i)<VAR>inst✝ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<GOAL>pi fv = 0 ↔ ∀ (i : ι), fv i = 0