ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this✝ : UniformAddGroup E<VAR>this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i<VAR>V : Set E<VAR>hV : Disjoint (⋃ x ∈ s, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V)) (⋃ x ∈ t, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))<VAR>hV0 : 0 ∈ V<VAR>hVopen : IsOpen V<VAR>hVconvex : Convex 𝕜 V<GOAL>Disjoint (⋃ a ∈ s, (fun x => -a + x) ⁻¹' V) (⋃ a ∈ t, (fun x => -a + x) ⁻¹' V)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this✝ : UniformAddGroup E<VAR>this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i<VAR>V : Set E<VAR>hV0 : 0 ∈ V<VAR>hVopen : IsOpen V<VAR>hVconvex : Convex 𝕜 V<VAR>hV : Disjoint (⋃ x ∈ s, (fun x => -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V) (⋃ x ∈ t, (fun x => -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)<GOAL>Disjoint (⋃ a ∈ s, (fun x => -a + x) ⁻¹' V) (⋃ a ∈ t, (fun x => -a + x) ⁻¹' V)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<GOAL>orthogonalProjectionFn K u = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<GOAL>⟪orthogonalProjectionFn K u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<VAR>hvs : orthogonalProjectionFn K u - v ∈ K<GOAL>⟪orthogonalProjectionFn K u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<VAR>hvs : orthogonalProjectionFn K u - v ∈ K<VAR>huo : ⟪u - orthogonalProjectionFn K u, orthogonalProjectionFn K u - v⟫_𝕜 = 0<GOAL>⟪orthogonalProjectionFn K u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<VAR>hvs : orthogonalProjectionFn K u - v ∈ K<VAR>huo : ⟪u - orthogonalProjectionFn K u, orthogonalProjectionFn K u - v⟫_𝕜 = 0<VAR>huv : ⟪u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0<GOAL>⟪orthogonalProjectionFn K u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<VAR>hvs : orthogonalProjectionFn K u - v ∈ K<VAR>huo : ⟪u - orthogonalProjectionFn K u, orthogonalProjectionFn K u - v⟫_𝕜 = 0<VAR>huv : ⟪u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0<VAR>houv : ⟪u - v - (u - orthogonalProjectionFn K u), orthogonalProjectionFn K u - v⟫_𝕜 = 0<GOAL>⟪orthogonalProjectionFn K u - v, orthogonalProjectionFn K u - v⟫_𝕜 = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>X : Type u_4<VAR>inst✝¹² : Monoid M<VAR>S : Submonoid M<VAR>inst✝¹¹ : OreSet S<VAR>inst✝¹⁰ : MulAction M X<VAR>inst✝⁹ : SMul R X<VAR>inst✝⁸ : SMul R M<VAR>inst✝⁷ : IsScalarTower R M M<VAR>inst✝⁶ : IsScalarTower R M X<VAR>inst✝⁵ : SMul R' X<VAR>inst✝⁴ : SMul R' M<VAR>inst✝³ : IsScalarTower R' M M<VAR>inst✝² : IsScalarTower R' M X<VAR>inst✝¹ : SMul R R'<VAR>inst✝ : IsScalarTower R R' M<VAR>r : M<VAR>x : OreLocalization S X<GOAL>(r /ₒ 1) • x = r • x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>X : Type u_4<VAR>inst✝¹² : Monoid M<VAR>S : Submonoid M<VAR>inst✝¹¹ : OreSet S<VAR>inst✝¹⁰ : MulAction M X<VAR>inst✝⁹ : SMul R X<VAR>inst✝⁸ : SMul R M<VAR>inst✝⁷ : IsScalarTower R M M<VAR>inst✝⁶ : IsScalarTower R M X<VAR>inst✝⁵ : SMul R' X<VAR>inst✝⁴ : SMul R' M<VAR>inst✝³ : IsScalarTower R' M M<VAR>inst✝² : IsScalarTower R' M X<VAR>inst✝¹ : SMul R R'<VAR>inst✝ : IsScalarTower R R' M<VAR>r : M<VAR>r' : X<VAR>s : ↥S<GOAL>(r /ₒ 1) • (r' /ₒ s) = r • (r' /ₒ s)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>F.εIso.inv.app ((F.obj n).obj X) = (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>𝟙 ((F.obj (𝟙_ M)).obj ((F.obj n).obj X)) = ((F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X) ≫ F.ε.app ((F.obj n).obj X)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<VAR>a b : ℝ<VAR>hab : a < b<GOAL>(interior (Ico a b)).Nonempty
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<VAR>a b : ℝ<VAR>hab : ¬a < b<GOAL>UniqueDiffOn ℝ (Ico a b)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ span R s<VAR>x : A<VAR>hx : x ∈ t<GOAL>0 • x ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ span R s<VAR>x : A<VAR>hx : x ∈ t<GOAL>0 ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ span R s<VAR>x : A<VAR>hx : x ∈ t<VAR>c₁ c₂ : S<VAR>ih₁ : c₁ • x ∈ span R (s • t)<VAR>ih₂ : c₂ • x ∈ span R (s • t)<GOAL>(c₁ + c₂) • x ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ span R s<VAR>x : A<VAR>hx : x ∈ t<VAR>c₁ c₂ : S<VAR>ih₁ : c₁ • x ∈ span R (s • t)<VAR>ih₂ : c₂ • x ∈ span R (s • t)<GOAL>c₁ • x + c₂ • x ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ span R s<VAR>x : A<VAR>hx : x ∈ t<VAR>b : R<VAR>c : S<VAR>hc : c • x ∈ span R (s • t)<GOAL>(b • c) • x ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ span R s<VAR>x : A<VAR>hx : x ∈ t<VAR>b : R<VAR>c : S<VAR>hc : c • x ∈ span R (s • t)<GOAL>b • c • x ∈ span R (s • t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>‖x⋆‖ * ‖x‖ ≤ ‖x‖ * ‖x‖
<VAR>A : Type u_1<VAR>inst✝³ : NormedCommRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>I : Ideal A<VAR>inst✝ : I.IsMaximal<VAR>a : A<VAR>ha : ¬IsUnit a<GOAL>∃ f, f a = 0
<VAR>A : Type u_1<VAR>inst✝³ : NormedCommRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>I : Ideal A<VAR>inst✝ : I.IsMaximal<VAR>a : A<VAR>ha : ¬IsUnit a<VAR>M : Ideal A<VAR>hM : M.IsMaximal<VAR>haM : span {a} ≤ M<GOAL>∃ f, f a = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>(inv f).unop = inv f.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>f.unop ≫ (inv f).unop = 𝟙 (unop Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β → σ<VAR>h : α → γ → σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<VAR>hh : Computable₂ h<VAR>a : α<GOAL>(bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2) else Option.map (g a) (decode (encode (f a)).div2)) = Option.some (Sum.casesOn (f a) (g a) (h a))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>fract (a + b) ≤ fract a + fract b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>ℝ≥0∞ ≃o ↑(Iic 1)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y : ℝ≥0∞<VAR>hxy : x < y<GOAL>(fun x => ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) x < (fun x => ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) y
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ↑(Iic 1)<GOAL>↑((fun x => ⟨(x⁻¹ + 1)⁻¹, ⋯⟩) ((fun x => ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<GOAL>f =O[𝓝 b] g ↔ (f ∘ ↑e) =O[𝓝 (↑e.symm b)] (g ∘ ↑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<GOAL>(∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>h : (condCount s) t = 1<GOAL>s ⊆ t
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>h : (condCount s) t = 1<VAR>hsf : s.Finite<GOAL>s ⊆ t
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>h : Measure.count (s ∩ t) * (Measure.count s)⁻¹ = 1<VAR>hsf : s.Finite<GOAL>s ⊆ t
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hsf : s.Finite<VAR>h : Measure.count (s ∩ t) = (Measure.count s)⁻¹⁻¹<GOAL>s ⊆ t
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hsf : s.Finite<VAR>h : ⋯.toFinset.card = hsf.toFinset.card<GOAL>s ⊆ t
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hsf : s.Finite<VAR>h : ⋯.toFinset.card = hsf.toFinset.card<GOAL>s ∩ t = s
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hsf : s.Finite<VAR>h : ⋯.toFinset.card = hsf.toFinset.card<GOAL>⋯.toFinset = hsf.toFinset
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<VAR>r : ℝ<GOAL>‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<VAR>r : ℝ<GOAL>(∃ x_1 ∈ {m | (mk' S) m = x}, ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) = μ s * ν t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) ≤ μ s * ν t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<GOAL>μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>(∀ ⦃i : ι⦄, i ∈ Set.univ → ∀ ⦃j : ι⦄, j ∈ Set.univ → 0 ≤ (f j - f i) • (g j - g i)) ↔ ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)
<VAR>p✝ p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<VAR>hlt : padicNorm p r < padicNorm p q<GOAL>padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
<VAR>p✝ p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<VAR>hlt : padicNorm p r < padicNorm p q<VAR>this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)<GOAL>padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
<VAR>p✝ p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<VAR>hlt : padicNorm p r < padicNorm p q<VAR>this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)<VAR>hnge : padicNorm p r ≤ padicNorm p (q + r)<GOAL>padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
<VAR>p✝ p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<VAR>hlt : padicNorm p r < padicNorm p q<VAR>this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)<VAR>hnge : padicNorm p r ≤ padicNorm p (q + r)<VAR>this : padicNorm p q ≤ padicNorm p (q + r)<GOAL>padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
<VAR>p✝ p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<VAR>hlt : padicNorm p r < padicNorm p q<VAR>this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)<VAR>hnge : padicNorm p r ≤ padicNorm p (q + r)<VAR>this : padicNorm p q ≤ padicNorm p (q + r)<GOAL>padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>p✝ p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<VAR>hlt : padicNorm p r < padicNorm p q<VAR>this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)<VAR>hnge : padicNorm p r ≤ padicNorm p (q + r)<VAR>this : padicNorm p q ≤ padicNorm p (q + r)<GOAL>max (padicNorm p q) (padicNorm p r) ≤ padicNorm p (q + r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : PartialOrder α<VAR>x y : α<GOAL>x ≤ y → y = x ↔ ¬x < y
<GOAL>π / 4 ∈ Ioo (-(π / 2)) (π / 2)
<VAR>m n : ℤ<GOAL>(m * n).bodd = (m.bodd && n.bodd)
<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>p q r : R[X]<VAR>x : R<VAR>n : ℕ<GOAL>eval x ↑n = ↑n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>hd : d ∈ χ.conductorSet<GOAL>χ.conductor ≤ (Classical.choose ⋯).conductor
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>hd : d ∈ χ.conductorSet<GOAL>χ = (changeLevel ⋯) ⋯.choose
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>hd : d ∈ χ.conductorSet<GOAL>χ = (changeLevel ⋯) (Classical.choose ⋯)
<VAR>x y : ℝ<VAR>h : tan x = y<VAR>hx : x ∈ Ioo (-(π / 2)) (π / 2)<GOAL>tan (arctan y) = tan x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : a - c < b<GOAL>a < b + c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : a - c < b<GOAL>a - c ≤ b ∧ a ≠ b + c
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>ι' : Type u_6<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>b : Basis ι R M<VAR>v : ι' → M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).det v = b.det (v ∘ ⇑e)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x : α<VAR>k : ℕ<GOAL>(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : α → PMF β<VAR>g : β → PMF γ<VAR>p : PMF α<VAR>q : PMF β<VAR>f : α → β → PMF γ<VAR>b : γ<GOAL>(p.bind fun a => q.bind (f a)) b = (q.bind fun b => p.bind fun a => f a b) b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : n ≠ 0<GOAL>Injective fun a => a ^ n
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : P n<GOAL>find P ≤ ↑n
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : P n<GOAL>∃ (h : (find P).Dom), (find P).get h ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>g : β → γ<VAR>b : β<VAR>s : Set β<VAR>inst✝ : Decidable (b ∈ s)<VAR>hb : b ∈ s<GOAL>(fun x => b) ⁻¹' s = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>g : β → γ<VAR>b : β<VAR>s : Set β<VAR>inst✝ : Decidable (b ∈ s)<VAR>hb : b ∉ s<GOAL>(fun x => b) ⁻¹' s = ∅
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>x : R<VAR>this : TopologicalSpace R := I.adicTopology<GOAL>(𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>x : R<VAR>this✝ : TopologicalSpace R := I.adicTopology<VAR>this : (Filter.map (fun y => x + y) (𝓝 0)).HasBasis (fun _n => True) fun i => (fun y => x + y) '' ↑(I ^ i)<GOAL>(𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a / 2 < a - b<GOAL>b ≤ a / 2
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a / 2 < a - b<GOAL>b * 2 ≤ a
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a + b * 2 < a + a<GOAL>b * 2 ≤ a
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvt : Set.InjOn v ↑t<VAR>hs : s.Nonempty<VAR>hst : s ⊆ t<GOAL>∑ i ∈ s, (interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i = (interpolate t v) r
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvt : Set.InjOn v ↑t<VAR>hs : s.Nonempty<VAR>hst : s ⊆ t<GOAL>(s.sup fun b => ((interpolate (insert b (t \ s)) v) r * Lagrange.basis s v b).degree) < ↑t.card
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i✝ j : ι<VAR>v r r' : ι → F<VAR>hvt : Set.InjOn v ↑t<VAR>hs : s.Nonempty<VAR>hst : s ⊆ t<VAR>i : ι<VAR>hi : i ∈ t<GOAL>eval (v i) (∑ i ∈ s, (interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i) = r i
<VAR>a✝ b✝ c p q a b : ℚ<VAR>na : ℤ<VAR>da : ℕ<VAR>ha : da ≠ 0<VAR>hared : na.natAbs.Coprime da<VAR>nb : ℤ<VAR>db : ℕ<VAR>hb : db ≠ 0<VAR>hbred : nb.natAbs.Coprime db<GOAL>(if (decide ({ num := nb, den := db, den_nz := hb, reduced := hbred }.num < 0) && decide (0 ≤ { num := na, den := da, den_nz := ha, reduced := hared }.num)) = true then true else if { num := nb, den := db, den_nz := hb, reduced := hbred }.num = 0 then decide (0 < { num := na, den := da, den_nz := ha, reduced := hared }.num) else if (decide (0 < { num := nb, den := db, den_nz := hb, reduced := hbred }.num) && decide ({ num := na, den := da, den_nz := ha, reduced := hared }.num ≤ 0)) = true then false else decide ({ num := nb, den := db, den_nz := hb, reduced := hbred }.num * ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den < { num := na, den := da, den_nz := ha, reduced := hared }.num * ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den)) = false ↔ 0 ≤ { num := nb, den := db, den_nz := hb, reduced := hbred } - { num := na, den := da, den_nz := ha, reduced := hared }
<VAR>a✝ b✝ c p q a b : ℚ<VAR>na : ℤ<VAR>da : ℕ<VAR>ha : da ≠ 0<VAR>hared : na.natAbs.Coprime da<VAR>nb : ℤ<VAR>db : ℕ<VAR>hb : db ≠ 0<VAR>hbred : nb.natAbs.Coprime db<GOAL>(if nb < 0 ∧ 0 ≤ na then False else if nb = 0 then na ≤ 0 else (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da) ↔ 0 ≤ ({ num := nb, den := db, den_nz := hb, reduced := hbred } - { num := na, den := da, den_nz := ha, reduced := hared }).num
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<VAR>h : a ^ 2 < b ^ 2<VAR>hb : 0 ≤ b<GOAL>|a| < b