ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Module.Flat R M₂<VAR>rs : List R<VAR>h : IsWeaklyRegular M rs<GOAL>IsWeaklyRegular (M ⊗[R] M₂) rs
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Semiring T<VAR>inst✝² : FunLike F R✝ S<VAR>rcf : RingHomClass F R✝ S<VAR>inst✝¹ : FunLike G T S<VAR>rcg : RingHomClass G T S<VAR>f : F<VAR>g : G<VAR>ι : Type u_3<VAR>R : ι → Type u_4<VAR>inst✝ : (i : ι) → Semiring (R i)<VAR>φ : (i : ι) → S →+* R i<VAR>x : S<GOAL>x ∈ ker (Pi.ringHom φ) ↔ x ∈ ⨅ i, ker (φ i)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>x✝ : ↥A.unitGroup<GOAL>x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ x✝ ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>x✝ : ↥A.unitGroup<GOAL>x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ A.unitGroupMulEquiv x✝ ∈ (Units.map ↑(LocalRing.residue ↥A)).ker
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x : ℝ≥0∞<GOAL>(min t x).toReal ≤ t.toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x : ℝ≥0∞<GOAL>min t x ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<VAR>m : a ∉ s<GOAL>s ≤ a ::ₘ t ↔ s ≤ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<VAR>m : a ∉ s<GOAL>s ≤ a ::ₘ t → s ≤ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<VAR>m : a ∉ s<GOAL>∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<VAR>t' : Multiset α<VAR>h : s ≤ t'<GOAL>a ∉ s → a ∈ t' → a ::ₘ s ≤ t'
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<VAR>t' : Multiset α<VAR>h : s ≤ t'<GOAL>∀ {l₁ l₂ : List α}, l₁ <+ l₂ → a ∉ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s✝ t : Multiset α<VAR>a : α<VAR>t' : Multiset α<VAR>h : s✝ ≤ t'<VAR>l₁ l₂ : List α<VAR>s : l₁ <+ l₂<VAR>m₁ : a ∉ ↑l₁<VAR>m₂ : a ∈ ↑l₂<GOAL>a ::ₘ ↑l₁ ≤ ↑l₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s✝ t : Multiset α<VAR>a : α<VAR>t' : Multiset α<VAR>h : s✝ ≤ t'<VAR>l₁ : List α<VAR>m₁ : a ∉ ↑l₁<VAR>r₁ r₂ : List α<VAR>s : l₁ <+ r₁ ++ a :: r₂<VAR>m₂ : a ∈ ↑(r₁ ++ a :: r₂)<GOAL>a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)
<VAR>k : Type u<VAR>inst✝⁵ : Field k<VAR>G : Grp<VAR>inst✝⁴ : IsAlgClosed k<VAR>inst✝³ : Fintype ↑G<VAR>inst✝² : Invertible ↑(Fintype.card ↑G)<VAR>V W : FDRep k ↑G<VAR>inst✝¹ : Simple V<VAR>inst✝ : Simple W<GOAL>⅟↑(Fintype.card ↑G) • ∑ g : ↑G, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then 1 else 0
<VAR>k : Type u<VAR>inst✝⁵ : Field k<VAR>G : Grp<VAR>inst✝⁴ : IsAlgClosed k<VAR>inst✝³ : Fintype ↑G<VAR>inst✝² : Invertible ↑(Fintype.card ↑G)<VAR>V W : FDRep k ↑G<VAR>inst✝¹ : Simple V<VAR>inst✝ : Simple W<GOAL>⅟↑(Fintype.card ↑G) • Finset.univ.sum (of (linHom W.ρ V.ρ)).character = if Nonempty (V ≅ W) then 1 else 0
<VAR>k : Type u<VAR>inst✝⁵ : Field k<VAR>G : Grp<VAR>inst✝⁴ : IsAlgClosed k<VAR>inst✝³ : Fintype ↑G<VAR>inst✝² : Invertible ↑(Fintype.card ↑G)<VAR>V W : FDRep k ↑G<VAR>inst✝¹ : Simple V<VAR>inst✝ : Simple W<GOAL>↑(finrank k ↥(invariants (of (linHom W.ρ V.ρ)).ρ)) = if Nonempty (V ≅ W) then 1 else 0
<VAR>k : Type u<VAR>inst✝⁵ : Field k<VAR>G : Grp<VAR>inst✝⁴ : IsAlgClosed k<VAR>inst✝³ : Fintype ↑G<VAR>inst✝² : Invertible ↑(Fintype.card ↑G)<VAR>V W : FDRep k ↑G<VAR>inst✝¹ : Simple V<VAR>inst✝ : Simple W<GOAL>↑(finrank k ↥(linHom W.ρ V.ρ).invariants) = if Nonempty (V ≅ W) then 1 else 0
<VAR>k : Type u<VAR>inst✝⁵ : Field k<VAR>G : Grp<VAR>inst✝⁴ : IsAlgClosed k<VAR>inst✝³ : Fintype ↑G<VAR>inst✝² : Invertible ↑(Fintype.card ↑G)<VAR>V W : FDRep k ↑G<VAR>inst✝¹ : Simple V<VAR>inst✝ : Simple W<GOAL>↑(finrank k (W ⟶ V)) = if Nonempty (V ≅ W) then 1 else 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))<GOAL>↑(numDerangements (n + 1)) = ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n + 1 - k))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))<GOAL>∀ x ∈ Finset.range (n + 1), (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))<VAR>x : ℕ<VAR>hx : x ∈ Finset.range (n + 1)<GOAL>(↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))<VAR>x : ℕ<VAR>hx : x ∈ Finset.range (n + 1)<VAR>h_le : x ≤ n<GOAL>(↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>inst✝ : Fintype ι<VAR>hμ : iIndep m μ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>μ (⋂ i, s i) = ∏ i : ι, μ (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s t : Set α<VAR>a : ↑s<GOAL>Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_anti : Antitone f<VAR>hbdd : BddAbove (range f)<GOAL>Tendsto f atBot (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<VAR>ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<VAR>ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal<GOAL>∀ (x : α), ↑(f x) < g x
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<VAR>ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal<GOAL>LowerSemicontinuous g
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<VAR>ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal<GOAL>Integrable (fun x => (g x).toReal) μ
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<VAR>ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal<GOAL>∀ᵐ (x : α) ∂μ, g x < ⊤
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ≥0 := ⟨ε / 2, ⋯⟩<VAR>δpos : 0 < δ<VAR>fp : α → ℝ≥0 := fun x => (f x).toNNReal<VAR>int_fp : Integrable (fun x => ↑(fp x)) μ<VAR>gp : α → ℝ≥0∞<VAR>fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x<VAR>gpcont : LowerSemicontinuous gp<VAR>gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤<VAR>gp_integrable : Integrable (fun x => (gp x).toReal) μ<VAR>gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ<VAR>fm : α → ℝ≥0 := fun x => (-f x).toNNReal<VAR>int_fm : Integrable (fun x => ↑(fm x)) μ<VAR>gm : α → ℝ≥0<VAR>gm_le_fm : ∀ (x : α), gm x ≤ fm x<VAR>gmcont : UpperSemicontinuous gm<VAR>gm_integrable : Integrable (fun x => ↑(gm x)) μ<VAR>gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ<VAR>g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)<VAR>ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal<GOAL>∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>↑(Fintype.card ↑(Set.Ioc a b)) = b - a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in l, p x) ↔ {x | p x}ᶜ ∉ l
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>P : Sort v<VAR>n : K[X]<VAR>d : ↥K[X]⁰<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'<GOAL>{ toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>P : Sort v<VAR>n : K[X]<VAR>d : ↥K[X]⁰<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'<GOAL>Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q => f p ↑q) ⋯ = f n ↑d
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>_h : φ.order ≠ ψ.order<VAR>H : φ.order < ψ.order<GOAL>(φ + ψ).order ≤ φ.order ⊓ ψ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>_h : φ.order ≠ ψ.order<VAR>H : φ.order < ψ.order<GOAL>(φ + ψ).order = φ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>_h : φ.order ≠ ψ.order<VAR>H : φ.order < ψ.order<GOAL>(∀ (i : ℕ), ↑i = φ.order → (coeff R i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < φ.order → (coeff R i) (φ + ψ) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>s : Set E<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : range f ∪ {0} ⊆ s<GOAL>Tendsto (fun n => SimpleFunc.integral μ (approxOn f fmeas s 0 ⋯ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))