ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>this : Monotone fun n => ∫⁻ (x : α), f n x ∂μ<GOAL>∫⁻ (x : α), F x ∂μ = ⨆ n, ∫⁻ (x : α), f n x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>this : Monotone fun n => ∫⁻ (x : α), f n x ∂μ<GOAL>∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ n, f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>this : Monotone fun n => ∫⁻ (x : α), f n x ∂μ<GOAL>F =ᶠ[ae μ] fun a => ⨆ n, f n a
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>(aeval (Function.uncurry fun i => (![] i).coeff)) (wittOne p 0) = 1
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>(fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b c x : R<VAR>h : a * x * x + b * x + c = 0<GOAL>b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a✝ : α<VAR>b✝ : β<VAR>a : α<VAR>b : β<GOAL>{a} ×ˢ {b} = {(a, b)}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>ι : Type u_4<VAR>p : ι → Submodule R M<VAR>m : M<VAR>hm : m ∈ ⨆ i, p i<GOAL>∃ s, m ∈ ⨆ i ∈ s, p i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>ι : Type u_4<VAR>p : ι → Submodule R M<VAR>m : M<VAR>hm : m ∈ ⨆ i, p i<VAR>this : span R {m} ≤ ⨆ i, p i → ∃ s, span R {m} ≤ ⨆ i ∈ s, p i<GOAL>∃ s, m ∈ ⨆ i ∈ s, p i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>ι : Type u_4<VAR>p : ι → Submodule R M<VAR>m : M<VAR>hm : m ∈ ⨆ i, p i<VAR>this : m ∈ ⨆ i, p i → ∃ s, m ∈ ⨆ i ∈ s, p i<GOAL>∃ s, m ∈ ⨆ i ∈ s, p i
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z p₁ p₂ p : P<GOAL>midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>(∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) y ∧ toMatrix' y = A₁) ↔ J.IsAdjointPair J₂ A₁ A₁
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<GOAL>Measure.map (fun x => y + x) (gaussianReal μ v) = gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<GOAL>Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : a.re < 0<VAR>b : ℂ<VAR>s : ℝ<GOAL>(fun x => ‖cexp (a * ↑x ^ 2 + b * ↑x)‖) =o[atTop] fun x => x ^ s
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : a.re < 0<VAR>b : ℂ<VAR>s x : ℝ<GOAL>‖cexp (a * ↑x ^ 2 + b * ↑x)‖ = rexp (a.re * x ^ 2 + b.re * x)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y✝ : E<VAR>h : IsLocalMin f a<VAR>hf : HasFDerivAt f f' a<VAR>y : E<GOAL>f' y = 0 y
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<GOAL>M.charpoly.Monic
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i))).Monic<GOAL>M.charpoly.Monic
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).Monic<GOAL>M.charpoly.Monic
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>M.charpoly.leadingCoeff = 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>(∏ i : n, (X - C (M i i)) - M.charpoly).degree < M.charpoly.degree
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>(∏ i : n, (X - C (M i i)) - M.charpoly).degree < ↑(Fintype.card n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>(-(M.charpoly - ∏ i : n, (X - C (M i i)))).degree < ↑(Fintype.card n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>(M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>↑(Fintype.card n - 1) < ↑(Fintype.card n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>Fintype.card n - 1 < Fintype.card n
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>(Fintype.card n).pred < Fintype.card n
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h : ¬Fintype.card n = 0<VAR>mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1<GOAL>Fintype.card n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s✝ : Set α<VAR>a✝ : α<VAR>f : α → β<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(map f (dirac a)) s = (dirac (f a)) s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>c : 𝕜<VAR>s : Set α<VAR>x : F<GOAL>(weightedSMul μ s) (c • x) = c • (weightedSMul μ s) x
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b<VAR>c' : Ordinal.{u_1}<VAR>h : c' < c<GOAL>(a + b) * c' ≤ a * c
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b<VAR>c' : Ordinal.{u_1}<VAR>h : c' < c<GOAL>(a + b) * succ c' ≤ a * c
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b<VAR>c' : Ordinal.{u_1}<VAR>h : c' < c<GOAL>a * succ c' + b ≤ a * c
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b<VAR>c' : Ordinal.{u_1}<VAR>h : c' < c<GOAL>a * succ c' + ?m.296861 ≤ a * c
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b<VAR>c' : Ordinal.{u_1}<VAR>h : c' < c<GOAL>Ordinal.{u_1}
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<VAR>l : c.IsLimit<VAR>IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b<VAR>c' : Ordinal.{u_1}<VAR>h : c' < c<GOAL>b ≤ ?m.296861
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddCommGroup R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>x ∈ skewAdjoint R ↔ star x = -x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddCommGroup R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>x ∈ (skewAdjoint R).carrier ↔ star x = -x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>IsIso (J.toPlus P)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)<GOAL>IsIso (J.toPlus P)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)<GOAL>∀ (X : Cᵒᵖ), IsIso ((J.toPlus P).app X)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)<VAR>X : Cᵒᵖ<GOAL>IsIso (colimit.ι (J.diagram P (unop X)) (op ⊤))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)<VAR>X : Cᵒᵖ<GOAL>∀ (S T : (J.Cover (unop X))ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P (unop X)).map f)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)<VAR>X : Cᵒᵖ<VAR>S T : (J.Cover (unop X))ᵒᵖ<VAR>e : S ⟶ T<GOAL>IsIso ((J.diagram P (unop X)).map e)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)<VAR>X : Cᵒᵖ<VAR>S T : (J.Cover (unop X))ᵒᵖ<VAR>e : S ⟶ T<VAR>this : (unop S).toMultiequalizer P ≫ (J.diagram P (unop X)).map e = (unop T).toMultiequalizer P<GOAL>IsIso ((J.diagram P (unop X)).map e)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>ho : lift.{v, u} o.card < c<GOAL>lift.{v, u} o.card < c.ord.cof
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<VAR>h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)<GOAL>‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>l : List α<GOAL>(a :: l).eraseIdx 0 = a :: l ↔ (a :: l).length ≤ 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : StandardBorelSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T0Space Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace Y<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace Z<VAR>inst✝ : CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Surjective f<VAR>s : Set Z<VAR>h : MeasurableSet (f ⁻¹' s)<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : StandardBorelSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T0Space Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace Y<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace Z<VAR>inst✝ : CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Surjective f<VAR>s : Set Z<VAR>h : MeasurableSet (f ⁻¹' s)<VAR>τ : TopologicalSpace Z<VAR>left✝¹ : SecondCountableTopology Z<VAR>left✝ : T4Space Z<VAR>right✝ : OpensMeasurableSpace Z<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : StandardBorelSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T0Space Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace Y<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace Z<VAR>inst✝ : CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Surjective f<VAR>s : Set Z<VAR>h : MeasurableSet (f ⁻¹' s)<VAR>τ : TopologicalSpace Z<VAR>left✝¹ : SecondCountableTopology Z<VAR>left✝ : T4Space Z<VAR>right✝ : OpensMeasurableSpace Z<GOAL>AnalyticSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : StandardBorelSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T0Space Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace Y<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace Z<VAR>inst✝ : CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Surjective f<VAR>s : Set Z<VAR>h : MeasurableSet (f ⁻¹' s)<VAR>τ : TopologicalSpace Z<VAR>left✝¹ : SecondCountableTopology Z<VAR>left✝ : T4Space Z<VAR>right✝ : OpensMeasurableSpace Z<GOAL>AnalyticSet sᶜ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<GOAL>levyProkhorovEDist μ ν ≤ δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<GOAL>∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<GOAL>ν B ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<GOAL>ν B ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<GOAL>ν (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<GOAL>1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<VAR>Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ<GOAL>1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<VAR>Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ<VAR>h : μ (thickening ε.toReal B)ᶜ ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε<GOAL>1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<VAR>Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ<VAR>h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε<GOAL>1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<VAR>Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ<VAR>h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε<VAR>almost : 1 - μ (thickening ε.toReal B) + μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε + μ (thickening ε.toReal B)<GOAL>1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε