ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)<GOAL>pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x y : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(normAtPlace w) (x + y) ≤ (normAtPlace w) x + (normAtPlace w) y
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x y : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤ (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖
<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>I : Ideal R<GOAL>I * annihilator I = ⊥
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>cramer 1 = 1
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i j : n<GOAL>(cramer 1 ∘ₗ LinearMap.single i) 1 j = (1 ∘ₗ LinearMap.single i) 1 j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i j : n<GOAL>1 = det 1
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i j : n<GOAL>∀ (j : n), Pi.single i 1 j = 1 j i
<VAR>α : Type u_1<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>(l.balRight v r).reverse = r.reverse.balLeft v l.reverse
<VAR>α : Type u_1<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>(l.balRight v r).reverse = (r.reverse.balLeft v l.reverse).reverse.reverse
<VAR>n✝ b m n : ℕ<GOAL>ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p < r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p < r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>p₂ ≠ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p < r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>p₂ ≠ p₃
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>Nonempty Ω
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>maybe_empty : ¬Nonempty Ω<GOAL>False
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>maybe_empty : ¬Nonempty Ω<VAR>zero : ↑μ univ = 0<GOAL>False
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>maybe_empty : ¬Nonempty Ω<VAR>zero : 1 = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : Disjoint s₁ s₂<GOAL>InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : Disjoint s₁ s₂<VAR>H : InjOn f (s₁ ∪ s₂)<GOAL>∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : Disjoint s₁ s₂<GOAL>(InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y) → InjOn f (s₁ ∪ s₂)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasPullbacks C<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>G : ModuleCat R<VAR>x y : Over G<VAR>P : ModuleCat R<VAR>p : P ⟶ x.left<VAR>q : P ⟶ y.left<VAR>hp : Epi p<VAR>hq : Epi q<VAR>H : p ≫ x.hom = q ≫ y.hom<GOAL>LinearMap.range x.hom = LinearMap.range y.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasPullbacks C<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>G : ModuleCat R<VAR>x y : Over G<VAR>P : ModuleCat R<VAR>p : P ⟶ x.left<VAR>q : P ⟶ y.left<VAR>hp : Epi p<VAR>hq : Epi q<VAR>H : p ≫ x.hom = q ≫ y.hom<VAR>a : ↑((Functor.fromPUnit G).obj x.right)<VAR>ha : a ∈ LinearMap.range x.hom<GOAL>a ∈ LinearMap.range y.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasPullbacks C<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>G : ModuleCat R<VAR>x y : Over G<VAR>P : ModuleCat R<VAR>p : P ⟶ x.left<VAR>q : P ⟶ y.left<VAR>hp : Epi p<VAR>hq : Epi q<VAR>H : p ≫ x.hom = q ≫ y.hom<VAR>a : ↑((Functor.fromPUnit G).obj x.right)<VAR>ha : a ∈ LinearMap.range y.hom<GOAL>a ∈ LinearMap.range x.hom
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : BooleanAlgebra α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>n : ℕ<VAR>hn : n ≤ Fintype.card α<VAR>h𝒜 : Set.Sized n ↑𝒜ᶜˢ<GOAL>Set.Sized (Fintype.card α - n) ↑𝒜
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : BooleanAlgebra α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>n : ℕ<VAR>hn : n ≤ Fintype.card α<VAR>h𝒜 : Set.Sized (Fintype.card α - n) ↑𝒜<GOAL>Set.Sized n ↑𝒜ᶜˢ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : StandardBorelSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T0Space Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace Y<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace Z<VAR>f : X → Z<VAR>inst✝ : CountablySeparated ↑(range f)<VAR>hf : Measurable f<VAR>hr : MeasurableSet (range f)<VAR>s : Set Z<GOAL>MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ∂ν a = (κ a) (s ×ˢ Iic ↑q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>ENNReal.ofReal (∫ (x : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, x)) ↑q ∂ν a) = (κ a) (s ×ˢ Iic ↑q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ((ν a).restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>0 ≤ᶠ[ae ((ν a).restrict s)] fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>Sopen : ∀ t ∈ S, IsOpen t<VAR>Scount : S.Countable<VAR>T : Set (Set X)<VAR>Topen : ∀ t ∈ T, IsOpen t<VAR>Tcount : T.Countable<GOAL>IsGδ (⋂₀ S ∪ ⋂₀ T)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>Sopen : ∀ t ∈ S, IsOpen t<VAR>Scount : S.Countable<VAR>T : Set (Set X)<VAR>Topen : ∀ t ∈ T, IsOpen t<VAR>Tcount : T.Countable<GOAL>IsGδ (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>Sopen : ∀ t ∈ S, IsOpen t<VAR>Scount : S.Countable<VAR>T : Set (Set X)<VAR>Topen : ∀ t ∈ T, IsOpen t<VAR>Tcount : T.Countable<GOAL>∀ i ∈ S ×ˢ T, IsOpen (i.1 ∪ i.2)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>Sopen : ∀ t ∈ S, IsOpen t<VAR>Scount : S.Countable<VAR>T : Set (Set X)<VAR>Topen : ∀ t ∈ T, IsOpen t<VAR>Tcount : T.Countable<VAR>a b : Set X<VAR>ha : (a, b).1 ∈ S<VAR>hb : (a, b).2 ∈ T<GOAL>IsOpen ((a, b).1 ∪ (a, b).2)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>epiWithInjectiveKernel f
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>∃ I, ∃ (_ : Injective I), ∃ f_1, ∃ (w : f_1 ≫ f = 0), Nonempty (ShortComplex.mk f_1 f w).Splitting
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<VAR>aeSeqLim : α → β := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<VAR>aeSeqLim : α → β := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some<VAR>x : α<GOAL>Tendsto (fun i => aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : PseudoMetrizableSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>ι : Type u_3<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<VAR>aeSeqLim : α → β := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some<GOAL>g =ᶠ[ae μ] aeSeqLim
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>x : S<VAR>z : R<GOAL>(map Q g hy) (z • x) = g z • (map Q g hy) x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x y : n → α<GOAL>(u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>e : α ↪ α<GOAL>map e univ = univ
<VAR>o : Ordinal.{u_1}<GOAL>o.toPGame.birthday = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.birthday = k<GOAL>o.toPGame.birthday = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.birthday = k<GOAL>max (lsub fun i => (typein (fun x x_1 => x < x_1) i).toPGame.birthday) (lsub fun i => i.elim.birthday) = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.birthday = k<GOAL>(lsub fun i => (typein (fun x x_1 => x < x_1) i).toPGame.birthday) = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.birthday = k<GOAL>(lsub fun i => (typein (fun x x_1 => x < x_1) i).toPGame.birthday) = lsub (typein fun x x_1 => x < x_1)
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.birthday = k<VAR>x : (Quotient.out o).α<GOAL>(typein (fun x x_1 => x < x_1) x).toPGame.birthday = typein (fun x x_1 => x < x_1) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>a b : X<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>hmono : MonotoneOn f ∅<VAR>ha : IsLeast ∅ a<VAR>hb : IsGreatest ∅ b<VAR>hs : μ ∅ ≠ ⊤<VAR>h's : MeasurableSet ∅<GOAL>IntegrableOn f ∅ μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>h✝ : s.Nonempty<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>h✝ : s.Nonempty<VAR>hbelow : BddBelow (f '' s)<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>h✝ : s.Nonempty<VAR>hbelow : BddBelow (f '' s)<VAR>habove : BddAbove (f '' s)<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>h✝ : s.Nonempty<VAR>hbelow : BddBelow (f '' s)<VAR>habove : BddAbove (f '' s)<VAR>this : IsBounded (f '' s)<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>h✝ : s.Nonempty<VAR>hbelow : BddBelow (f '' s)<VAR>habove : BddAbove (f '' s)<VAR>this : IsBounded (f '' s)<VAR>C : ℝ<VAR>hC : ∀ x ∈ f '' s, ‖x‖ ≤ C<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁵ : BorelSpace X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder X<VAR>inst✝³ : ConditionallyCompleteLinearOrder E<VAR>inst✝² : OrderTopology X<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>h✝ : s.Nonempty<VAR>hbelow : BddBelow (f '' s)<VAR>habove : BddAbove (f '' s)<VAR>this : IsBounded (f '' s)<VAR>C : ℝ<VAR>hC : ∀ x ∈ f '' s, ‖x‖ ≤ C<VAR>A : IntegrableOn (fun x => C) s μ<GOAL>IntegrableOn f s μ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>ha : 0 ≤ a<VAR>hbc : b ≤ c<GOAL>(fun x => a * x) '' Icc b c = Icc (a * b) (a * c)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>im z⁻¹ = -im z / normSq z
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n + 1 + (n + 1 - 1) = 2 * (n + 1) - 1
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n + 1 + (n + 1 - 1) = n + 1 + (n + 1) - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<GOAL>comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α