ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : Algebra S B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S B<VAR>x : R<GOAL>(algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝³ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ₁ φ₂ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>inst✝² : Category.{u_5, u_3} E<VAR>L₁ : C ⥤ D<VAR>L₂ : C ⥤ E<VAR>inst✝¹ : L₁.IsLocalization W<VAR>inst✝ : L₂.IsLocalization W<VAR>h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯<GOAL>φ₁.map L₂ ⋯ = φ₂.map L₂ ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝³ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ₁ φ₂ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>inst✝² : Category.{u_5, u_3} E<VAR>L₁ : C ⥤ D<VAR>L₂ : C ⥤ E<VAR>inst✝¹ : L₁.IsLocalization W<VAR>inst✝ : L₂.IsLocalization W<VAR>h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯<GOAL>(Localization.uniq L₂ L₁ W).functor.map (φ₁.map L₂ ⋯) = (Localization.uniq L₂ L₁ W).functor.map (φ₂.map L₂ ⋯)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>x : L<GOAL>x ∈ idealizer I ↔ x ∈ normalizer I
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x y : AddCircle T<VAR>hxy : x ≠ y<GOAL>∃ f ∈ (fun f => ⇑f) '' ↑fourierSubalgebra.toSubalgebra, f x ≠ f y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x y : AddCircle T<VAR>hxy : x ≠ y<GOAL>(fun f => ⇑f) (fourier 1) x ≠ (fun f => ⇑f) (fourier 1) y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x y : AddCircle T<VAR>hxy : x ≠ y<GOAL>(fourier 1) x ≠ (fourier 1) y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x y : AddCircle T<VAR>hxy : x ≠ y<GOAL>↑x.toCircle ≠ ↑y.toCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x y : AddCircle T<VAR>hxy : ↑x.toCircle = ↑y.toCircle<GOAL>x = y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x y : AddCircle T<VAR>hxy : x.toCircle = y.toCircle<GOAL>x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>a b : ℝ<VAR>e : X → Y<VAR>hf : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>he : ClosedEmbedding e<GOAL>∃ g, (∀ (y : Y), g y ∈ Icc a b) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>a b : ℝ<VAR>e : X → Y<VAR>hf : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>he : ClosedEmbedding e<VAR>g : Y →ᵇ ℝ<VAR>hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖<VAR>hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))<GOAL>∃ g, (∀ (y : Y), g y ∈ Icc a b) ∧ ⇑g ∘ e = ⇑f
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<GOAL>ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<GOAL>LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x → ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<VAR>h₁ : LowerSemicontinuousWithinAt f s x<VAR>h₂ : UpperSemicontinuousWithinAt f s x<VAR>v : Set γ<VAR>hv : v ∈ 𝓝 (f x)<GOAL>v ∈ map f (𝓝[s] x)
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<VAR>h₁ : LowerSemicontinuousWithinAt f s x<VAR>h₂ : UpperSemicontinuousWithinAt f s x<VAR>v : Set γ<VAR>hv : v ∈ 𝓝 (f x)<GOAL>f ⁻¹' v ∈ 𝓝[s] x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>n : PosNum<GOAL>1 ≤ ↑n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>n : PosNum<GOAL>1 ≤ ↑↑n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>n : PosNum<GOAL>↑1 ≤ ↑↑n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝¹ : Group G<VAR>inst✝ : MulOneClass M<VAR>f : M → G<VAR>map_mul : ∀ (a b : M), f (a * b) = f a * f b<GOAL>f 1 = 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.degree = Q.degree<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.degree = Q.degree<GOAL>Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.degree = Q.degree<GOAL>Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑Q.natDegree - ↑Q.natDegree)) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y : E<VAR>hs : s.Nonempty<GOAL>(convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} ((convexHull 𝕜) s)
<VAR>x y : ℝ<GOAL>mk 1 = 1
<VAR>x y : ℝ<GOAL>mk 1 = { cauchy := 1 }
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K V<VAR>Φ : Subspace K (Module.Dual K V)<GOAL>finrank K ↥(dualCoannihilator Φ) = finrank K ↥(dualAnnihilator Φ)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K V<VAR>Φ : Subspace K (Module.Dual K V)<GOAL>finrank K ↥(comap (↑(Module.evalEquiv K V)) (dualAnnihilator Φ)) = finrank K ↥(dualAnnihilator Φ)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.inv.map (F.map f) = (F.asEquivalence.functor ⋙ F.asEquivalence.inverse).map f
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>a₀ a₁ b₀ b₁ : α<GOAL>![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<GOAL>∫ (x : ℝ) in a..b, f x - g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..b, g x ∂μ
<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>inst✝ : Finite ι<VAR>s : Set ((a : ι) → π a)<GOAL>IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s
<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>inst✝ : Finite ι<VAR>s : Set ((a : ι) → π a)<VAR>val✝ : Fintype ι<GOAL>IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s
<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>inst✝ : Finite ι<VAR>s : Set ((a : ι) → π a)<VAR>val✝ : Fintype ι<GOAL>(∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s
<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>inst✝ : Finite ι<VAR>s : Set ((a : ι) → π a)<VAR>val✝ : Fintype ι<GOAL>(∀ x ∈ s, ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ x i ∈ t_1) ∧ (↑I).pi t ⊆ s) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s
<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>inst✝ : Finite ι<VAR>s : Set ((a : ι) → π a)<VAR>val✝ : Fintype ι<VAR>a : (a : ι) → π a<VAR>x✝ : a ∈ s<GOAL>(∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) → ∃ u, (∀ (a_2 : ι), IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ univ.pi u ⊆ s
<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>inst✝ : Finite ι<VAR>s : Set ((a : ι) → π a)<VAR>val✝ : Fintype ι<VAR>a : (a : ι) → π a<VAR>x✝ : a ∈ s<GOAL>(∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) → ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : n → R<GOAL>(Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<VAR>p : s₁.entries ~ s₂.entries<GOAL>(insert a b s₁).entries ~ (insert a b s₂).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<VAR>p : s₁.entries ~ s₂.entries<GOAL>⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries
<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>g : α → E'''<VAR>h : f =O[l] g<GOAL>∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g 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>g : α → E'''<VAR>h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖<GOAL>f =O[l] g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<GOAL>∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<GOAL>∀ (i : Finset ι), ∑ a ∈ i, μ (As a) ≤ μ (⋃ i, As i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>s : Finset ι<GOAL>∑ a ∈ s, μ (As a) ≤ μ (⋃ i, As i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>s : Finset ι<GOAL>μ (⋃ b ∈ s, As b) ≤ μ (⋃ i, As i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>s : Finset ι<VAR>i✝ : ι<GOAL>⋃ (_ : i✝ ∈ s), As i✝ ⊆ As i✝
<VAR>x : ℝ<GOAL>rexp x = NormedSpace.exp ℝ x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>convexBodySumFactor K ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>2 ^ NrRealPlaces K * (NNReal.pi / 2) ^ NrComplexPlaces K ≠ 0
<VAR>a✝ b : Cardinal.{u}<VAR>n m : ℕ<VAR>a : Cardinal.{u_1}<VAR>h : ¬ℵ₀ ≤ a<GOAL>IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
<VAR>a✝ b : Cardinal.{u}<VAR>n m : ℕ<VAR>a : Cardinal.{u_1}<VAR>h : ¬ℵ₀ ≤ a<GOAL>IsPrimePow a ↔ ∃ n, a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<GOAL>IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<GOAL>(∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<GOAL>(∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) → ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<VAR>p : Cardinal.{u_1}<VAR>k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<VAR>hpk : p ^ k = ↑a<GOAL>∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<VAR>p : Cardinal.{u_1}<VAR>k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<VAR>hpk : p ^ k = ↑a<VAR>key : p ^ 1 ≤ ↑a<GOAL>∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<VAR>p : Cardinal.{u_1}<VAR>k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<VAR>hpk : p ^ k = ↑a<VAR>key : p ≤ ↑a<GOAL>∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ¬ℵ₀ ≤ ↑a<VAR>k : ℕ<VAR>hk : 0 < k<VAR>p : ℕ<VAR>hp : Prime ↑p<VAR>hpk : ↑p ^ k = ↑a<VAR>key : ↑p ≤ ↑a<GOAL>∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<GOAL>⊥ < affineSpan k s ↔ s.Nonempty
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<GOAL>affineSpan k s ≠ ⊥ ↔ s ≠ ∅
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>h : DifferentiableAt 𝕜 f x<GOAL>HasGradientAt f (∇ f x) x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>h : DifferentiableAt 𝕜 f x<GOAL>HasFDerivAt f (fderiv 𝕜 f x) x
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>g : R[X]<GOAL>(pb.quotientEquivQuotientMinpolyMap I) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)) = (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<GOAL>#↑Set.univ = 𝔠
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X X' Y Y' Z Z' : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : X ⟶ Z ⊗ Y'<VAR>g : X' ⟶ Z'<GOAL>(tensorRightHomEquiv (X' ⊗ X) Y Y' (Z' ⊗ Z)).symm ((g ⊗ f) ≫ (α_ Z' Z Y').inv) = (α_ X' X Y).hom ≫ (g ⊗ (tensorRightHomEquiv X Y Y' Z).symm f)
<VAR>m n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.succ<VAR>i : Fin n✝<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>b : Fin n → α<GOAL>Set.range (cons x b) = insert x (Set.range b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Filter β<GOAL>(⨅ i, f i).prod g = ⨅ i, (f i).prod g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Filter β<GOAL>⨅ x, comap Prod.fst (f x) ⊓ comap Prod.snd g = ⨅ i, (f i).prod g
<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>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Inducing g<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
<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>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Inducing g<VAR>s : Set α<VAR>x : α<GOAL>Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>h : Function.Commute f g<VAR>hco : (minimalPeriod f x).Coprime (minimalPeriod g x)<GOAL>minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>h : Function.Commute f g<VAR>hco : (minimalPeriod f x).Coprime (minimalPeriod g x)<GOAL>minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>h : Function.Commute f g<VAR>hco : (minimalPeriod f x).Coprime (minimalPeriod g x)<GOAL>∀ {f g : α → α}, Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g✝ : α → α<VAR>h✝ : Function.Commute f✝ g✝<VAR>hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hco : (minimalPeriod f x).Coprime (minimalPeriod g x)<GOAL>minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g✝ : α → α<VAR>h✝ : Function.Commute f✝ g✝<VAR>hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hco : (minimalPeriod f x).Coprime (minimalPeriod g x)<GOAL>IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g✝ : α → α<VAR>h✝ : Function.Commute f✝ g✝<VAR>hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hco : (minimalPeriod f x).Coprime (minimalPeriod g x)<GOAL>IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>(frontier s)ᶜ = interior s ∪ interior sᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ