ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>s t : Set α<VAR>a✝ b✝ c : α<VAR>h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : ⊥ ∈ s<VAR>hab : b = ⊥<VAR>this : a = b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝³ : ConditionallyCompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sInf (s / t) = sInf s / sSup t
<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>c : F<VAR>hμ : μ ≠ 0<GOAL>eLpNormEssSup (fun x => c) μ = ↑‖c‖₊
<VAR>y : ℝ<GOAL>WithBot.some ∘ WithTop.some ⁻¹' Iio ↑↑y = Iio y
<VAR>y : ℝ<GOAL>WithTop.some ⁻¹' (WithBot.some ⁻¹' Iio ↑↑y) = Iio y
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<GOAL>IsCoprime x.num x.denom
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>IsCoprime ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>IsCoprime (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)) (C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>s : Finset α<GOAL>s.toList.length = s.card
<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>hab : a ≤ b<VAR>hcont : ContinuousOn f (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>f'int : IntervalIntegrable f' volume a b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<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>hab : a ≤ b<VAR>hcont : ContinuousOn f (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>f'int : IntervalIntegrable f' volume a b<VAR>g : NormedSpace.Dual ℝ E<GOAL>g (∫ (y : ℝ) in a..b, f' y) = g (f b - f a)
<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>hab : a ≤ b<VAR>hcont : ContinuousOn f (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>f'int : IntervalIntegrable f' volume a b<VAR>g : NormedSpace.Dual ℝ E<GOAL>∫ (x : ℝ) in a..b, g (f' x) = g (f b) - g (f a)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(∏ μ ∈ primitiveRoots n R, (X - C μ)).natDegree = n.totient
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>∑ i ∈ primitiveRoots n R, (X - C i).natDegree = n.totient
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>∀ i ∈ primitiveRoots n R, X - C i ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>z : R<VAR>a✝ : z ∈ primitiveRoots n R<GOAL>X - C z ≠ 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x✝ : X<VAR>s✝ : Set X<VAR>x : X<VAR>s : Set X<VAR>h : s ∈ 𝓝 x<GOAL>∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x✝ : X<VAR>s✝ : Set X<VAR>x : X<VAR>s : Set X<VAR>h : s ∈ 𝓝 x<VAR>h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s<GOAL>∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroupWithOne G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x + ↑n) = f x + n • b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>x : ℕ<GOAL>x ∈ (map f p).support → x ∈ p.support
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>x : ℕ<GOAL>x ∉ p.support → x ∉ (map f p).support
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>logb b x < logb b y ↔ y < x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>log y < log x ↔ y < x
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : t ⊆ s<GOAL>⋃₀ insert t ↑(hC.diffFinset hs ht) = s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : t ⊆ s<GOAL>⋃₀ insert t ↑(hC.diffFinset hs ht) = t ∪ ⋃₀ ↑(hC.diffFinset hs ht)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>g : Y ⟶ X<VAR>inv_hom_id : g ≫ f = 𝟙 Y<GOAL>inv f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>g : Y ⟶ X<VAR>inv_hom_id : g ≫ f = 𝟙 Y<GOAL>inv f ≫ f = g ≫ f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>h₁ : IsMulFreimanHom n A B₁ f₁<VAR>h₂ : IsMulFreimanHom n A B₂ f₂<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>(map (f₁ * f₂) s).prod = (map (f₁ * f₂) t).prod
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>s : Finset P<VAR>w : P → k<GOAL>(affineCombination k s.attach Subtype.val) (w ∘ Subtype.val) = (affineCombination k s id) w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, Tendsto (f (a, b)) atBot (𝓝 0)
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq k<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>a : m<VAR>b : n<VAR>c : k<GOAL>(single a b).toMatrix * (single b c).toMatrix = (single a c).toMatrix
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>k : ℕ<GOAL>multichoose 0 (k + 1) = 0
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>k : ℕ<GOAL>(fun x => (k + 1).factorial • x) (multichoose 0 (k + 1)) = (fun x => (k + 1).factorial • x) 0
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>k : ℕ<GOAL>(k + 1).factorial • multichoose 0 (k + 1) = (k + 1).factorial • 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>s t : Finset α<VAR>a b : α<GOAL>(∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>((PartialEquiv.refl α).trans e).source = e.source
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d = 1<GOAL>P.toPoly.Monic
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<GOAL>∃ i, V i ⊆ U
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<VAR>W : Set X<VAR>hsubW : ⋂ i, V i ⊆ W<VAR>W_op : IsOpen W<VAR>hWU : W ⊆ U<GOAL>∃ i, V i ⊆ U
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<VAR>W : Set X<VAR>hsubW : ⋂ i, V i ⊆ W<VAR>W_op : IsOpen W<VAR>hWU : W ⊆ U<GOAL>∃ i, V i ⊆ W
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<VAR>W : Set X<VAR>hsubW : ⋂ i, V i ⊆ W<VAR>W_op : IsOpen W<VAR>hWU : W ⊆ U<VAR>H : ∀ (i : ι), ¬V i ⊆ W<GOAL>False
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<VAR>W : Set X<VAR>hsubW : ⋂ i, V i ⊆ W<VAR>W_op : IsOpen W<VAR>hWU : W ⊆ U<VAR>H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty<GOAL>False
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<VAR>W : Set X<VAR>hsubW : ⋂ i, V i ⊆ W<VAR>W_op : IsOpen W<VAR>hWU : W ⊆ U<VAR>H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty<VAR>this : (⋂ i, V i ∩ Wᶜ).Nonempty<GOAL>False
<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>inst✝ : Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<VAR>W : Set X<VAR>hsubW : ⋂ i, V i ⊆ W<VAR>W_op : IsOpen W<VAR>hWU : W ⊆ U<VAR>H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty<VAR>this✝ : (⋂ i, V i ∩ Wᶜ).Nonempty<VAR>this : ¬⋂ i, V i ⊆ W<GOAL>False
<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 α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : IsBigOWith c l f g<VAR>h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<GOAL>IsBigOWith c l (fun x => (g x)⁻¹) fun x => (f x)⁻¹
<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 α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : IsBigOWith c l f g<VAR>h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<VAR>x : α<VAR>h₀ : f x = 0 → g x = 0<VAR>hle : ‖f x‖ ≤ c * ‖g x‖<GOAL>‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
<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 α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : IsBigOWith c l f g<VAR>h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<VAR>x : α<VAR>h₀ : f x = 0 → g x = 0<VAR>hle : ‖f x‖ ≤ c * ‖g x‖<VAR>hx : f x = 0<GOAL>‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
<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 α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : IsBigOWith c l f g<VAR>h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<VAR>x : α<VAR>h₀ : f x = 0 → g x = 0<VAR>hle : ‖f x‖ ≤ c * ‖g x‖<VAR>hx : f x ≠ 0<GOAL>‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > (map (⇑f) μ) A<GOAL>∃ U ⊇ A, IsOpen U ∧ (map (⇑f) μ) U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ (⇑f.symm '' A)<GOAL>∃ U ⊇ A, IsOpen U ∧ (map (⇑f) μ) U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ (⇑f.symm '' A)<VAR>U : Set α<VAR>hAU : U ⊇ ⇑f.symm '' A<VAR>hUo : IsOpen U<VAR>hU : μ U < r<GOAL>∃ U ⊇ A, IsOpen U ∧ (map (⇑f) μ) U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ (⇑f.symm '' A)<VAR>U : Set α<VAR>hAU : U ⊇ ⇑f.symm '' A<VAR>hUo : IsOpen U<VAR>hU : μ U < r<VAR>this : IsOpen (⇑f.symm ⁻¹' U)<GOAL>∃ U ⊇ A, IsOpen U ∧ (map (⇑f) μ) U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ (⇑f.symm '' A)<VAR>U : Set α<VAR>hAU : U ⊇ ⇑f.symm '' A<VAR>hUo : IsOpen U<VAR>hU : μ U < r<VAR>this : IsOpen (⇑f.symm ⁻¹' U)<GOAL>(map (⇑f) μ) (⇑f.symm ⁻¹' U) < r
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>M.LinearDisjoint 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>Function.Injective ⇑(M.subtype ∘ₗ ↑M.rTensorOne)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 < b<GOAL>Tendsto (fun x => (b * rexp x + c) / x ^ n) atTop atTop
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>hb : 0 < b<GOAL>Tendsto (fun x => (b * rexp x + c) / x ^ 0) atTop atTop
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 < b<VAR>hn : n ≠ 0<GOAL>Tendsto (fun x => (b * rexp x + c) / x ^ n) atTop atTop
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 < b<VAR>hn : n ≠ 0<GOAL>Tendsto (fun x => b * (rexp x / x ^ n) + c / x ^ n) atTop atTop
<VAR>l m r : List Char<VAR>f : Char → Bool<GOAL>{ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.any f = m.any f
<VAR>α : Type u_1<VAR>c : RBColor<VAR>n : Nat<VAR>cmp : α → α → Ordering<VAR>v : α<VAR>t : RBNode α<VAR>h : t.Balanced c n<GOAL>∃ c' n', (match t.isRed with | red => (ins cmp v t).setBlack | black => ins cmp v t).Balanced c' n'
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g f : NormedAddGroupHom V₁ V₂<VAR>K : ℝ≥0<VAR>hf : LipschitzWith K ⇑f<VAR>x : V₁<GOAL>‖f x‖ ≤ ↑K * ‖x‖
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C = (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Tendsto (fun r => (ρ.IicSnd ↑r) s) atTop (𝓝 (ρ.fst s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (s ×ˢ univ)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (⋃ i, s ×ˢ Iic ↑i)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r q : ℚ<VAR>hr_le_q : r ≤ q<VAR>x : α × ℝ<GOAL>x ∈ s ×ˢ Iic ↑r → x ∈ s ×ˢ Iic ↑q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r q : ℚ<VAR>hr_le_q : r ≤ q<VAR>x : α × ℝ<GOAL>x.1 ∈ s → x.2 ≤ ↑r → x.1 ∈ s ∧ x.2 ≤ ↑q
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<GOAL>a * (b % c) % c = a * b % c
<VAR>i j k : ℤ<VAR>H1 : k ∣ i<VAR>H2 : k ∣ j<GOAL>(i / k).gcd (j / k) = i.gcd j / k.natAbs
<VAR>i j k : ℤ<VAR>H1 : k ∣ i<VAR>H2 : k ∣ j<GOAL>(i.natAbs / k.natAbs).gcd (j.natAbs / k.natAbs) = i.gcd j / k.natAbs
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : ℝ<GOAL>Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)
<VAR>a : ℤ<VAR>b : ℕ<VAR>inst✝ : NeZero b<GOAL>0 ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯ ↔ a.gcd ↑b ≠ 1
<VAR>a : ℤ<VAR>b : ℕ<VAR>inst✝ : NeZero b<GOAL>(∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>ℱ : Presheaf C X<VAR>x : ↑X<VAR>U✝ : Opens ↑X<VAR>hxU✝ : (𝟙 X) x ∈ U✝<GOAL>((pushforward C (𝟙 X)).obj ℱ).germ ⟨(𝟙 X) x, hxU✝⟩ ≫ stalkPushforward C (𝟙 X) ℱ x = ((pushforward C (𝟙 X)).obj ℱ).germ ⟨(𝟙 X) x, hxU✝⟩ ≫ (stalkFunctor C x).map (Pushforward.id ℱ).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>ℱ : Presheaf C X<VAR>x : ↑X<VAR>U✝ : Opens ↑X<VAR>hxU✝ : (𝟙 X) x ∈ U✝<GOAL>ℱ.map ((NatTrans.op (OpenNhds.inclusionMapIso (𝟙 X) x).inv).app (op { obj := U✝, property := ⋯ })) ≫ colimit.ι ((OpenNhds.map (𝟙 X) x).op ⋙ ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ) (op { obj := U✝, property := ⋯ }) ≫ colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ) (OpenNhds.map (𝟙 X) x).op = colimit.ι ((OpenNhds.inclusion ((𝟙 X) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ) (op { obj := U✝, property := ⋯ }) ≫ (stalkFunctor C x).map (Pushforward.id ℱ).hom