ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (⇑(measurableEquivIoc T t).symm) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ((measurableEquivIoc T t).symm a)<GOAL>∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a<GOAL>∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a<GOAL>∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a<GOAL>∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a<GOAL>∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T))) = ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.Finite<GOAL>↑s.ncard = s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>G.IsNClique 0 s ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>s = ∅ → G.IsClique ↑s
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>AddMonoidAlgebra.single 0 a * AddMonoidAlgebra.single s a' = AddMonoidAlgebra.single s (a * a')
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p : R[X]<VAR>x : R<GOAL>(X - C x).Monic
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type v<VAR>f : α → β<VAR>x : Comp F G α<GOAL>(Seq.seq (pure f) fun x_1 => x).run = (f <$> x).run
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : 0 ∉ t<GOAL>↑(f.restrict s) ⁻¹' t = s ∩ ↑f ⁻¹' t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>V W : C<VAR>i : V ⟶ unop U<VAR>hi : (fun V f => F.map f.op s ∈ G.obj (op V)) V i<VAR>j : W ⟶ V<GOAL>(fun V f => F.map f.op s ∈ G.obj (op V)) W (j ≫ i)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>V W : C<VAR>i : V ⟶ unop U<VAR>hi : (fun V f => F.map f.op s ∈ G.obj (op V)) V i<VAR>j : W ⟶ V<GOAL>F.map j.op (F.map i.op s) ∈ G.obj (op W)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>x : α<VAR>H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>hs : s ⊆ u ∪ v<VAR>z : α<VAR>zs : z ∈ s<VAR>zu : z ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<VAR>xs : x ∈ s<GOAL>(s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c a : M<VAR>h : IsUnit a<VAR>y : M<GOAL>(fun x => x * a) (y * ↑h.unit⁻¹) = y
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<GOAL>(EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter = (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<VAR>h_faces : ↑((EuclideanGeometry.orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)<GOAL>(EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter = (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<VAR>h_faces : ↑((EuclideanGeometry.orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)<GOAL>∑ i : Fin (n + 1), (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n + centroidWeightsWithCircumcenter {i₁, i₂} - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) (pointIndex i) • (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) + (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n + centroidWeightsWithCircumcenter {i₁, i₂} - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) circumcenterIndex • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<VAR>h_faces : ↑((EuclideanGeometry.orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)<GOAL>∑ x : Fin (n + 1), ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) - if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<VAR>h_faces : ↑((EuclideanGeometry.orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)<GOAL>∑ x : Fin (n + 1), ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else ∑ _x ∈ ?m.329271, 0) - if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else ∑ _x ∈ ?m.329271, 0) = ∑ _x ∈ ?m.329271, 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<VAR>h_faces : ↑((EuclideanGeometry.orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)<GOAL>Type ?u.329268
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<VAR>hc : {i₁, i₂}.card = 2<VAR>W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})<VAR>h_faces : ↑((EuclideanGeometry.orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)<GOAL>Finset ?m.329269
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>a b : R<VAR>hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl<VAR>p : ↥(unop (op V))<GOAL>↑((comap f U V hUV) (const R a b U hb)) p = ↑(const S (f a) (f b) V ⋯) p
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>a b : R<VAR>hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl<VAR>p : ↥(unop (op V))<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap f) ↑p).asIdeal (↑p).asIdeal f ⋯) (IsLocalization.mk' (Localizations R ↑⟨(PrimeSpectrum.comap f) ↑p, ⋯⟩) a ⟨b, ⋯⟩) = IsLocalization.mk' (Localizations S ↑p) (f a) ⟨f b, ⋯⟩
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>a b : R<VAR>hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl<VAR>p : ↥(unop (op V))<GOAL>IsLocalization.mk' (Localization.AtPrime (↑p).asIdeal) (f a) ⟨f ↑⟨b, ⋯⟩, ⋯⟩ = IsLocalization.mk' (Localizations S ↑p) (f a) ⟨f b, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : SetLike S R<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid ι<VAR>A : ι → S<VAR>inst✝ : GradedMonoid A<VAR>n : ℕ<VAR>i : Fin n → ι<VAR>r : Fin n → R<VAR>h : ∀ (j : Fin n), r j ∈ A (i j)<GOAL>(List.ofFn r).prod ∈ A (List.ofFn i).sum
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : SetLike S R<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid ι<VAR>A : ι → S<VAR>inst✝ : GradedMonoid A<VAR>n : ℕ<VAR>i : Fin n → ι<VAR>r : Fin n → R<VAR>h : ∀ (j : Fin n), r j ∈ A (i j)<GOAL>(List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum
<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>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>F' : Type u_3 := UniformSpace.Completion F<VAR>e : F →L[𝕜] F' := UniformSpace.Completion.toComplL<GOAL>EqOn f 0 U
<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>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>F' : Type u_3 := UniformSpace.Completion F<VAR>e : F →L[𝕜] F' := UniformSpace.Completion.toComplL<VAR>this : AnalyticOn 𝕜 (⇑e ∘ f) U<GOAL>EqOn f 0 U
<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>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>F' : Type u_3 := UniformSpace.Completion F<VAR>e : F →L[𝕜] F' := UniformSpace.Completion.toComplL<VAR>this : AnalyticOn 𝕜 (⇑e ∘ f) U<VAR>A : EqOn (⇑e ∘ f) 0 U<GOAL>EqOn f 0 U
<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>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>F' : Type u_3 := UniformSpace.Completion F<VAR>e : F →L[𝕜] F' := UniformSpace.Completion.toComplL<VAR>this✝ : AnalyticOn 𝕜 (⇑e ∘ f) U<VAR>A : EqOn (⇑e ∘ f) 0 U<VAR>z : E<VAR>hz : z ∈ U<VAR>this : e (f z) = e 0<GOAL>f z = 0 z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p : α → Prop<VAR>f✝ : (a : α) → p a → β<VAR>x✝ : Option α<VAR>f : α → Option β<VAR>x : Option α<GOAL>(x.pbind fun a x => f a) = x.bind f
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>x y : Fin (n + 1)<VAR>h : x ≠ y<GOAL>∃ z, y.succAbove z = x
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>x y : Fin (n + 1)<VAR>h : x ≠ y<VAR>hxy : x < y<GOAL>∃ z, y.succAbove z = x
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>x y : Fin (n + 1)<VAR>h : x ≠ y<VAR>hyx : y < x<GOAL>∃ z, y.succAbove z = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s✝ : Set α<VAR>a✝ : α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<GOAL>(dirac a) s = s.indicator 1 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s✝ : Set α<VAR>a✝ : α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<GOAL>(dirac a) s ≤ 0
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>a✝ : ℕ<GOAL>a✝ ∈ filter (fun x => x ∣ n) (range n) ↔ a✝ ∈ n.properDivisors
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>a✝ : ℕ<GOAL>a✝ ∣ n → a✝ < n → 1 ≤ a✝
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α → α<VAR>h : Commute f g<VAR>n✝ : ℕ<VAR>x : α<VAR>hx : f x = g x<VAR>n : ℕ<VAR>ihn : f^[n] x = g^[n] x<GOAL>f^[n.succ] x = g^[n.succ] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>hs : MeasurableSet s<GOAL>((κ ⊗ₖ η) a) s = 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>hs : MeasurableSet s<GOAL>(fun b => (η (a, b)) {c | (b, c) ∈ s}) =ᶠ[ae (κ a)] 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => (η (a, b)) {c | (b, c) ∈ s}
<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>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<GOAL>map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α✝<VAR>inst✝² : Fintype β<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>(∃! a, p a) ↔ (filter p univ).card = 1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α✝<VAR>inst✝² : Fintype β<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>(∃! a, p a) ↔ ∃ a, filter p univ = {a}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α✝<VAR>inst✝² : Fintype β<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x : α<GOAL>((fun a => p a) x ∧ ∀ (y : α), (fun a => p a) y → y = x) ↔ filter p univ = {x}
<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>f : α → E<VAR>hf : Memℒp f p μ<VAR>q : ℝ≥0∞<GOAL>Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
<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>f : α → E<VAR>hf : Memℒp f p μ<VAR>q : ℝ≥0∞<GOAL>eLpNorm (fun x => ‖f x‖ ^ q.toReal) (p / q) μ < ⊤
<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>f : α → E<VAR>hf : Memℒp f p μ<VAR>q : ℝ≥0∞<VAR>q_top : ¬q = ⊤<VAR>q_zero : ¬q = 0<GOAL>eLpNorm (fun x => ‖f x‖ ^ q.toReal) (p / q) μ < ⊤
<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>f : α → E<VAR>hf : Memℒp f p μ<VAR>q : ℝ≥0∞<VAR>q_top : ¬q = ⊤<VAR>q_zero : ¬q = 0<GOAL>eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ⊤
<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>f : α → E<VAR>hf : Memℒp f p μ<VAR>q : ℝ≥0∞<VAR>q_top : ¬q = ⊤<VAR>q_zero : ¬q = 0<GOAL>eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ⊤
<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>f : α → E<VAR>hf : Memℒp f p μ<VAR>q : ℝ≥0∞<VAR>q_top : ¬q = ⊤<VAR>q_zero : ¬q = 0<GOAL>eLpNorm f p μ ≠ ⊤
<VAR>J K : Type v<VAR>inst✝⁶ : SmallCategory J<VAR>inst✝⁵ : SmallCategory K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝³ : HasColimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimitsOfShape (J × K) C<VAR>inst✝ : HasColimitsOfShape (K × J) C<VAR>k : K<VAR>j : J<GOAL>colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (((colimitUncurryIsoColimitCompColim F).inv ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫ (HasColimit.isoOfNatIso (uncurryObjFlip F)).inv) ≫ (colimitUncurryIsoColimitCompColim F.flip).hom = colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k
<VAR>J K : Type v<VAR>inst✝⁶ : SmallCategory J<VAR>inst✝⁵ : SmallCategory K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝³ : HasColimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimitsOfShape (J × K) C<VAR>inst✝ : HasColimitsOfShape (K × J) C<VAR>k : K<VAR>j : J<GOAL>(((colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv) ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫ (HasColimit.isoOfNatIso (uncurryObjFlip F)).inv) ≫ (colimitUncurryIsoColimitCompColim F.flip).hom = colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f✝ : α → β<VAR>s✝ s' : Set α<VAR>x : α<VAR>p✝ : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>s : Set α<GOAL>TendstoUniformlyOn F f p s ↔ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>variance X ℙ = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), ((fun x => ∫ (x : Ω), X x) ^ 2) a) - ∫ (a : Ω), (2 * X * fun x => ∫ (x : Ω), X x) a = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>Integrable (X ^ 2) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>Integrable ((fun x => ∫ (x : Ω), X x) ^ 2) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>Integrable (X ^ 2 + (fun x => ∫ (x : Ω), X x) ^ 2) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>Integrable (2 * X * fun x => ∫ (x : Ω), X x) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<GOAL>(∫ (a : Ω), X a ^ 2) + (∫ (x : Ω), X x) ^ 2 - (2 * ∫ (x : Ω), X x) * ∫ (x : Ω), X x = (∫ (a : Ω), X a ^ 2) - (∫ (x : Ω), X x) ^ 2
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>p✝ : α✝ → Prop<VAR>f✝ : (a : α✝) → p✝ a → β✝<VAR>x✝ : Option α✝<VAR>α β γ : Type u_5<VAR>x : Option α<VAR>g : α → Option β<VAR>p : β → Prop<VAR>f : (b : β) → p b → γ<VAR>H : ∀ (a : β), a ∈ x >>= g → p a<VAR>H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g<GOAL>pmap f (x >>= g) H = do let a ← x pmap f (g a) ⋯
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>h : a ≤ n + n<GOAL>n * n + a < n.succ * n.succ
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>h : a ≤ n + n<GOAL>n * n + a < (n * n + (n + n)).succ
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I J : Ideal 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>f : M →ₗ[R] M'<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Nontrivial M<GOAL>(associatedPrimes R M).Nonempty
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I J : Ideal 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>f : M →ₗ[R] M'<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Nontrivial M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>(associatedPrimes R M).Nonempty