ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<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>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<VAR>l₁ : ι →₀ R<VAR>hl₁ : l₁ ∈ Finsupp.supported R R s<VAR>hl₂ : l₁ ∈ Finsupp.supported R R t<GOAL>(Finsupp.total ι M R v) l₁ = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<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>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<VAR>l₁ : ι →₀ R<VAR>hl₁ : l₁ ∈ Finsupp.supported R R s<VAR>hl₂ : l₁ ∈ Finsupp.supported R R t<VAR>this : l₁ = 0<GOAL>(Finsupp.total ι M R v) l₁ = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁹ : Ring R<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✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>b : ι → M<VAR>h : LinearIndependent R b<GOAL>Fintype.card ι ≤ finrank R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>la : Filter α<VAR>lb : Filter β<VAR>p : α × β → Prop<VAR>h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x<GOAL>∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>la : Filter α<VAR>lb : Filter β<VAR>p : α × β → Prop<VAR>h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x<VAR>pa : α → Prop<VAR>ha : ∀ᶠ (x : α) in la, pa x<VAR>pb : β → Prop<VAR>hb : ∀ᶠ (y : β) in lb, pb y<VAR>h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)<GOAL>∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
<VAR>a b c d✝ m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n d : ℕ<GOAL>d * (n / d) = n ↔ d * (n / d) = d * (n / d) + n % d
<VAR>a b c d✝ m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n d : ℕ<GOAL>d * (n / d) = d * (n / d) + n % d ↔ d ∣ n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : MeasurableSet t<GOAL>∫ (x : X) in s, t.indicator f x ∂μ = ∫ (x : X) in s ∩ t, f x ∂μ
<VAR>k✝ : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁹ : CommSemiring k✝<VAR>inst✝⁸ : Monoid G<VAR>inst✝⁷ : Monoid H<VAR>A✝ : Type u₃<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Algebra k✝ A✝<VAR>B : Type u_3<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra k✝ B<VAR>k : Type u_4<VAR>A : Type u_5<VAR>inst✝² : CommSemiring k<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra k A<VAR>x✝ : MonoidAlgebra A G<GOAL>(mapDomainAlgHom k A (MonoidHom.id G)) x✝ = (AlgHom.id k (MonoidAlgebra A G)) x✝
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[id] Y₁<VAR>g : Y₁ → X<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>m : M<VAR>x : Y₁<GOAL>g (m • f (g x)) = g (f (m • g x))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<VAR>h0 : p 0 = 0<GOAL>(p.leftInv i).comp (id 𝕜 F) = (p.leftInv i).comp (p.comp (p.rightInv i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<VAR>h0 : p 0 = 0<GOAL>(p.leftInv i).comp (p.comp (p.rightInv i)) = ((p.leftInv i).comp p).comp (p.rightInv i)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<VAR>h0 : p 0 = 0<GOAL>((p.leftInv i).comp p).comp (p.rightInv i) = (id 𝕜 E).comp (p.rightInv i)
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<GOAL>¬p ^ (padicValNat p n + 1) ∣ n
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<GOAL>padicValNat p n < padicValNat p n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>AEStronglyMeasurable f 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>a b : α<VAR>s : Set α<VAR>f : ι → α<GOAL>(iSup f)ᶜᶜ = (⨅ i, (f i)ᶜ)ᶜ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>x : G<GOAL>condexpIndSMul hm ⋯ ⋯ x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>x : G<GOAL>(compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) 0) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>g : F →L[𝕜] G<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y✝ : E<VAR>hy : y✝ ∈ EMetric.ball 0 r<GOAL>HasSum (fun n => (g.compFormalMultilinearSeries p n) fun x => y✝) ((⇑g ∘ f) (x + y✝))
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ b<GOAL>a + b = max a b
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>0 / a = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < (zipWith f l l').length<GOAL>i < l.length
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < min l.length l'.length<GOAL>i < l.length
<VAR>a b : ℝ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : IsNat b nb<VAR>pe' : IsRat (a ^ nb) num den<GOAL>IsRat (a ^ b) num den
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<GOAL>𝔠 ≤ #𝕜
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<GOAL>∃ f, range f ⊆ Set.univ ∧ Continuous f ∧ Injective f
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<GOAL>Perfect Set.univ
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<GOAL>∃ y ∈ U ∩ Set.univ, y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<GOAL>∃ y ∈ U ∩ Set.univ, y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 (x + 0))<GOAL>∃ y ∈ U ∩ Set.univ, y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)<GOAL>∃ y ∈ U ∩ Set.univ, y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)<VAR>B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U<GOAL>∃ y ∈ U ∩ Set.univ, y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)<VAR>B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U<VAR>n : ℕ<VAR>hn : x + c ^ n ∈ U<GOAL>∃ y ∈ U ∩ Set.univ, y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)<VAR>B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U<VAR>n : ℕ<VAR>hn : x + c ^ n ∈ U<GOAL>x + c ^ n ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)<VAR>B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U<VAR>n : ℕ<VAR>hn : x + c ^ n ∈ U<GOAL>¬c ^ n = 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>x : 𝕜<VAR>x✝ : x ∈ Set.univ<VAR>U : Set 𝕜<VAR>hU : U ∈ 𝓝 x<VAR>c : 𝕜<VAR>c_pos : 0 < ‖c‖<VAR>hc : ‖c‖ < 1<VAR>A : Tendsto (fun n => x + c ^ n) atTop (𝓝 x)<VAR>B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U<VAR>n : ℕ<VAR>hn : x + c ^ n ∈ U<GOAL>c ≠ 0
<VAR>b o : Ordinal.{u_1}<VAR>hbo : o < b<GOAL>log b o = 0
<VAR>b : Ordinal.{u_1}<VAR>hbo : 0 < b<GOAL>log b 0 = 0
<VAR>b o : Ordinal.{u_1}<VAR>hbo : o < b<VAR>ho : o ≠ 0<GOAL>log b o = 0
<VAR>b o : Ordinal.{u_1}<VAR>hbo : o < b<VAR>ho : o ≠ 0<VAR>hb : b ≤ 1<GOAL>log b o = 0
<VAR>b o : Ordinal.{u_1}<VAR>hbo : o < b<VAR>ho : o ≠ 0<VAR>hb : 1 < b<GOAL>log b o = 0
<VAR>α : Type u_1<VAR>f : Nat<VAR>n : α<VAR>l : List α<GOAL>insertNth f n l = insertNthTR f n l
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<VAR>hst : s ⊆ t<VAR>hs' : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>h : μ t < μ s + ε<GOAL>μ (t \ 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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<VAR>hst : s ⊆ t<VAR>hs' : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>h : μ t < μ s + ε<GOAL>μ t - μ 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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<VAR>hst : s ⊆ t<VAR>hs' : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>h : μ t < ε + μ s<GOAL>μ t - μ s < ε
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>0 < Nat.card α ↔ Nonempty α ∧ Finite α
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.45694, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>d e : ℤ<VAR>γ : Cochain F K d<VAR>he : 1 + d = e<VAR>hf : 0 + e = e<GOAL>(Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<GOAL>s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<VAR>hst : s.ncard ≤ t.ncard<VAR>a₁ : α<VAR>ha₁ : a₁ ∈ s<VAR>a₂ : α<VAR>ha₂ : a₂ ∈ s<VAR>ha₁a₂ : f a₁ ha₁ = f a₂ ha₂<VAR>hs : autoParam s.Finite _auto✝<GOAL>a₁ = a₂
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS b c d (2 * (↑m + 3)) = preNormEDS b c d (↑m + 2) ^ 2 * preNormEDS b c d (↑m + 3) * preNormEDS b c d (↑m + 5) - preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 3) * preNormEDS b c d (↑m + 4) ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS' b c d (2 * (m + 3)) = preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>inst✝ : DivisionCommMonoid G<VAR>f g : α → G<VAR>hs : s.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>ha : ∃ l, l < a<GOAL>(𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>ha : ∃ l, l < a<VAR>e_1✝ : α = αᵒᵈ<VAR>x✝ : α<GOAL>Ioc x✝ a = Ico a x✝
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<GOAL>(b - a) • slope f a b = f b -ᵥ f a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a : k<GOAL>(a - a) • slope f a a = f a -ᵥ f a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<VAR>hne : a ≠ b<GOAL>(b - a) • slope f a b = f b -ᵥ f a
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2<VAR>z x y : ℕ<GOAL>y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2<VAR>z x y : ℕ<GOAL>y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z = x / y
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Monoid G<VAR>h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom<GOAL>QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Monoid G<VAR>h : QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫ (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app (Rep.trivial k G k))<GOAL>QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1<GOAL>Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1<GOAL>Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Gamma) x - (log ∘ Gamma) 1))
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>(log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Monotone seq<VAR>hseq_tendsto : Tendsto seq atTop atTop<GOAL>∀ᵐ (c : β) ∂ν a, Tendsto (fun m => f (a, c) (seq m)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Monotone seq<VAR>hseq_tendsto : Tendsto seq atTop atTop<GOAL>∀ (n : ℕ), Integrable (fun c => f (a, c) (seq n)) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Monotone seq<VAR>hseq_tendsto : Tendsto seq atTop atTop<GOAL>Tendsto (fun i => ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 (∫ (a : β), 1 ∂ν a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Monotone seq<VAR>hseq_tendsto : Tendsto seq atTop atTop<GOAL>∀ᵐ (a_1 : β) ∂ν a, Monotone fun i => f (a, a_1) (seq i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Monotone seq<VAR>hseq_tendsto : Tendsto seq atTop atTop<GOAL>∀ᵐ (a_1 : β) ∂ν a, ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s t u : Finset α<VAR>hus : u ⊆ s ∪ t<VAR>hcard : u.card = mulRothNumber (s ∪ t)<VAR>hu : ThreeGPFree ↑u<GOAL>u.card = (u ∩ s ∪ u ∩ t).card
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : HasLineDerivWithinAt 𝕜 f f' t x v<VAR>hst : t ∈ 𝓝[s] x<GOAL>HasLineDerivWithinAt 𝕜 f f' s x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : HasLineDerivWithinAt 𝕜 f f' t x v<VAR>hst : t ∈ 𝓝[s] x<GOAL>(fun t => x + t • v) ⁻¹' t ∈ 𝓝[(fun t => x + t • v) ⁻¹' s] 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : HasLineDerivWithinAt 𝕜 f f' t x v<VAR>hst : t ∈ 𝓝[s] x<GOAL>ContinuousWithinAt (fun t => x + t • v) ((fun t => x + t • v) ⁻¹' s) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : HasLineDerivWithinAt 𝕜 f f' t x v<VAR>hst : t ∈ 𝓝[s] x<GOAL>Continuous fun t => x + t • v
<VAR>d : ℤ<VAR>b c : ℤ√d<VAR>hb : IsPell b<VAR>hc : IsPell c<GOAL>b * c * star (b * c) = 1
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R✝<VAR>m n✝ : ℕ<VAR>inst✝² : CommSemiring R✝<VAR>p q : R✝[X]<VAR>x✝ : R✝<VAR>inst✝¹ : CommSemiring S<VAR>f : R✝ →+* S<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>x : R<GOAL>eval x (∑ i ∈ range n, X ^ i) = ∑ i ∈ range n, x ^ i
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>u v : Rˣ<VAR>m n : ℕ<VAR>h : ↑u * ϖ ^ m = ↑v * ϖ ^ n<GOAL>u = v
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>u v : Rˣ<VAR>m : ℕ<VAR>h : ↑u * ϖ ^ m = ↑v * ϖ ^ m<GOAL>u = v
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>u v : Rˣ<VAR>m : ℕ<VAR>h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0<GOAL>u = v
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>u v : Rˣ<VAR>m : ℕ<VAR>h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0<GOAL>u = v
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<GOAL>IntegrableOn g' (Ioi a) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<GOAL>ContinuousWithinAt g (Ici a) a