ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a<VAR>a : α<GOAL>((fun a x => f a x - g a x) + g) a =ᶠ[ae (κ a)] f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a<VAR>a : α<VAR>x : β<VAR>hx : g a x ≤ f a x<GOAL>((fun a x => f a x - g a x) + g) a x = f a x
<VAR>R : Type u_2<VAR>K : Type ?u.2896<VAR>L : Type ?u.2899<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<GOAL>map (algebraMap R S) (minpoly R x) /ₘ (X - C x) * (X - C x) = map (algebraMap R S) (minpoly R x)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<GOAL>map Prod.fst s.val ≤ m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<GOAL>∀ (a : α), card (filter (fun a_1 => a = a_1.1) s.val) ≤ count a m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<VAR>a : α<GOAL>card (filter (fun a_1 => a = a_1.1) s.val) ≤ count a m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<VAR>a : α<VAR>ha : card (filter (fun x => a = x.1) s.val) = 0<GOAL>card (filter (fun a_1 => a = a_1.1) s.val) ≤ count a m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<VAR>a : α<VAR>ha : card (filter (fun x => a = x.1) s.val) > 0<GOAL>card (filter (fun a_1 => a = a_1.1) s.val) ≤ count a m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>s : Finset (α × ℕ)<VAR>hsm : s ⊆ m.toEnumFinset<VAR>a : α<VAR>ha : card (filter (fun x => a = x.1) s.val) > 0<VAR>n : ℕ<VAR>han : n ≥ card (filter (fun x => a = x.1) s.val) - 1<VAR>hn : (a, n) ∈ s<GOAL>card (filter (fun a_1 => a = a_1.1) s.val) ≤ count a m
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>f : l ≃. m<VAR>g : m ≃. n<VAR>i : l<VAR>j : n<GOAL>(f.trans g).toMatrix i j = (f.toMatrix * g.toMatrix) i j
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>f : l ≃. m<VAR>g : m ≃. n<VAR>i : l<VAR>j : n<GOAL>(f.trans g).toMatrix i j = Option.casesOn (f i) 0 fun fi => g.toMatrix fi j
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<VAR>h : a < b<GOAL>∃ c x, a * c = b
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c✝ d : α<VAR>h : a < b<VAR>c : α<VAR>hc : b = a * c<GOAL>∃ c x, a * c = b
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c✝ d : α<VAR>h : a < b<VAR>c : α<VAR>hc : b = a * c<GOAL>c ≠ 1
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<VAR>h : a < b<VAR>hc : b = a * 1<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => min (f x) a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)<GOAL>b ∈ doset a ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ∃ x ∈ doset a ↑H ↑K, x ∈ doset b ↑H ↑K<GOAL>b ∈ doset a ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ∃ x, (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) ∧ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * b * y<GOAL>∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b l : G<VAR>hl : l ∈ ↑H<VAR>r : G<VAR>hr : r ∈ ↑K<VAR>y : G<VAR>hy : y ∈ ↑H<VAR>r' : G<VAR>hr' : r' ∈ ↑K<VAR>hrx : y * b * r' = l * a * r<GOAL>∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b l : G<VAR>hl : l ∈ ↑H<VAR>r : G<VAR>hr : r ∈ ↑K<VAR>y : G<VAR>hy : y ∈ ↑H<VAR>r' : G<VAR>hr' : r' ∈ ↑K<VAR>hrx : y * b * r' = l * a * r<GOAL>b = y⁻¹ * l * a * (r * r'⁻¹)
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ι → α → M<VAR>l✝ : Multiset (α → M)<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ Quot.mk Setoid.r l, Measurable f<GOAL>Measurable (prod (Quot.mk Setoid.r l))
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>hωb : BddAbove (Set.range fun n => f n ω)<GOAL>∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>hωb : (upperBounds (Set.range fun n => f n ω)).Nonempty<GOAL>∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>hωb : (upperBounds (Set.range fun n => f n ω)).Nonempty<VAR>i : ℕ<VAR>hi : hωb.some < ↑i<GOAL>∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>hωb : (upperBounds (Set.range fun n => f n ω)).Nonempty<VAR>i : ℕ<VAR>hi : hωb.some < ↑i<VAR>hib : ∀ (n : ℕ), f n ω < ↑i<GOAL>∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n => stoppedValue f (leastGE f (↑i) n) ω) atTop (𝓝 c)<VAR>hωb : (upperBounds (Set.range fun n => f n ω)).Nonempty<VAR>i : ℕ<VAR>hi : hωb.some < ↑i<VAR>hib : ∀ (n : ℕ), f n ω < ↑i<VAR>heq : ∀ (n : ℕ), stoppedValue f (leastGE f (↑i) n) ω = f n ω<GOAL>∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>G : SimpleGraph V<VAR>v : V<VAR>inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)<GOAL>(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset.card = Fintype.card V - 1
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q a b : MvPolynomial σ R<GOAL>∀ {a b : σ →₀ ℕ}, ((a + b).sum fun x e => e) ≤ (a.sum fun x e => e) + b.sum fun x e => e
<VAR>p s : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<GOAL>IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume
<VAR>p s : ℝ<VAR>hs : -1 < s<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<GOAL>IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume
<VAR>p s : ℝ<VAR>hs : -1 < s<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 = p<GOAL>IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume
<VAR>α β : Type<VAR>n✝ n : ℕ<VAR>S : Set (Vector3 ℕ n.succ)<VAR>d : Dioph S<VAR>v : Fin2 n → ℕ<VAR>x : ℕ<GOAL>((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>m : ℕ<VAR>φ : L[[↑A]].Formula (α ⊕ Fin m)<VAR>x : α → M<GOAL>x ∈ (fun g => g ∘ Sum.inl) '' setOf φ.Realize ↔ x ∈ setOf (BoundedFormula.relabel id φ).exs.Realize
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>m : ℕ<VAR>φ : L[[↑A]].Formula (α ⊕ Fin m)<VAR>x : α → M<GOAL>(∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔ ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hF_meas : AEMeasurable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hF_meas : AEMeasurable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hF_meas : AEMeasurable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤<VAR>h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<GOAL>span Set.univ = ⊤
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<GOAL>∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x : ℙ K V<VAR>_hx : x ∈ ⊤<GOAL>x ∈ span Set.univ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : Integrable f μ<GOAL>setToFun μ T hT f = setToFun μ' T hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : Integrable f μ<VAR>h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'<GOAL>setToFun μ T hT f = setToFun μ' T hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : Integrable f μ<VAR>h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'<GOAL>∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun x => c)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : Integrable f μ<VAR>h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'<GOAL>∀ ⦃f g : α → E⦄, Disjoint (Function.support f) (Function.support g) → Integrable f μ → Integrable g μ → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (f + g)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : Integrable f μ<VAR>h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'<GOAL>IsClosed {f | (fun f => setToFun μ T hT f = setToFun μ' T hT' f) ↑↑f}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : Integrable f μ<VAR>h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'<GOAL>∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Integrable f μ → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s<GOAL>comap (fun x => (f x.1, f x.2)) (𝓤 β) = 𝓤 α
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n : ℕ<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => x ^ 0) (↑0 * x ^ (0 - 1)) x
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n : ℕ<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => x ^ 1) (↑1 * x ^ (1 - 1)) x
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n✝ n : ℕ<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => x ^ (n + 1 + 1)) (↑(n + 1 + 1) * x ^ (n + 1 + 1 - 1)) x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set σ<GOAL>x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set σ<VAR>this : x ∈ Ideal.span ((fun s => (monomial s) 1) '' ((fun i => Finsupp.single i 1) '' s)) ↔ ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi<GOAL>x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set σ<VAR>this : x ∈ Ideal.span ((fun x => (monomial (Finsupp.single x 1)) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi<GOAL>x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set σ<VAR>this : x ∈ Ideal.span ((fun x => (monomial (Finsupp.single x 1)) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi<GOAL>(∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : β → α<VAR>h : Monotone m ∨ Surjective f<GOAL>(comap f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : β → α<VAR>h : Monotone m ∨ Surjective f<VAR>s : Set β<GOAL>((comap f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f '' s)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : β → α<VAR>h : Monotone m ∨ Surjective f<VAR>s : Set β<GOAL>(OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯) s ≤ ((comap f) (OuterMeasure.ofFunction m m_empty)) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>(starRingEnd 𝕜) (-1) * ⟪x, y⟫_𝕜 = -⟪x, y⟫_𝕜
<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>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>h : IsOpen U<VAR>x : X<VAR>x_in : x ∈ U<GOAL>(𝓝 ⟨x, x_in⟩).HasBasis (fun s => s ∈ 𝓝 ⟨x, x_in⟩ ∧ IsPathConnected s) id
<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>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>h : IsOpen U<VAR>x : X<VAR>x_in : x ∈ U<GOAL>(comap Subtype.val (𝓝 x)).HasBasis (fun s => s ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected s) id
<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>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>h : IsOpen U<VAR>x : X<VAR>x_in : x ∈ U<VAR>V : Set ↑U<GOAL>V ∈ comap Subtype.val (𝓝 x) ↔ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V
<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>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>h : IsOpen U<VAR>x : X<VAR>x_in : x ∈ U<VAR>V : Set ↑U<GOAL>(∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i ∧ i ⊆ U) ∧ Subtype.val ⁻¹' id i ⊆ V) ↔ ∃ i, (i ∈ comap Subtype.val (𝓝 x) ∧ IsPathConnected i) ∧ id i ⊆ V