ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b : Basis ι R L<VAR>x : L<GOAL>Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = charpoly (φ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>F : Type u_5<VAR>inst✝ : NormedDivisionRing F<VAR>f g : α → F<VAR>hint : Integrable g μ<VAR>hm : AEStronglyMeasurable f μ<VAR>hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C<GOAL>Integrable (fun x => f x * g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>F : Type u_5<VAR>inst✝ : NormedDivisionRing F<VAR>f g : α → F<VAR>hint : Integrable g μ<VAR>hm : AEStronglyMeasurable f μ<VAR>hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C<VAR>hα : IsEmpty α<GOAL>Integrable (fun x => f x * g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>F : Type u_5<VAR>inst✝ : NormedDivisionRing F<VAR>f g : α → F<VAR>hint : Integrable g μ<VAR>hm : AEStronglyMeasurable f μ<VAR>hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C<VAR>hα : Nonempty α<GOAL>Integrable (fun x => f x * g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>inst✝ : LE α<VAR>x : α<VAR>z : β<GOAL>z ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f g : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct g<VAR>p : (j : J) → f j ⟶ g j<VAR>j : J<GOAL>ι f j ≫ map p = p j ≫ ι g j
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f g : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct g<VAR>p : (j : J) → f j ⟶ g j<VAR>j : J<GOAL>ι f j ≫ map' p = p j ≫ ι g j
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>h : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>x + t • (y - x) ∈ interior s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>h : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>x + t • (y - x) ∈ openSegment 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>h : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Ioo 0 1
<VAR>R : Type u_1<VAR>inst✝⁶ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>x✝ y✝ z : M<VAR>inst✝ : Subsingleton M<VAR>x y : M<GOAL>SameRay R x y
<VAR>R : Type u_1<VAR>inst✝⁶ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>x✝ y✝ z : M<VAR>inst✝ : Subsingleton M<VAR>x y : M<GOAL>SameRay R 0 y
<VAR>x y : ZFSet<GOAL>y ∈ ⋂₀ {x} ↔ y ∈ x
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>m m' : (i : ι) → M₁ i<GOAL>f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>hI : I ≠ 0<GOAL>‖I‖ = 1
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<GOAL>recF g ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<GOAL>g (abs ⟨a, splitFun f' fun i => (P F).wRec (fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) = g (abs ⟨a, splitFun f' (((P F).wRec fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)) ∘ f)⟩)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>C : Type u_4<VAR>inst✝¹ : Category.{u_5, u_4} C<VAR>X Y Z : GradedObject I C<VAR>φ : X ⟶ Y<VAR>e✝ : X ≅ Y<VAR>ψ : Y ⟶ Z<VAR>p✝ : I → J<VAR>j✝ : J<VAR>e : X ≅ Y<VAR>p : I → J<VAR>inst✝ : X.HasMap p<VAR>j : J<VAR>α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j)<GOAL>HasCoproduct (Y.mapObjFun p j)
<VAR>a b : Int<GOAL>↑(a + b) = ↑a + ↑b
<VAR>a b : Int<GOAL>↑(a + b) = normalize ((↑a).num * ↑(↑b).den + (↑b).num * ↑(↑a).den) ((↑a).den * (↑b).den) ⋯
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ fixedBy α g<GOAL>s ∈ fixedBy (Set α) g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ fixedBy α g<GOAL>s ∈ fixedBy (Set α) g⁻¹
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ fixedBy α g<VAR>x : α<GOAL>x ∈ g⁻¹ • s ↔ x ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ fixedBy α g<VAR>x : α<GOAL>g • x ∈ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ fixedBy α g<VAR>x : α<VAR>gxs : g • x ∈ s<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ fixedBy α g⁻¹<VAR>x : α<VAR>gxs : g • x ∈ s<GOAL>x ∈ s
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>h : ¬gcd x y = 0<GOAL>gcd x y * (x * y / gcd x y) = x * y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>h : ¬gcd x y = 0<VAR>r : R<VAR>hr : x = gcd x y * r<VAR>s : R<VAR>hs : y = gcd x y * s<GOAL>gcd x y * (x * y / gcd x y) = x * y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>y r s g : R<VAR>h : ¬g = 0<VAR>hs : y = gcd (g * r) y * s<GOAL>g * (g * r * y / g) = g * r * y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>inst✝ : T1Space X<VAR>hs : s.Countable<GOAL>IsGδ sᶜ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>inst✝ : T1Space X<VAR>hs : s.Countable<GOAL>IsGδ (⋂ i ∈ s, {i}ᶜ)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<GOAL>o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<GOAL>o.oangle x (x + 0 • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan 0)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>C : WSeq α → WSeq β → Prop<GOAL>Function.swap (LiftRelO R C) = LiftRelO (Function.swap R) (Function.swap C)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>C : WSeq α → WSeq β → Prop<VAR>x : Option (β × WSeq β)<VAR>y : Option (α × WSeq α)<GOAL>Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hB : M.Base B<GOAL>∃ B', M.Base B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hB : M.Base B<VAR>B' : Set α<VAR>hB' : M.Basis B' (I ∪ B)<VAR>hIB' : I ⊆ B'<GOAL>∃ B', M.Base B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r : ℝ≥0∞<VAR>h : LipschitzWith K f<VAR>x y : α<GOAL>(↑K)⁻¹ * edist (f x) (f y) ≤ edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r : ℝ≥0∞<VAR>h : LipschitzWith K f<VAR>x y : α<GOAL>edist (f x) (f y) / ↑K ≤ edist x y
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>φ : K →+* ℂ<VAR>hφ : IsReal φ<VAR>x : K<GOAL>↑(hφ.embedding x) = φ x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>φ : K →+* ℂ<VAR>hφ : IsReal φ<VAR>x : K<GOAL>(↑(hφ.embedding x)).re = (φ x).re
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>φ : K →+* ℂ<VAR>hφ : IsReal φ<VAR>x : K<GOAL>(↑(hφ.embedding x)).im = (φ x).im
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : HasFPowerSeriesWithinAt f p s x<GOAL>ContinuousWithinAt f s x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>(rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData).op = leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData ≫ leftHomologyMap' (opMap φ) S₂.op.leftHomologyData S₁.op.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M✝ N✝ : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Fintype m<VAR>M N : Matrix m m R<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<GOAL>(M * N) i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M✝ N✝ : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Fintype m<VAR>M N : Matrix m m R<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<VAR>i j : m<VAR>hij : b j < b i<GOAL>∀ x ∈ univ, (fun j => M i j) x * (fun j_1 => N j_1 j) x = 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : C ⥤ Type v₁<VAR>f : coyoneda.obj (op X) ⟶ F<VAR>g : X ⟶ Y<GOAL>(f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : C ⥤ Type v₁<VAR>f : coyoneda.obj (op X) ⟶ F<VAR>g : X ⟶ Y<GOAL>((coyoneda.obj (op X)).map g ≫ f.app Y) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)
<VAR>m : ℕ<VAR>hm : m ≠ 1<GOAL>schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹
<VAR>hm : 0 ≠ 1<GOAL>schnirelmannDensity {n | n % 0 = 1} = (↑0)⁻¹
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<GOAL>schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<GOAL>↑(filter (fun x => x ∈ {n | n % m = 1}) (Ioc 0 m)).card / ↑m ≤ (↑m)⁻¹
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<GOAL>(↑m)⁻¹ ≤ schnirelmannDensity {n | n % m = 1}
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<GOAL>∀ (n : ℕ), 0 < n → (↑m)⁻¹ ≤ ↑(filter (fun x => x ∈ {n | n % m = 1}) (Ioc 0 n)).card / ↑n
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(↑m)⁻¹ ≤ ↑(filter (fun x => x ∈ {n | n % m = 1}) (Ioc 0 n)).card / ↑n
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(↑m)⁻¹ ≤ ↑(filter (fun x => x % m = 1) (Ioc 0 n)).card / ↑n
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)<GOAL>(↑m)⁻¹ ≤ ↑(filter (fun x => x % m = 1) (Ioc 0 n)).card / ↑n
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)<GOAL>↑n / ↑m ≤ ↑(filter (fun x => x % m = 1) (Ioc 0 n)).card
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)<GOAL>↑n / ↑m ≤ ↑(image (fun x => x * m + 1) (Icc 0 ((n - 1) / m))).card
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)<GOAL>n ≤ (n - 1) / m * m + m
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)<GOAL>Function.Injective fun x => x * m + 1
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>hm' : m > 0<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)<VAR>a b : ℕ<GOAL>(fun x => x * m + 1) a = (fun x => x * m + 1) b → a = b
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>F₁ = F₂
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>curry.obj F₁ = curry.obj F₂
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>W₁.Q ⋙ curry.obj F₁ = W₁.Q ⋙ curry.obj F₂
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>(W₁.Q ⋙ curry.obj F₁).flip = (W₁.Q ⋙ curry.obj F₂).flip
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>(W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₁, u₁} C₁<VAR>inst✝³ : Category.{v₂, u₂} C₂<VAR>inst✝² : Category.{v₃, u₃} D₁<VAR>inst✝¹ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝ : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E<VAR>h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂<GOAL>uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : SequentialSpace X<VAR>h₂ : SequentialSpace X<GOAL>SequentialSpace X
<VAR>R S : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f : R →+* S<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : LocalizationPreserves P<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>hf : P f<GOAL>P (IsLocalization.Away.map R' S' f r)
<VAR>R S : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f : R →+* S<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : LocalizationPreserves P<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>hf : P f<VAR>this : IsLocalization (Submonoid.map f (Submonoid.powers r)) S'<GOAL>P (IsLocalization.Away.map R' S' f r)
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>inst✝ : Unique Mˣ<VAR>a : M<VAR>l₁ : List M<VAR>b : M<VAR>l₂ : List M<VAR>h : (a :: l₁).prod = (b :: l₂).prod<VAR>hl₁ : ∀ p ∈ a :: l₁, Prime p<VAR>hl₂ : ∀ p ∈ b :: l₂, Prime p<GOAL>a :: l₁ ~ b :: l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<GOAL>BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b
<VAR>p : ℕ<VAR>pp : Fact (Nat.Prime p)<VAR>a r : ℤ<VAR>hr : IsInt (jacobiSym a p) r<GOAL>IsInt (legendreSym p a) r
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K f<VAR>hf : f 1 = 1<VAR>x : E<GOAL>‖x‖ ≤ ↑K * ‖f x‖
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>inst✝¹ : MvFunctor F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>pp : β → Prop<VAR>rr : β → β → Prop<VAR>x y : F (α ::: β)<GOAL>(∃ u, (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y) ↔ ∃ u, (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>inst✝¹ : MvFunctor F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>pp : β → Prop<VAR>rr : β → β → Prop<VAR>x y : F (α ::: β)<GOAL>MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α = TypeVec.id
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>inst✝¹ : MvFunctor F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>pp : β → Prop<VAR>rr : β → β → Prop<VAR>x y : F (α ::: β)<GOAL>∀ (u : F fun i => { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }), (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y ↔ (fun i t => (↑t).1) <$$> MvFunctor.f' rr n α <$$> u = x ∧ (fun i t => (↑t).2) <$$> MvFunctor.f' rr n α <$$> u = y
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A B : Matrix m m R<VAR>hA : A.PosDef<VAR>hB : B.PosSemidef<VAR>x : m → R<VAR>hx : x ≠ 0<GOAL>0 < star x ⬝ᵥ (A + B) *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A B : Matrix m m R<VAR>hA : A.PosDef<VAR>hB : B.PosSemidef<VAR>x : m → R<VAR>hx : x ≠ 0<GOAL>0 < star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑(μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ