ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>r : R<VAR>N : Submodule R M<GOAL>Ideal.span {r} • N = r • N
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>r : R<VAR>N : Submodule R M<VAR>this : span R (⋃ t ∈ N, {r • t}) = r • N<GOAL>Ideal.span {r} • N = r • N
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>r : R<VAR>N : Submodule R M<VAR>this : span R (⋃ t ∈ N, {r • t}) = r • N<GOAL>span R (⋃ s ∈ {r}, ⋃ t ∈ ↑N, {s • t}) = r • N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : SuccOrder α<VAR>a : α<GOAL>succ a = ⨅ b, ⨅ (_ : a < b), b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : SuccOrder α<VAR>a : α<GOAL>⨅ b, ⨅ (_ : a < b), b ≤ succ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : SuccOrder α<GOAL>⨅ b, ⨅ (_ : ⊤ < b), b ≤ succ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : SuccOrder α<VAR>a : α<VAR>ha : a ≠ ⊤<GOAL>⨅ b, ⨅ (_ : a < b), b ≤ succ a
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>t.eraseMax.Valid
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>t.dual.eraseMin.Valid
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>u : ι → UniformSpace γ<GOAL>UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>u : ι → UniformSpace γ<GOAL>UniformFun.filter α γ (⨅ i, 𝓤 γ) = ⨅ i, 𝓤 (α →ᵤ γ)
<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✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>h₁ : IsUnramifiedAtInfinitePlaces k F<VAR>inst✝ : Algebra.IsAlgebraic K F<VAR>w : InfinitePlace K<GOAL>InfinitePlace.IsUnramified k w
<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✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>h₁ : IsUnramifiedAtInfinitePlaces k F<VAR>inst✝ : Algebra.IsAlgebraic K F<VAR>w : InfinitePlace F<GOAL>InfinitePlace.IsUnramified k ((fun x => x.comap (algebraMap K F)) w)
<VAR>m n : ℤ<GOAL>(m + n).bodd = xor m.bodd n.bodd
<VAR>m n : ℕ<GOAL>((m + n).succ + 1).bodd = (m + 1 + (n + 1)).bodd
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>coyonedaEquiv (coyoneda.map f.op) = f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(coyoneda.map f.op).app Y (𝟙 Y) = f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : C<VAR>inst✝ : HasBinaryCoproducts C<VAR>A : (coprodMonad X).Algebra<GOAL>coprod.inr ≫ (coprodMonad X).map (Iso.refl ((𝟭 (coprodMonad X).Algebra).obj A).A).hom ≫ ((algebraToUnder X ⋙ underToAlgebra X).obj A).a = coprod.inr ≫ ((𝟭 (coprodMonad X).Algebra).obj A).a ≫ (Iso.refl ((𝟭 (coprodMonad X).Algebra).obj A).A).hom
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop (𝓝 0)<VAR>r : ℝ<VAR>hr : r < 0<GOAL>↑r < ofSeq f
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop (𝓝 0)<VAR>r : ℝ<VAR>hr : r < 0<GOAL>-↑(-r) < ofSeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s ×ˢ s \ s.offDiag = s.diag
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : A → A → Prop<VAR>k : S<VAR>a b : A<VAR>h : Rel r a b<GOAL>Rel r (k • a) (k • b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonUnitalNonAssocRing α<VAR>a b c : α<GOAL>(a - b) * c = a * c - b * c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → F<VAR>U : Set E<VAR>c : E<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hd : DifferentiableOn ℂ f U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>x : E<VAR>hx : x ∈ U<VAR>H₁ : ‖f x‖ = ‖f c‖<VAR>H₂ : ‖f x + f c‖ = ‖f c + f c‖<GOAL>‖f x + Function.const E (f c) x‖ = ‖f x‖ + ‖Function.const E (f c) x‖
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(PInfty.f n ≫ (PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))) ≫ (PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))) ≫ PInfty.f n ≫ (Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) = PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(PInfty.f n ≫ (Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) = PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) = 𝟙 (Γ₀.Obj.obj₂ X (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>∀ (A : Splitting.IndexSet (op [n])), (((Γ₀.splitting X).cofan (op [n])).inj A ≫ (Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) = ((Γ₀.splitting X).cofan (op [n])).inj A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<VAR>A : Splitting.IndexSet (op [n])<GOAL>(((Γ₀.splitting X).cofan (op [n])).inj A ≫ (Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) = ((Γ₀.splitting X).cofan (op [n])).inj A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<VAR>A : Splitting.IndexSet (op [n])<GOAL>𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A = ((Γ₀.splitting X).cofan (op [n])).inj A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>b b' : F<GOAL>Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>b b' : F<GOAL>b' ∈ (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).baseSet
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>inst✝ : ⊥.IsCountablyGenerated<GOAL>MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) ⊥ (𝓝 c)}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<GOAL>MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this : UpgradedPolishSpace γ := upgradePolishSpace γ<GOAL>MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<GOAL>MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<GOAL>MeasurableSet {x | Cauchy (map (fun n => f n x) l)}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<VAR>this : ∀ (x : β), (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n => ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)<GOAL>MeasurableSet {x | (map (fun n => f n x) l).NeBot ∧ map (fun n => f n x) l ×ˢ map (fun n => f n x) l ≤ uniformity γ}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<VAR>this : ∀ (x : β), (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n => ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)<GOAL>MeasurableSet (⋂ i, ⋂ (_ : True), {x | ∃ i_2, True ∧ ((fun n => f n x) '' u i_2) ×ˢ ((fun n => f n x) '' u i_2) ⊆ {p | dist p.1 p.2 < 1 / (↑i + 1)}})
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<VAR>this : ∀ (x : β), (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n => ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)<VAR>K : ℕ<VAR>x✝ : K ∈ fun i => True<GOAL>MeasurableSet {x | ∃ i, True ∧ ((fun n => f n x) '' u i) ×ˢ ((fun n => f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<VAR>this : ∀ (x : β), (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n => ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)<VAR>K : ℕ<VAR>x✝ : K ∈ fun i => True<GOAL>MeasurableSet (⋃ i, {x | ((fun n => f n x) '' u i) ×ˢ ((fun n => f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}})
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<VAR>this : ∀ (x : β), (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n => ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)<VAR>K : ℕ<VAR>x✝ : K ∈ fun i => True<VAR>N : ℕ<GOAL>MeasurableSet {x | ((fun n => f n x) '' u N) ×ˢ ((fun n => f n x) '' u N) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁷ : T2Space β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : PolishSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>inst✝¹ : Countable ι<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hl : l.NeBot<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>u : ℕ → Set ι<VAR>hu : l.HasAntitoneBasis u<VAR>this : ∀ (x : β), (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n => ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)<VAR>K : ℕ<VAR>x✝ : K ∈ fun i => True<VAR>N : ℕ<GOAL>MeasurableSet (⋂ i ∈ u N, ⋂ i_1 ∈ u N, {x | (i, i_1) ∈ (fun p => (f p.1 x, f p.2 x)) ⁻¹' {p | dist p.1 p.2 < 1 / (↑K + 1)}})
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q✝ r q : ℚ≥0<VAR>a : α<GOAL>Commute (↑q) a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n : ℕ<GOAL>x ∈ Ideal.span {↑p ^ n} ↔ ↑n ≤ x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n : ℕ<GOAL>↑p ^ n ∣ x ↔ ↑n ≤ x.valuation
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommSemiring α<VAR>A : Matrix n n α<GOAL>IsUnit Aᵀ ↔ IsUnit A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>⌊a⌋₊ ≤ ⌈a⌉₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>ha : a ≤ 0<GOAL>⌊a⌋₊ ≤ ⌈a⌉₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ ≤ ⌈a⌉₊
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<GOAL>Prime a
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<GOAL>¬IsUnit a
<VAR>a b✝ : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<VAR>b c : Cardinal.{u}<VAR>hbc : a ∣ b * c<GOAL>a ∣ b ∨ a ∣ c
<VAR>a b✝ : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<VAR>b c : Cardinal.{u}<VAR>hbc : a ∣ b * c<VAR>hz : b * c = 0<GOAL>a ∣ b ∨ a ∣ c
<VAR>a b✝ : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<VAR>b c : Cardinal.{u}<VAR>hbc : a ∣ b * c<VAR>hz : b * c ≠ 0<GOAL>a ∣ b ∨ a ∣ c
<VAR>a✝ a b✝ : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<VAR>b c : Cardinal.{u}<VAR>hbc : a ∣ b * c<VAR>hz : b * c ≠ 0<VAR>h : c ≤ b<GOAL>a ∣ b
<VAR>a✝ a b✝ : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<VAR>b c : Cardinal.{u}<VAR>hbc : a ∣ b * c<VAR>hz : b * c ≠ 0<VAR>h : c ≤ b<VAR>habc : a ≤ b * c<GOAL>a ∣ b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b c d : α<GOAL>min a b < min a c ↔ b < c ∧ b < a
<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>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>hE : CompleteSpace E<GOAL>∀ (f : α × β → E), Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
<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>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>hE : CompleteSpace E<GOAL>∀ (c : E) ⦃s : Set (α × β)⦄, MeasurableSet s → (μ.prod ν) s < ⊤ → ∫ (z : α × β), s.indicator (fun x => c) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), s.indicator (fun x => c) (x, y) ∂ν ∂μ
<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>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>hE : CompleteSpace E<GOAL>∀ ⦃f g : α × β → E⦄, Disjoint (support f) (support g) → Integrable f (μ.prod ν) → Integrable g (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ → ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ → ∫ (z : α × β), (f + g) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
<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>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>hE : CompleteSpace E<GOAL>IsClosed {f | ∫ (z : α × β), ↑↑f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ}
<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>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>hE : CompleteSpace E<GOAL>∀ ⦃f g : α × β → E⦄, f =ᶠ[ae (μ.prod ν)] g → Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ → ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ