ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f : γ → β → γ<VAR>b : β<VAR>h : ∀ (a : γ), f a b = a<VAR>s : Finset γ<GOAL>image₂ f s {b} = s
<VAR>c : Cardinal.{u}<VAR>n : ℕ<GOAL>c ^ ↑n ≤ max c ℵ₀
<VAR>c : Cardinal.{u}<VAR>n : ℕ<VAR>hc : ℵ₀ ≤ c<GOAL>c ^ ↑n ≤ max c ℵ₀
<VAR>c : Cardinal.{u}<VAR>n : ℕ<VAR>hc : c < ℵ₀<GOAL>c ^ ↑n ≤ max c ℵ₀
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<GOAL>Presheaf.IsLocallyInjective J ((sheafToPresheaf J D).map φ) ↔ IsLocallyInjective φ
<VAR>n✝ n b e : ℕ<VAR>h_b_pos : 0 < b<GOAL>n < b ^ e.succ → n / b < b ^ e
<VAR>n✝ n b e : ℕ<VAR>h_b_pos : 0 < b<GOAL>n < b ^ e * b → n / b < b ^ e
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hk' : n + k < l.length<VAR>hk : optParam (n + k + 1 < (insertNth n x l).length) ⋯<GOAL>(insertNth n x l).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<VAR>quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<VAR>quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0<VAR>rbar_root : eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r) (Polynomial.map (Quotient.mk (comap f I)) p) = 0<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<VAR>quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0<VAR>rbar_root : eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r) (Polynomial.map (Quotient.mk (comap f I)) p) = 0<VAR>i : ℕ<VAR>ne_zero : (Polynomial.map (Quotient.mk (comap f I)) p).coeff i ≠ 0<VAR>mem : (Polynomial.map (Quotient.mk (comap f I)) p).coeff i ∈ comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<VAR>quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0<VAR>rbar_root : eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r) (Polynomial.map (Quotient.mk (comap f I)) p) = 0<VAR>i : ℕ<VAR>ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0<VAR>mem : (Quotient.mk (comap f I)) (p.coeff i) ∈ comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)<GOAL>∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<VAR>quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0<VAR>rbar_root : eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r) (Polynomial.map (Quotient.mk (comap f I)) p) = 0<VAR>i : ℕ<VAR>ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0<VAR>mem : (Quotient.mk (comap f I)) (p.coeff i) ∈ comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)<GOAL>(Quotient.mk I) (f (p.coeff i)) ∈ map (Quotient.mk I) J
<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✝ : I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>p : R[X]<VAR>p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0<VAR>hpI : eval₂ f r p ∈ I<VAR>hrJ : r ∈ ↑J<VAR>hrI : r ∉ ↑I<VAR>rbar_ne_zero : (Quotient.mk I) r ≠ 0<VAR>rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J<VAR>quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0<VAR>rbar_root : eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r) (Polynomial.map (Quotient.mk (comap f I)) p) = 0<VAR>i : ℕ<VAR>ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0<VAR>mem : (Quotient.mk (comap f I)) (p.coeff i) ∈ comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)<GOAL>p.coeff i ∈ ↑(comap f I) → (Quotient.mk (comap f I)) (p.coeff i) = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ : Set α<VAR>ν : Measure α<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((μ + ν).trim hm) s = (μ.trim hm + ν.trim hm) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b c : α<GOAL>(a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) + (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>inst✝ : MeasurableSpace β<VAR>μb : Measure β<VAR>f : α → β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hμs : μb s ≠ ⊤<VAR>c : E<VAR>hf : MeasurePreserving f μ μb<GOAL>μ (f ⁻¹' s) ≠ ⊤
<VAR>this : -(π / 2) < π / 2<GOAL>Tendsto (fun x => tan ↑x) atBot atBot
<VAR>this : -(π / 2) < π / 2<GOAL>Tendsto tan (𝓝[>] (-(π / 2))) atBot
<VAR>this : -(π / 2) < π / 2<GOAL>Tendsto (fun x => tan ↑x) atTop atTop
<VAR>this : -(π / 2) < π / 2<GOAL>Tendsto tan (𝓝[<] (π / 2)) atTop
<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>f : α × β → M<VAR>hf : (mulSupport f).Finite<VAR>h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a<VAR>h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ hf.toFinset), f a<GOAL>∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<GOAL>¬Tendsto diracProba L (𝓝 (diracProba x))
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<GOAL>¬Tendsto diracProba L (𝓝 (diracProba x))
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<GOAL>¬Tendsto diracProba L (𝓝 (diracProba x))
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<GOAL>¬Tendsto diracProba L (𝓝 (diracProba x))
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<GOAL>∃ x_1, ¬Tendsto (fun i => ∫⁻ (ω : X), ↑(x_1 ω) ∂↑(diracProba i)) L (𝓝 (∫⁻ (ω : X), ↑(x_1 ω) ∂↑(diracProba x)))
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<GOAL>¬Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) L (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<GOAL>¬Tendsto (fun i => ↑(f i)) L (𝓝 ↑1)
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<GOAL>∃ s ∈ 𝓝 ↑1, ∃ᶠ (x : X) in L, ↑(f x) ∉ s
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<GOAL>∀ x ∉ U, ↑(f x) ∉ Ioi 0
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x✝ : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x✝)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x✝<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x✝<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x✝ = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<VAR>x : X<VAR>x_notin_U : x ∉ U<GOAL>↑(f x) ∉ Ioi 0
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>x✝ : X<VAR>L : Filter X<VAR>h : ¬Tendsto id L (𝓝 x✝)<VAR>U : Set X<VAR>U_nhd : U ∈ 𝓝 x✝<VAR>hU : ∃ᶠ (x : X) in L, x ∉ U<VAR>Uint_nhd : interior U ∈ 𝓝 x✝<VAR>f : X →ᵇ ℝ≥0<VAR>fx_eq_one : f x✝ = 1<VAR>f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0<VAR>x : X<VAR>x_notin_U : x ∉ U<GOAL>↑0 ∉ Ioi 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : CommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(∏ i : ι, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalSpace Z<VAR>proj : Z → B<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>Continuous proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalSpace Z<VAR>e : Z ≃ₜ B × F<VAR>h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)<GOAL>Continuous (Prod.fst ∘ ⇑e)
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>μ : FiniteMeasure Ω<VAR>A : Set Ω<GOAL>μ.restrict A = 0 ↔ μ A = 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<GOAL>(∀ (X Y : C), HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ ((CochainComplex.singleFunctor C 0).obj X) ((CochainComplex.singleFunctor C 0).obj Y)) ↔ ∀ (X Y : C) (n : ℤ), Small.{w, w'} ((DerivedCategory.singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<GOAL>(∀ (X Y : C) (a b : ℤ), Small.{w, w'} ((shiftFunctor (DerivedCategory C) a).obj (DerivedCategory.Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶ (shiftFunctor (DerivedCategory C) b).obj (DerivedCategory.Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))) ↔ ∀ (X Y : C) (n : ℤ), Small.{w, w'} ((DerivedCategory.singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>hs' : s.Nonempty<GOAL>count s ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>hs' : s.Nonempty<GOAL>¬s = ∅
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<VAR>hb : IsRightRegular b<GOAL>a * b = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<VAR>hb : IsRightRegular b<GOAL>a * b = 0 * b ↔ a = 0
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>B : Type uB<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝⁵ : (i : ι) → Module R (A i)<VAR>inst✝⁴ : AddMonoid ι<VAR>inst✝³ : GSemiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : GAlgebra R A<VAR>inst✝ : Algebra R B<VAR>f : (i : ι) → A i →ₗ[R] B<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>r : R<GOAL>(toModule R ι B f) ((algebraMap R (⨁ (i : ι), A i)) r) = (algebraMap R B) r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪x, x⟫_𝕜 - ⟪y, x⟫_𝕜 - (⟪x, y⟫_𝕜 - ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℕ<GOAL>a⁻¹ ^ ↑n = (a ^ ↑n)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℕ<GOAL>a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>hs : LinearIndependent K fun (b : ↑s) => ↑b<VAR>hx : x ∉ span K s<GOAL>LinearIndependent K fun (b : ↑(insert x s)) => ↑b
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>hs : LinearIndependent K fun (b : ↑s) => ↑b<VAR>hx : x ∉ span K s<GOAL>LinearIndependent K fun (b : ↑(s ∪ {x})) => ↑b
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>hs : LinearIndependent K fun (b : ↑s) => ↑b<VAR>hx : x ∉ span K s<VAR>x0 : x ≠ 0<GOAL>LinearIndependent K fun (b : ↑(s ∪ {x})) => ↑b
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>hs : LinearIndependent K fun (b : ↑s) => ↑b<VAR>hx : x ∉ span K s<VAR>x0 : x ≠ 0<GOAL>Disjoint (span K s) (span K {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n✝ : Type u_4<VAR>R : Type u_5<VAR>n : Type u_6<VAR>inst✝³ : Semiring α<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : AddGroup n<VAR>inst✝ : Fintype n<VAR>a : α<VAR>i j : n<GOAL>circulant (Pi.single 0 a) i j = (scalar n) a i j
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => a.1 ≤ k) = (fun a => a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<GOAL>filter (fun a => a.1 ≤ k) (antidiagonal n) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (antidiagonal k)
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => a.1 ≤ k) = (fun a => a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<VAR>aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j<GOAL>filter (fun a => a.1 ≤ k) (antidiagonal n) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (antidiagonal k)
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => a.1 ≤ k) = (fun a => a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<VAR>aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j<GOAL>filter (fun a => a.1 ≤ k) (map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n)) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (antidiagonal k)
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => a.1 ≤ k) = (fun a => a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<VAR>aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j<GOAL>map (({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding) (antidiagonal k) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (antidiagonal k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>f : β → α<VAR>s : Finset β<GOAL>∏ x ∈ s, f x = ∏' (x : β), (↑s).mulIndicator f x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<GOAL>ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<GOAL>(ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)) ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>hc : ContinuousSMul G X<GOAL>(∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)) ↔ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>hc : ContinuousSMul G X<VAR>𝒰 : Ultrafilter (G × X)<VAR>x₁ x₂ : X<VAR>hxx : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))<VAR>g : G<GOAL>g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g) ↔ Tendsto fst (↑𝒰) (𝓝 g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<VAR>V : Set X<VAR>h : V ∈ 𝓝 x<VAR>h' : V ∩ s = {x}<GOAL>{x}ᶜ ∩ V ∩ s = ∅
<VAR>α : Type u_1<VAR>xs : List α<VAR>ns : List Nat<GOAL>xs.takeList ns = xs.takeListTR ns