ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b✝ c d e : α<VAR>m n : ℤ<VAR>a : α<VAR>h : 0 < a<VAR>b : α<VAR>this : 0 < a / max (b + 1) 1<GOAL>b * (a / max (b + 1) 1) < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b✝ c d e : α<VAR>m n : ℤ<VAR>a : α<VAR>h : 0 < a<VAR>b : α<VAR>this : 0 < a / max (b + 1) 1<GOAL>b < max (b + 1) 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>interior (a • s) + closure (b • s) = interior (a • s) + b • s
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>hizw : (f.map ⋯ k) z = (f.map ⋯ k) w<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<VAR>ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<VAR>ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)<VAR>z' w' : M<VAR>x : ↥S<VAR>hxz : z * f.toMap ↑x = f.toMap z'<VAR>hxw : w * f.toMap ↑x = f.toMap w'<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<VAR>ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)<VAR>z' w' : M<VAR>x : ↥S<VAR>hxz : z * f.toMap ↑x = f.toMap z'<VAR>hxw : w * f.toMap ↑x = f.toMap w'<VAR>this : k.toMap (g z') = k.toMap (g w')<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<VAR>ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)<VAR>z' w' : M<VAR>x : ↥S<VAR>hxz : z * f.toMap ↑x = f.toMap z'<VAR>hxw : w * f.toMap ↑x = f.toMap w'<VAR>this : k.toMap (g z') = k.toMap (g w')<VAR>c : M<VAR>hc : c ∈ ↑S<VAR>eq : ↑⟨g c, ⋯⟩ * g z' = ↑⟨g c, ⋯⟩ * g w'<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<VAR>ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)<VAR>z' w' : M<VAR>x : ↥S<VAR>hxz : z * f.toMap ↑x = f.toMap z'<VAR>hxw : w * f.toMap ↑x = f.toMap w'<VAR>this : k.toMap (g z') = k.toMap (g w')<VAR>c : M<VAR>hc : c ∈ ↑S<VAR>eq : c * z' = c * w'<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z w : N<VAR>i : N →* Q := f.map ⋯ k<VAR>hizw : i z = i w<VAR>ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)<VAR>z' w' : M<VAR>x : ↥S<VAR>hxz : z * f.toMap ↑x = f.toMap z'<VAR>hxw : w * f.toMap ↑x = f.toMap w'<VAR>this : k.toMap (g z') = k.toMap (g w')<VAR>c : M<VAR>hc : c ∈ ↑S<VAR>eq : c * z' = c * w'<GOAL>∃ c, ↑c * z' = ↑c * w'
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>i : m<GOAL>(M.toMvPolynomial i).totalDegree ≤ 1
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>(x * y).Numeric
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<GOAL>(x * y).Numeric
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<GOAL>(x * y).Numeric
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>ihxyn : IH1 (-x) (-y)<GOAL>(x * y).Numeric
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>ihxyn : IH1 (-x) (-y)<VAR>ihyxn : IH1 (-y) (-x)<GOAL>(x * y).Numeric
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>ihxyn : IH1 (-x) (-y)<VAR>ihyxn : IH1 (-y) (-x)<GOAL>∀ (i : (x * y).LeftMoves) (j : (x * y).RightMoves), (x * y).moveLeft i < (x * y).moveRight j
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>ihxyn : IH1 (-x) (-y)<VAR>ihyxn : IH1 (-y) (-x)<GOAL>∀ (i : (x * y).LeftMoves), ((x * y).moveLeft i).Numeric
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>ihxyn : IH1 (-x) (-y)<VAR>ihyxn : IH1 (-y) (-x)<GOAL>∀ (j : (x * y).RightMoves), ((x * y).moveRight j).Numeric
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c : X ⟶ Y<GOAL>a - b + c = a - (b - c)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>x : Π₀ (i : ι), β i<VAR>x✝ : x ∈ ⊤<GOAL>x ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>x : Π₀ (i : ι), β i<VAR>x✝ : x ∈ ⊤<GOAL>0 ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>x : Π₀ (i : ι), β i<VAR>x✝ : x ∈ ⊤<GOAL>∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) → single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁶ : Field F<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K₁<VAR>inst✝¹¹ : Field K₂<VAR>inst✝¹⁰ : Field K₃<VAR>inst✝⁹ : Algebra F K₁<VAR>inst✝⁸ : Algebra F K₂<VAR>inst✝⁷ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra K₁ E<VAR>inst✝³ : Algebra K₂ E<VAR>inst✝² : IsScalarTower F K₁ E<VAR>inst✝¹ : IsScalarTower F K₂ E<VAR>inst✝ : Normal F K₁<VAR>h1 : IsSolvable (K₁ ≃ₐ[F] K₁)<VAR>h2 : IsSolvable (E ≃ₐ[K₁] E)<GOAL>IsSolvable (E ≃ₐ[F] E)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁶ : Field F<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K₁<VAR>inst✝¹¹ : Field K₂<VAR>inst✝¹⁰ : Field K₃<VAR>inst✝⁹ : Algebra F K₁<VAR>inst✝⁸ : Algebra F K₂<VAR>inst✝⁷ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra K₁ E<VAR>inst✝³ : Algebra K₂ E<VAR>inst✝² : IsScalarTower F K₁ E<VAR>inst✝¹ : IsScalarTower F K₂ E<VAR>inst✝ : Normal F K₁<VAR>h1 : IsSolvable (K₁ ≃ₐ[F] K₁)<VAR>h2 : IsSolvable (E ≃ₐ[K₁] E)<VAR>f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E := { toFun := fun ϕ => AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯, map_one' := ⋯, map_mul' := ⋯ }<GOAL>IsSolvable (E ≃ₐ[F] E)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁶ : Field F<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K₁<VAR>inst✝¹¹ : Field K₂<VAR>inst✝¹⁰ : Field K₃<VAR>inst✝⁹ : Algebra F K₁<VAR>inst✝⁸ : Algebra F K₂<VAR>inst✝⁷ : Algebra F K₃<VAR>ϕ✝ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra K₁ E<VAR>inst✝³ : Algebra K₂ E<VAR>inst✝² : IsScalarTower F K₁ E<VAR>inst✝¹ : IsScalarTower F K₂ E<VAR>inst✝ : Normal F K₁<VAR>h1 : IsSolvable (K₁ ≃ₐ[F] K₁)<VAR>h2 : IsSolvable (E ≃ₐ[K₁] E)<VAR>f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E := { toFun := fun ϕ => AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯, map_one' := ⋯, map_mul' := ⋯ }<VAR>ϕ : E ≃ₐ[F] E<VAR>hϕ : ϕ ∈ (AlgEquiv.restrictNormalHom K₁).ker<VAR>x : K₁<GOAL>ϕ.toFun ((algebraMap K₁ E) x) = (algebraMap K₁ E) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>huv : v ≤ᶠ[lt] u<VAR>t : ι<GOAL>-(∫ (x : ℝ) in v t..u t, f x ∂μ - (μ (Ioc (v t) (u t))).toReal • c) = ∫ (x : ℝ) in u t..v t, f x ∂μ + (μ (Ioc (v t) (u t))).toReal • c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>a : Set α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ x ∈ a, p x
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc : a % c + b % c < c<GOAL>(a + b) % c = a % c + b % c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<GOAL>l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<GOAL>(a, b, c) ∈ Corners.triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<GOAL>(∃ a_1 b_1, (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) ↔ (a, b) ∈ A ∧ c = a + b
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<GOAL>(∃ a_1 b_1, (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) → (a, b) ∈ A ∧ c = a + b
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<GOAL>(hT.eigenvectorBasis hn).repr (T v) i = ↑(hT.eigenvalues hn i) * (hT.eigenvectorBasis hn).repr v i
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<GOAL>∀ (w : EuclideanSpace 𝕜 (Fin n)), T ((hT.eigenvectorBasis hn).repr.symm w) = (hT.eigenvectorBasis hn).repr.symm fun i => ↑(hT.eigenvalues hn i) * w i
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<VAR>w : EuclideanSpace 𝕜 (Fin n)<GOAL>T ((hT.eigenvectorBasis hn).repr.symm w) = (hT.eigenvectorBasis hn).repr.symm fun i => ↑(hT.eigenvalues hn i) * w i
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<VAR>w : EuclideanSpace 𝕜 (Fin n)<GOAL>∑ x : Fin n, w x • ↑(hT.eigenvalues hn x) • (hT.eigenvectorBasis hn) x = ∑ x : Fin n, (↑(hT.eigenvalues hn x) * w x) • (hT.eigenvectorBasis hn) x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<VAR>w : EuclideanSpace 𝕜 (Fin n)<GOAL>∀ (a : Fin n), w a • ↑(hT.eigenvalues hn a) • (hT.eigenvectorBasis hn) a = (↑(hT.eigenvalues hn a) * w a) • (hT.eigenvectorBasis hn) a
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<VAR>w : EuclideanSpace 𝕜 (Fin n)<VAR>a : Fin n<GOAL>w a • ↑(hT.eigenvalues hn a) • (hT.eigenvectorBasis hn) a = (↑(hT.eigenvalues hn a) * w a) • (hT.eigenvectorBasis hn) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>r r' : ℚ<VAR>hrr' : r ≤ r'<GOAL>∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) a, (preCDF ρ r (a, c).2).toReal ≤ (preCDF ρ r' (a, c).2).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a✝ : Unit<VAR>r r' : ℚ<VAR>hrr' : r ≤ r'<VAR>a : α<VAR>h1 : Monotone fun r => preCDF ρ r a<VAR>h2 : ∀ (r : ℚ), preCDF ρ r a ≤ 1<GOAL>(preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a✝ : Unit<VAR>r r' : ℚ<VAR>hrr' : r ≤ r'<VAR>a : α<VAR>h1 : Monotone fun r => preCDF ρ r a<VAR>h2 : ∀ (r : ℚ), preCDF ρ r a ≤ 1<VAR>h_ne_top : ∀ (r : ℚ), preCDF ρ r a ≠ ⊤<GOAL>(preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a✝ : Unit<VAR>r r' : ℚ<VAR>hrr' : r ≤ r'<VAR>a : α<VAR>h1 : Monotone fun r => preCDF ρ r a<VAR>h2 : ∀ (r : ℚ), preCDF ρ r a ≤ 1<VAR>h_ne_top : ∀ (r : ℚ), preCDF ρ r a ≠ ⊤<GOAL>preCDF ρ r a ≤ preCDF ρ r' a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>q : ℚ<GOAL>∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) a, (preCDF ρ q (a, c).2).toReal ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>q : ℚ<GOAL>∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a✝ : Unit<VAR>q : ℚ<VAR>a : α<VAR>ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1<GOAL>(preCDF ρ q a).toReal ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a✝ : Unit<VAR>q : ℚ<VAR>a : α<VAR>ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1<GOAL>preCDF ρ q a ≤ ENNReal.ofReal 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<GOAL>Tendsto (fun m => ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<VAR>h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<VAR>h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ENNReal.toReal 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<VAR>h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)<VAR>h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0)<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ENNReal.toReal 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<GOAL>Tendsto (fun m => ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 (((Kernel.const Unit ρ.fst) a) univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<VAR>h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atTop (𝓝 (ρ.fst univ))<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : ℕ → ℚ<VAR>x✝ : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<VAR>h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atTop (𝓝 (ρ.fst univ))<VAR>h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst univ).toReal)<GOAL>Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : Unit<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>q : ℚ<GOAL>∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a = (((Kernel.const Unit ρ) a) (s ×ˢ Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>(⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |b - a| < r}).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>inst✝ : NoMaxOrder α<VAR>a x : α<VAR>hx : x > 0<VAR>y : α<VAR>hy : y > 0<GOAL>∃ k > 0, {b | |b - a| < k} ⊆ {b | |b - a| < x} ∧ {b | |b - a| < k} ⊆ {b | |b - a| < y}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<VAR>e : PartialEquiv M E := f.extend I<GOAL>map (↑e) (𝓝[s] y) = 𝓝[↑e '' (e.source ∩ s)] ↑e y
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>f : Γ → Γ<VAR>n : ℕ<VAR>IH : ∀ (L R : ListBlank Γ), write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))<VAR>L R : ListBlank Γ<GOAL>write (f (R.nth (n + 1))) ((move Dir.right)^[n + 1] (mk' L R)) = (move Dir.right)^[n + 1] (mk' L (ListBlank.modifyNth f (n + 1) R))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<GOAL>1 < card α ↔ Nontrivial α