ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type uι<VAR>inst✝¹⁰ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝³ : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝² : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>u : E i →L[𝕜] E' i<GOAL>↑u = ↑(update f i u i) ∧ ∀ (x : ι), x ≠ i → ↑(f x) = ↑(update f i u x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>n : ℕ<GOAL>card (n • s) = n * card s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>F : Type u_5<VAR>inst✝ : Monoid F<VAR>c : F → M → M<VAR>h1 : c 1 = id<VAR>hmul : ∀ (f g : F), c (f * g) = c f ∘ c g<VAR>f : F<GOAL>c (f ^ 0) = (c f)^[0]
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>F : Type u_5<VAR>inst✝ : Monoid F<VAR>c : F → M → M<VAR>h1 : c 1 = id<VAR>hmul : ∀ (f g : F), c (f * g) = c f ∘ c g<VAR>f : F<GOAL>id = (c f)^[0]
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>F : Type u_5<VAR>inst✝ : Monoid F<VAR>c : F → M → M<VAR>h1 : c 1 = id<VAR>hmul : ∀ (f g : F), c (f * g) = c f ∘ c g<VAR>f : F<VAR>n : ℕ<GOAL>c (f ^ (n + 1)) = (c f)^[n + 1]
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<GOAL>{I | I.IsMaximal}.Finite
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<GOAL>{I | I.IsPrime}.Finite
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>h : (x - y) ^ n = 0<GOAL>x ^ m ∣ y ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>h : (x - y) ^ n = 0<GOAL>x ^ m ∣ (y - x + x) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>h : (x - y) ^ n = 0<GOAL>(y - x) ^ n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Tendsto (fun r => (ρ.IicSnd ↑r) s) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<GOAL>Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<GOAL>Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<GOAL>Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<GOAL>Antitone fun r => s ×ˢ Iic ↑(-r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<VAR>q r : ℚ<VAR>hqr : q ≤ r<VAR>x : ℝ<VAR>hx : x ∈ Iic ↑(-r)<GOAL>x ∈ Iic ↑(-q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<VAR>q r : ℚ<VAR>hqr : q ≤ r<VAR>x : ℝ<VAR>hx : x ≤ -↑r<GOAL>x ≤ -↑q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h_empty : ρ (s ×ˢ ∅) = 0<VAR>q r : ℚ<VAR>hqr : q ≤ r<VAR>x : ℝ<VAR>hx : x ≤ -↑r<GOAL>↑q ≤ ↑r
<VAR>z : ℂ<GOAL>(norm ℝ) z = normSq z
<VAR>z : ℂ<GOAL>!![z.re, -z.im; z.im, z.re] 0 0 * !![z.re, -z.im; z.im, z.re] 1 1 - !![z.re, -z.im; z.im, z.re] 0 1 * !![z.re, -z.im; z.im, z.re] 1 0 = z.re * z.re + z.im * z.im
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>this : MeasurableSpace Ω := ⨆ n, ↑ℱ n<GOAL>∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>this : MeasurableSpace Ω := ⨆ n, ↑ℱ n<GOAL>μ {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)} = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>this : MeasurableSpace Ω := ⨆ n, ↑ℱ n<GOAL>MeasurableSet {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)}
<VAR>n : ℕ<GOAL>(n + 0 - 1).descFactorial 0 = n.ascFactorial 0
<VAR>n k : ℕ<GOAL>(n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>a n' : ℤ<VAR>γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>m m' : ℤ<VAR>hm' : m + a = m'<GOAL>δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n✝<VAR>a n' n : ℤ<VAR>hn : n + a = n'<VAR>m m' : ℤ<VAR>hm' : m + a = m'<VAR>γ' : Cochain K L n<GOAL>δ n m (((leftShiftAddEquiv K L n a n' hn) γ').leftUnshift n hn) = a.negOnePow • (δ n' m' ((leftShiftAddEquiv K L n a n' hn) γ')).leftUnshift m hm'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n✝<VAR>a n' n : ℤ<VAR>hn : n + a = n'<VAR>m m' : ℤ<VAR>hm' : m + a = m'<VAR>γ' : Cochain K L n<GOAL>δ n m ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{?u.16886, u_1} C<VAR>inst✝⁶ : Category.{?u.16890, u_2} D<VAR>inst✝⁵ : Category.{?u.16894, u_3} E<VAR>inst✝⁴ : Category.{?u.16898, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>n m mn : A<VAR>hnm : m + n = mn<VAR>a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.16894, u_3} E<VAR>inst✝⁴ : Category.{?u.16898, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>n m mn : A<VAR>hnm : m + n = mn<VAR>a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).hom.app X = (shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X) ≫ (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>h : finrank ℚ K = 1<GOAL>NrComplexPlaces K = 0
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Iio ⊤ = univ
<GOAL>StrictConcaveOn ℝ (Set.Ici 0) negMulLog
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha_top : a ≠ ⊤<VAR>ha_zero : ¬a = 0<VAR>g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x<GOAL>limsup (fun x => a * u x) f = a * limsup u f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha_top : a ≠ ⊤<VAR>ha_zero : ¬a = 0<VAR>g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x<VAR>hg_bij : Function.Bijective g<GOAL>limsup (fun x => a * u x) f = a * limsup u f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha_top : a ≠ ⊤<VAR>ha_zero : ¬a = 0<VAR>g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x<VAR>hg_bij : Function.Bijective g<VAR>hg_mono : StrictMono g<GOAL>limsup (fun x => a * u x) f = a * limsup u f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha_top : a ≠ ⊤<VAR>ha_zero : ¬a = 0<VAR>g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x<VAR>hg_bij : Function.Bijective g<VAR>hg_mono : StrictMono g<VAR>g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective g hg_mono ⋯<GOAL>limsup (fun x => a * u x) f = a * limsup u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>y : α<VAR>ys : List α<VAR>f : List α → β<GOAL>(permutationsAux2 t ts r (y :: ys) f).2 = f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun x => f (y :: x)).2
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Tendsto (fun x => x ^ (-↑n)) atTop (𝓝 0)
<VAR>m✝ n a b c d m : ℕ<VAR>h : a ≡ b [MOD m * n]<GOAL>a ≡ b [MOD n]
<VAR>m✝ n a b c d m : ℕ<VAR>h : ↑(m * n) ∣ ↑b - ↑a<GOAL>↑n ∣ ↑b - ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ⊤
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (wittMul p n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (X 0 * X 1) = 0
<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>ι : Type u_7<VAR>α : ι → Type u_8<VAR>inst✝ : (i : ι) → TopologicalSpace (α i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (α i)<VAR>x : (i : ι) → α i<GOAL>x ∈ closure (I.pi s) ↔ ∀ i ∈ I, x i ∈ closure (s i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>a ⊓ b ∈ s
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.44478, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : (HomologicalComplex V c)ᵒᵖ<VAR>i✝ : ι<GOAL>((opFunctor V c).map ((opUnitIso V c).hom.app X) ≫ (opCounitIso V c).hom.app ((opFunctor V c).obj X)).f i✝ = (𝟙 ((opFunctor V c).obj X)).f i✝
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.44478, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : (HomologicalComplex V c)ᵒᵖ<VAR>i✝ : ι<GOAL>(Iso.refl ((unop X).op.unopSymm.X i✝)).hom.op ≫ (Iso.refl (((opInverse V c ⋙ opFunctor V c).obj ((opFunctor V c).obj X)).X i✝)).hom = (𝟙 ((opFunctor V c).obj X)).f i✝
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : Set A<GOAL>(adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))
<VAR>f : ℂ → ℂ<VAR>c z : ℂ<VAR>R R₁ R₂ : ℝ<VAR>hd : DifferentiableOn ℂ f (ball c R)<VAR>h_maps : MapsTo f (ball c R) (ball c R)<VAR>hc : f c = c<VAR>hz : z ∈ ball c R<GOAL>dist (f z) c ≤ dist z c
<VAR>f : ℂ → ℂ<VAR>c z : ℂ<VAR>R R₁ R₂ : ℝ<VAR>hd : DifferentiableOn ℂ f (ball c R)<VAR>h_maps : MapsTo f (ball c R) (ball c R)<VAR>hc : f c = c<VAR>hz : z ∈ ball c R<VAR>this : dist (f z) (f c) ≤ R / R * dist z c<GOAL>dist (f z) c ≤ dist z c
<VAR>f : ℂ → ℂ<VAR>c z : ℂ<VAR>R R₁ R₂ : ℝ<VAR>hd : DifferentiableOn ℂ f (ball c R)<VAR>h_maps : MapsTo f (ball c R) (ball c R)<VAR>hc : f c = c<VAR>hz : z ∈ ball c R<VAR>this : dist (f z) c ≤ R / R * dist z c<GOAL>R ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(fun x => -f' x) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(∃ c, IsBigOWith c l (fun x => -f' x) g) ↔ ∃ c, IsBigOWith c l f' g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁵ : NonAssocSemiring α<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : NonAssocSemiring β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : NonAssocSemiring γ<VAR>inst✝ : Preorder γ<VAR>f g : α ≃+*o β<VAR>h : f.toOrderRingHom = g.toOrderRingHom<GOAL>(fun f => ⇑f) f = (fun f => ⇑f) g
<VAR>u : ℤˣ<GOAL>↑u * ↑u = 1
<VAR>Y : Type u_1<VAR>inst✝ : TopologicalSpace Y<GOAL>SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
<VAR>Y : Type u_1<VAR>inst✝ : TopologicalSpace Y<VAR>a✝¹ a✝ : Y<GOAL>(∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)
<VAR>Y : Type u_1<VAR>inst✝ : TopologicalSpace Y<VAR>a✝¹ a✝ : Y<GOAL>(∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝).Rel x y
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>size✝ : ℕ<VAR>l✝ : Ordnode α<VAR>x✝ : α<VAR>r✝ : Ordnode α<GOAL>All P (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f : Y → Set X<VAR>e : U = ⋃ i, f i<VAR>hf : ∀ (i : Y), f i ∈ range b<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f : Y → Set X<VAR>e : U = ⋃ i, f i<VAR>f' : Y → ι<VAR>hf' : ∀ (i : Y), b (f' i) = f i<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f : Y → Set X<VAR>e : U = ⋃ i, f i<VAR>f' : Y → ι<VAR>hf' : ∀ (i : Y), b (f' i) = f i<VAR>this : b ∘ f' = f<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f' : Y → ι<VAR>e : U = ⋃ i, (b ∘ f') i<VAR>hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t✝ : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f' : Y → ι<VAR>e : U = ⋃ i, (b ∘ f') i<VAR>hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i<VAR>t : Finset Y<VAR>ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t✝ : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f' : Y → ι<VAR>e : U = ⋃ i, (b ∘ f') i<VAR>hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i<VAR>t : Finset Y<VAR>ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i<GOAL>U ≤ ⋃ i ∈ ↑(Finset.image f' t), b i
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y✝<VAR>s t✝ : Set X<VAR>b : ι → Set X<VAR>hb : IsTopologicalBasis (range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>Y : Type u<VAR>f' : Y → ι<VAR>e : U = ⋃ i, (b ∘ f') i<VAR>hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i<VAR>t : Finset Y<VAR>ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i<GOAL>⋃ i ∈ ↑(Finset.image f' t), b i ≤ U
<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 : MvPolynomial σ R<VAR>f : σ → τ<VAR>p : MvPolynomial σ R<VAR>b : τ →₀ ℕ<GOAL>b ∈ ((rename f) p).support → (b.sum fun x e => e) ≤ p.totalDegree
<VAR>α : Type u_1<VAR>c : RBColor<VAR>n : Nat<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<VAR>hr : r.Balanced c n<GOAL>(l.balance2 v r).reverse.reverse = node black l v r
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>(gaussianReal μ v) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring R<VAR>a b : R<VAR>n✝ n : ℕ<GOAL>(-1) ^ n = (-1) ^ (n % 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring R<VAR>a b : R<VAR>n✝ n : ℕ<GOAL>(-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>f✝ : α → ℝ<VAR>s✝ : Set α<VAR>x : α<VAR>ι : Type u_2<VAR>f g : ι → ℝ<VAR>s : Finset ι<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<GOAL>∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)
<VAR>α✝ : Type u<VAR>inst✝² : DecidableEq α✝<VAR>β : Type v<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>σ : α → Perm β<VAR>l : List α<VAR>hl : l.Nodup<VAR>mem_l : ∀ (a : α), a ∈ l<VAR>a : α<VAR>b : β<GOAL>(List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (a, b)
<VAR>α✝ : Type u<VAR>inst✝² : DecidableEq α✝<VAR>β : Type v<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>σ : α → Perm β<VAR>l : List α<VAR>hl : l.Nodup<VAR>mem_l : ∀ (a : α), a ∈ l<VAR>a : α<VAR>b : β<GOAL>a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨ a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
<VAR>α✝ : Type u<VAR>inst✝² : DecidableEq α✝<VAR>β : Type v<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>σ : α → Perm β<VAR>a : α<VAR>b : β<VAR>a' : α<VAR>l : List α<VAR>ih : l.Nodup → a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨ a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)<VAR>hl : (a' :: l).Nodup<GOAL>a ∈ a' :: l ∧ (List.map (fun a => prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, (σ a) b) ∨ a ∉ a' :: l ∧ (List.map (fun a => prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, b)
<VAR>α✝ : Type u<VAR>inst✝² : DecidableEq α✝<VAR>β : Type v<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>σ : α → Perm β<VAR>a : α<VAR>b : β<VAR>a' : α<VAR>l : List α<VAR>ih : l.Nodup → a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨ a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)<VAR>hl : (a' :: l).Nodup<GOAL>a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨ a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)
<VAR>α✝ : Type u<VAR>inst✝² : DecidableEq α✝<VAR>β : Type v<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>σ : α → Perm β<VAR>a : α<VAR>b : β<VAR>a' : α<VAR>l : List α<VAR>ih : l.Nodup → a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨ a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)<VAR>hl : (a' :: l).Nodup<VAR>mem_l : a ∈ l<VAR>prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)<GOAL>a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b) ∨ a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, b)