ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun n => (s n).indicator f a) atTop (𝓝 ((⋂ b, s b).indicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<GOAL>μ.rnDeriv ν' =ᶠ[ae ν] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<GOAL>μ.rnDeriv ν' =ᶠ[ae ν] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<GOAL>∀ᵐ (x : α) ∂ν.restrict t, μ.rnDeriv ν' x = 0 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<GOAL>μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<VAR>this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'<GOAL>μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<VAR>this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'<GOAL>(μ.restrict t).rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<VAR>this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'<GOAL>rnDeriv 0 ν' =ᶠ[ae (ν.restrict h.nullSet)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>ν' : Measure α<VAR>inst✝ : SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<VAR>t : Set α := h.nullSet<VAR>ht : MeasurableSet t<VAR>this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'<GOAL>rnDeriv 0 ν' =ᶠ[ae ν'] 0
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<GOAL>adjoin K ((cyclotomic (↑n) K).rootSet L) = ⊤
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<GOAL>adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>this : DecidableEq L := Classical.decEq L<GOAL>adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>this : DecidableEq L := Classical.decEq L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<VAR>x : α<GOAL>x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<VAR>x : α<GOAL>(∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x) ↔ (∃ y, p.toFun y = x) ∨ x = newLast
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq β<VAR>h : s.Nonempty<GOAL>image2 (fun x y => y) ↑s ↑t = ↑t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹² : EMetricSpace X<VAR>inst✝¹¹ : EMetricSpace Y<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : MeasurableSpace P<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor E P<VAR>inst✝ : BorelSpace P<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>x : P<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set P<GOAL>μH[d] (⇑((AffineEquiv.homothetyUnitsMulHom x) (Units.mk0 c hc)) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a b : α<VAR>s : Sym α 1<VAR>l l' : { x // x.length = 1 }<GOAL>Setoid.r l l' ↔ Setoid.r ↑l ↑l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a b : α<VAR>s : Sym α 1<VAR>x✝¹ x✝ : { x // x.length = 1 }<VAR>val✝¹ : List α<VAR>property✝ : val✝¹.length = 1<VAR>val✝ : List α<VAR>h : val✝.length = 1<VAR>perm : ⟨val✝¹, property✝⟩ ≈ ⟨val✝, h⟩<GOAL>(fun l => (↑l).head ⋯) ⟨val✝¹, property✝⟩ = (fun l => (↑l).head ⋯) ⟨val✝, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a✝ b : α<VAR>s : Sym α 1<VAR>x✝¹ x✝ : { x // x.length = 1 }<VAR>val✝ : List α<VAR>property✝ : val✝.length = 1<VAR>a : α<VAR>h : [a].length = 1<VAR>perm : ⟨val✝, property✝⟩ ≈ ⟨[a], h⟩<GOAL>(fun l => (↑l).head ⋯) ⟨val✝, property✝⟩ = (fun l => (↑l).head ⋯) ⟨[a], h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a b : α<VAR>val✝ : Multiset α<VAR>l : List α<VAR>h : Multiset.card (Quot.mk Setoid.r l) = 1<GOAL>(fun a => ⟨{a}, ⋯⟩) ((fun s => ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x => x.length = 1) (fun x => Multiset.card x = 1) ⋯ ⋯) s).liftOn (fun l => (↑l).head ⋯) ⋯) ⟨Quot.mk Setoid.r l, h⟩) = ⟨Quot.mk Setoid.r l, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>val✝ : Multiset α<VAR>a : α<VAR>h : Multiset.card (Quot.mk Setoid.r [a]) = 1<GOAL>(fun a => ⟨{a}, ⋯⟩) ((fun s => ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x => x.length = 1) (fun x => Multiset.card x = 1) ⋯ ⋯) s).liftOn (fun l => (↑l).head ⋯) ⋯) ⟨Quot.mk Setoid.r [a], h⟩) = ⟨Quot.mk Setoid.r [a], h⟩
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>M : Type u_6<VAR>inst✝ : CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ range n, f (i + 1) / f i = f n / f 0
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<GOAL>μ s ≤ μ.mass
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<GOAL>∑ i ∈ Finset.range 0, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < 0), s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n.succ, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n.succ), s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>n : ℕ<GOAL>s n ∩ ⋃ k, ⋃ (_ : k < n), s k ⊆ ∅
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ s n ∩ ⋃ k, ⋃ (_ : k < n), s k → a ∈ ∅
<VAR>n : ℕ<VAR>hn0 : ¬n = 0<GOAL>↑(harmonic n) ≤ 1 + Real.log ↑n
<VAR>n : ℕ<VAR>hn0 : ¬n = 0<VAR>hn : 1 ≤ n<GOAL>↑(harmonic n) ≤ 1 + Real.log ↑n
<VAR>n : ℕ<VAR>hn0 : ¬n = 0<VAR>hn : 1 ≤ n<GOAL>∑ x ∈ Finset.Icc 1 n, (↑x)⁻¹ ≤ 1 + Real.log ↑n
<VAR>n : ℕ<VAR>hn0 : ¬n = 0<VAR>hn : 1 ≤ n<GOAL>1 + ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + Real.log ↑n
<VAR>n : ℕ<VAR>hn0 : ¬n = 0<VAR>hn : 1 ≤ n<GOAL>∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ Real.log ↑n
<VAR>n : ℕ<VAR>hn0 : ¬n = 0<VAR>hn : 1 ≤ n<GOAL>∑ x ∈ Finset.Ioc 1 n, (↑x)⁻¹ ≤ Real.log ↑n
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s t = hausdorffEdist t s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>(⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s = (⨆ y ∈ t, infEdist y s) ⊔ ⨆ x ∈ s, infEdist x t
<VAR>a✝¹ a✝ : ℕ<GOAL>↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Subsingleton R<VAR>f : R[X]<GOAL>f.Separable
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Field R<VAR>p q : R[X]<VAR>inst✝¹ : CommSemiring k<VAR>inst✝ : DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0<GOAL>eval₂ ϕ α g = 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Field R<VAR>p✝ q : R[X]<VAR>inst✝¹ : CommSemiring k<VAR>inst✝ : DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0<VAR>p : R[X]<VAR>hp : g = EuclideanDomain.gcd f g * p<GOAL>eval₂ ϕ α g = 0
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>(∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J) ↔ ∀ z ∈ I, x * z ∈ J
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ s : ℕ → Set Ω<VAR>ω : Ω<VAR>n : ℕ<GOAL>|process s (n + 1) ω - process s n ω| ≤ 1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ s : ℕ → Set Ω<VAR>ω : Ω<VAR>n : ℕ<GOAL>(s (n + 1)).indicator (fun a => ‖1 a‖) ω ≤ 1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ s : ℕ → Set Ω<VAR>ω : Ω<VAR>n : ℕ<VAR>x✝¹ : Ω<VAR>x✝ : x✝¹ ∈ s (n + 1)<GOAL>‖1 x✝¹‖ ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hμ : IsFiniteMeasure μ<VAR>hν : IsFiniteMeasure ν<VAR>this✝ : IsFiniteMeasure μ<VAR>this : IsFiniteMeasure ν<GOAL>⨍⁻ (x : α), f x ∂(μ + ν) = μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>(o.blsub f).cof ≤ o.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>(o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hA : A₁ ⊆ A₂<VAR>hf : IsMulFreimanIso n A₂ B₂ f<VAR>hf' : BijOn f A₁ B₁<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A₁<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A₁<VAR>hs : card s = n<VAR>ht : card t = n<GOAL>(map f s).prod = (map f t).prod ↔ s.prod = t.prod
<VAR>m : ℤ<VAR>hm : 0 < m<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>Hpv : (multiplicity (↑p) m).get ⋯ % 2 = 1<GOAL>1 ≠ 0
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>cosZeta a (-2 * (↑n + 1)) = 0
<VAR>a : UnitAddCircle<VAR>n : ℕ<VAR>this : -2 * (↑n + 1) ≠ 0<GOAL>cosZeta a (-2 * (↑n + 1)) = 0
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>f.toMap x * f.mk' 1 y = f.mk' x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>s✝ t s : Finset α<GOAL>filter q (filter p s) = filter p (filter q s)
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>↑(Ioc a b).card = b - a
<VAR>n p : ℕ<VAR>hp : Prime p<GOAL>(p - 1) * (multiplicity p n !).get ⋯ = n - (p.digits n).sum
<VAR>n p : ℕ<VAR>hp : Prime p<GOAL>(p - 1) * (↑(∑ x ∈ range (log p n + 1), n / p ^ (x + 1))).get ⋯ = (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a * (f x + m / 2 * ‖x‖ ^ 2) + b * (f y + m / 2 * ‖y‖ ^ 2) - m / 2 * ‖a • x + b • y‖ ^ 2 = a * f x + b * f y + m / 2 * a * b * ‖x - y‖ ^ 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α<GOAL>u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α<GOAL>(∀ x ∈ u, x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α<VAR>x : α<GOAL>x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : β ≃ᵐ α<GOAL>Measure.map (⇑e.symm) μ = Measure.comap (⇑e) μ
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x * r) l atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<GOAL>∀ᶠ (a : α) in l, b ≤ f a * r
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<VAR>n : ℕ<VAR>hn : 1 ≤ n • r<GOAL>∀ᶠ (a : α) in l, b ≤ f a * r
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<VAR>n : ℕ<VAR>hn : 1 ≤ n • r<VAR>hn' : 1 ≤ ↑n * r<GOAL>∀ᶠ (a : α) in l, b ≤ f a * r
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<VAR>n : ℕ<VAR>hn : 1 ≤ n • r<VAR>hn' : 1 ≤ ↑n * r<VAR>x : α<VAR>hx : max b 0 * ↑n ≤ f x<GOAL>b ≤ f x * r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>hm : f.FinMeasSupp μ<VAR>hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤<GOAL>f.lintegral μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>hm : f.FinMeasSupp μ<VAR>hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤<VAR>a : ℝ≥0∞<VAR>ha : a ∈ f.range<GOAL>a * μ (↑f ⁻¹' {a}) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>hm : f.FinMeasSupp μ<VAR>hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤<VAR>ha : ⊤ ∈ f.range<GOAL>⊤ * μ (↑f ⁻¹' {⊤}) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>hm : f.FinMeasSupp μ<VAR>hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤<VAR>a : ℝ≥0∞<VAR>ha✝ : a ∈ f.range<VAR>ha : a ≠ ⊤<GOAL>a * μ (↑f ⁻¹' {a}) ≠ ⊤
<GOAL>map cexp (comap re atBot) = 𝓝[≠] 0
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 ≤ b<GOAL>1 < (a ^ b - 1) / (a - 1)
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 ≤ b<VAR>h₁ : a - 1 ∣ a ^ b - 1<GOAL>1 < (a ^ b - 1) / (a - 1)
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 ≤ b<VAR>h₁ : a - 1 ∣ a ^ b - 1<GOAL>a < a ^ b
<VAR>n : ℕ<GOAL>fib (n + 2) < fib (n + 1 + 2)
<VAR>n : ℕ<GOAL>fib (n + 2) < fib (n + 2 + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>p : T[X]<GOAL>(-p).aroots S = p.aroots S
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>s : Finset α<VAR>i j : α → ℕ<VAR>is_prime : ∀ p ∈ s, Prime p<VAR>is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<GOAL>f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>i j : α → ℕ<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<VAR>is_prime : ∀ p ∈ ∅, Prime p<VAR>is_coprime : ∀ p ∈ ∅, ∀ q ∈ ∅, p ∣ q → p = q<GOAL>f (∏ p ∈ ∅, p ^ (i p + j p)) = f (∏ p ∈ ∅, p ^ i p) * f (∏ p ∈ ∅, p ^ j p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>i j : α → ℕ<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>s : Finset α<VAR>hps : p ∉ s<VAR>ih : (∀ p ∈ s, Prime p) → (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) → f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)<VAR>is_prime : ∀ p_1 ∈ insert p s, Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q<GOAL>f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>i j : α → ℕ<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>s : Finset α<VAR>hps : p ∉ s<VAR>ih : (∀ p ∈ s, Prime p) → (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) → f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)<VAR>is_prime : ∀ p_1 ∈ insert p s, Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q<VAR>hpr_p : Prime p<GOAL>f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>i j : α → ℕ<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>s : Finset α<VAR>hps : p ∉ s<VAR>ih : (∀ p ∈ s, Prime p) → (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) → f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)<VAR>is_prime : ∀ p_1 ∈ insert p s, Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q<VAR>hpr_p : Prime p<VAR>hpr_s : ∀ p ∈ s, Prime p<GOAL>f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)