ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>f f' : 𝕜 → E<VAR>z₀ z₁ : 𝕜<VAR>hcont : ContinuousOn (fun t => f' (z₀ + t • z₁)) (Icc 0 1)<VAR>hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)<VAR>γ : ℝ → 𝕜 := fun t => z₀ + t • z₁<VAR>hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1<VAR>hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t<GOAL>f (z₀ + z₁) - f z₀ = (f ∘ γ) 1 - (f ∘ γ) 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<GOAL>finrank ℤ ↥(unitLattice K) = rank K
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ✝ : F<VAR>s✝ t✝ : Set α<VAR>μ : F<VAR>s t : Set α<GOAL>μ s ≤ μ (s ∩ t) + μ (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>ha : a ∈ s<VAR>hst : { ofColex := s } ≤ { ofColex := s }<VAR>hcard : s.card ≤ s.card<VAR>ht : s.Nonempty<VAR>m : α := s.min' ht<GOAL>{ ofColex := s.erase a } ≤ { ofColex := s.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>hst : { ofColex := s } < { ofColex := t }<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>hst : ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>w : α<VAR>hwt : w ∈ t<VAR>hws : w ∉ s<VAR>hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>w : α<VAR>hwt : w ∈ t<VAR>hws : w ∉ s<VAR>hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)<VAR>hwa : w < a<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>w : α<VAR>hwt : w ∈ t<VAR>hws : w ∉ s<VAR>hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)<VAR>haw : a < w<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>hwt : m ∈ t<VAR>hws : m ∉ s<VAR>hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)<VAR>haw : a < m<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<VAR>ht : t.Nonempty<VAR>m : α := t.min' ht<VAR>h' : s ≠ t<VAR>w : α<VAR>hwt : w ∈ t<VAR>hws : w ∉ s<VAR>hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)<VAR>haw : a < w<VAR>hmw : m < w<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase m }
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>hAs : A.Definable L s<VAR>hAB : A ⊆ B<GOAL>B.Definable L s
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>hAs : ∅.Definable (L[[↑A]]) s<VAR>hAB : A ⊆ B<GOAL>∅.Definable (L[[↑B]]) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<GOAL>x ⩿ y → x.1 = y.1 ∨ x.2 = y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h : x ⩿ y<VAR>hab : ¬(x.1 = y.1 ∨ x.2 = y.2)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h : x ⩿ y<VAR>hab : x.1 ≠ y.1 ∧ x.2 ≠ y.2<GOAL>False
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>h : 0 < q<GOAL>ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<GOAL>ν.IsEverywherePos s ↔ μ.IsEverywherePos s
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<VAR>H : ν.IsEverywherePos s<GOAL>∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<VAR>H : ν.IsEverywherePos s<VAR>x : α<VAR>hx : x ∈ s<VAR>t : Set α<VAR>ht : t ∈ 𝓝 x<VAR>h't : ∀ u ⊆ t, ν u = μ u<GOAL>∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>inst✝ : Subsingleton ↥S<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>inst✝ : Subsingleton ↥S<GOAL>∀ x ∈ S, x = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>inst✝ : Subsingleton ↥S<VAR>y : M<VAR>hy : y ∈ S<GOAL>y = 1
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n] i0)<VAR>m : ℕ := (toZ i0 (succ^[n] i0)).toNat<GOAL>toZ i0 (succ^[n] i0) = ↑n
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n] i0)<VAR>m : ℕ := (toZ i0 (succ^[n] i0)).toNat<VAR>h_eq : succ^[m] i0 = succ^[n] i0<GOAL>toZ i0 (succ^[n] i0) = ↑n
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<VAR>hn : ¬IsMax (succ^[n] i0)<VAR>m : ℕ := (toZ i0 (succ^[n] i0)).toNat<VAR>h_eq : succ^[m] i0 = succ^[n] i0<VAR>hmn : ¬m = n<GOAL>IsMax (succ^[n] i0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>p : Set α → Prop<VAR>h : l.HasBasis (fun s => s ∈ l ∧ p s) id<VAR>V : Set α<VAR>hV : V ∈ l<GOAL>l.HasBasis (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : ι → Set β<VAR>hι : Nonempty ι<VAR>x : α × β<GOAL>x ∈ s ×ˢ ⋂ i, t i ↔ x ∈ ⋂ i, s ×ˢ t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : ι → Set β<VAR>hι : Nonempty ι<VAR>x : α × β<GOAL>(x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<GOAL>OpenEmbedding ⇑(D.ι i).base
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<GOAL>OpenEmbedding ⇑((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<GOAL>OpenEmbedding (⇑(D.gluedIso (forget C)).inv ∘ ⇑((D.mapGlueData (forget C)).ι i))
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<GOAL>Nontrivial (Dual K V) ↔ Nontrivial V
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>z : Sym2 α<GOAL>z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>z : Sym2 α<VAR>x y : α<GOAL>s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>P_max : P.IsMaximal<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<GOAL>∃ Q, Q.IsMaximal ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>P_max : P.IsMaximal<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>Q : Ideal S<VAR>Q_prime : Q.IsPrime<VAR>hQ : comap (algebraMap R S) Q = P<GOAL>∃ Q, Q.IsMaximal ∧ comap (algebraMap R S) Q = P
<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>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>ls : l ≤ 𝓟 (f '' s)<GOAL>∃ x ∈ f '' s, ClusterPt x l
<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>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this : (comap f l ⊓ 𝓟 s).NeBot<GOAL>∃ x ∈ f '' s, ClusterPt x l
<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>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<GOAL>∃ x ∈ f '' s, ClusterPt x l
<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>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this✝ : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<VAR>this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot<GOAL>∃ x ∈ f '' s, ClusterPt x l
<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>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this✝ : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<VAR>this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot<GOAL>ClusterPt (f x) l
<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>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this✝¹ : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<VAR>this✝ : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot<VAR>this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)<GOAL>ClusterPt (f x) l
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q : Karoubi (Karoubi C)<VAR>f : P ⟶ Q<GOAL>P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f
<GOAL>∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = √π
<GOAL>∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * ∫ (x : ℝ) in Ioi 0, rexp (-1 * x ^ 2)
<GOAL>√π = 2 * (√(π / 1) / 2)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>s : Submodule k V<VAR>x : V<GOAL>x ∈ s.toAffineSubspace.direction ↔ x ∈ s
<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>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>w x y : P<VAR>h₂ : Wbtw R w x y<VAR>h₁ : Wbtw R w y x<VAR>h : y ≠ x<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : ι × α → Prop<GOAL>(∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : ι × α → Prop<GOAL>(∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i).swap) ↔ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>C : Type u_2<VAR>inst✝¹³ : Category.{u_5, u_2} C<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : Linear R C<VAR>inst✝¹⁰ : MonoidalCategory C<VAR>inst✝⁹ : MonoidalPreadditive C<VAR>inst✝⁸ : MonoidalLinear R C<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_3} D<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : Linear R D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : MonoidalPreadditive D<VAR>F : MonoidalFunctor D C<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Functor.Linear R F.toFunctor<VAR>X Y Z : D<VAR>r : R<VAR>f : Y ⟶ Z<GOAL>X ◁ (r • f) = r • X ◁ f
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>C : Type u_2<VAR>inst✝¹³ : Category.{u_5, u_2} C<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : Linear R C<VAR>inst✝¹⁰ : MonoidalCategory C<VAR>inst✝⁹ : MonoidalPreadditive C<VAR>inst✝⁸ : MonoidalLinear R C<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_3} D<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : Linear R D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : MonoidalPreadditive D<VAR>F : MonoidalFunctor D C<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Functor.Linear R F.toFunctor<VAR>X Y Z : D<VAR>r : R<VAR>f : Y ⟶ Z<GOAL>F.map (X ◁ (r • f)) = F.map (r • X ◁ f)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>C : Type u_2<VAR>inst✝¹³ : Category.{u_5, u_2} C<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : Linear R C<VAR>inst✝¹⁰ : MonoidalCategory C<VAR>inst✝⁹ : MonoidalPreadditive C<VAR>inst✝⁸ : MonoidalLinear R C<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_3} D<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : Linear R D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : MonoidalPreadditive D<VAR>F : MonoidalFunctor D C<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Functor.Linear R F.toFunctor<VAR>X Y Z : D<VAR>r : R<VAR>f : Y ⟶ Z<GOAL>inv (F.μ X Y) ≫ F.obj X ◁ F.map (r • f) ≫ F.μ X Z = F.map (r • X ◁ f)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>C : Type u_2<VAR>inst✝¹³ : Category.{u_5, u_2} C<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : Linear R C<VAR>inst✝¹⁰ : MonoidalCategory C<VAR>inst✝⁹ : MonoidalPreadditive C<VAR>inst✝⁸ : MonoidalLinear R C<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_3} D<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : Linear R D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : MonoidalPreadditive D<VAR>F : MonoidalFunctor D C<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Functor.Linear R F.toFunctor<VAR>r : R<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>Z : D<GOAL>(r • f) ▷ Z = r • f ▷ Z
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>C : Type u_2<VAR>inst✝¹³ : Category.{u_5, u_2} C<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : Linear R C<VAR>inst✝¹⁰ : MonoidalCategory C<VAR>inst✝⁹ : MonoidalPreadditive C<VAR>inst✝⁸ : MonoidalLinear R C<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_3} D<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : Linear R D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : MonoidalPreadditive D<VAR>F : MonoidalFunctor D C<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Functor.Linear R F.toFunctor<VAR>r : R<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>Z : D<GOAL>F.map ((r • f) ▷ Z) = F.map (r • f ▷ Z)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>C : Type u_2<VAR>inst✝¹³ : Category.{u_5, u_2} C<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : Linear R C<VAR>inst✝¹⁰ : MonoidalCategory C<VAR>inst✝⁹ : MonoidalPreadditive C<VAR>inst✝⁸ : MonoidalLinear R C<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_3} D<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : Linear R D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : MonoidalPreadditive D<VAR>F : MonoidalFunctor D C<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Functor.Linear R F.toFunctor<VAR>r : R<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>Z : D<GOAL>inv (F.μ X Z) ≫ F.map (r • f) ▷ F.obj Z ≫ F.μ Y Z = F.map (r • f ▷ Z)
<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>m : α → β → γ<VAR>f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h✝ h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b✝ : β<VAR>c : γ<VAR>f : α → β → α<VAR>b : β<VAR>h : ∀ (a : α), f a b = a<VAR>l : Filter α<GOAL>map₂ f l (pure b) = l
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>a : (i : ι) → π i<GOAL>𝓝 a = Filter.pi fun i => 𝓝 (a i)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n m : ℕ<VAR>a : K<VAR>hm : Irreducible (X ^ m - C a)<VAR>hn : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))<GOAL>Irreducible (X ^ (n * m) - C a)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n m : ℕ<VAR>a : K<VAR>hm : Irreducible (X ^ m - C a)<VAR>hn : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))<VAR>hm' : m ≠ 0<GOAL>Irreducible (X ^ (n * m) - C a)
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : gcd x y = 0<GOAL>y ∣ lcm x y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : gcd x y = 0<GOAL>y ∣ 0
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : ¬gcd x y = 0<VAR>z : R<VAR>hz : x = gcd x y * z<GOAL>gcd x y * (y * z) = x * y
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : C<VAR>f : Y ≅ Z<GOAL>X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z)
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport g
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport g
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ (f g : α → E), Continuous f ∧ Memℒp f p μ ∧ HasCompactSupport f → Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport g → Continuous (f + g) ∧ Memℒp (f + g) p μ ∧ HasCompactSupport (f + g)
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ (f : α → E), Continuous f ∧ Memℒp f p μ ∧ HasCompactSupport f → AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport g