ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>inst✝⁷ : HasFiniteCoproducts D<VAR>inst✝⁶ : HasPullbacksOfInclusions D<VAR>inst✝⁵ : FinitaryExtensive C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)<VAR>inst✝¹ : (X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl<VAR>inst✝ : PreservesPullbacksOfInclusions Gl<VAR>this : PreservesColimitsOfSize.{?u.89276, ?u.89275, v, v'', u, u''} Gl<VAR>X Y : D<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>inst✝⁷ : HasFiniteCoproducts D<VAR>inst✝⁶ : HasPullbacksOfInclusions D<VAR>inst✝⁵ : FinitaryExtensive C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)<VAR>inst✝¹ : (X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl<VAR>inst✝ : PreservesPullbacksOfInclusions Gl<VAR>this : PreservesColimitsOfSize.{?u.89276, ?u.89275, v, v'', u, u''} Gl<VAR>X Y : D<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<GOAL>IsVanKampenColimit ((Cocones.precompose (isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ (pair X Y).rightUnitor).hom).obj c)
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>inst✝⁷ : HasFiniteCoproducts D<VAR>inst✝⁶ : HasPullbacksOfInclusions D<VAR>inst✝⁵ : FinitaryExtensive C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)<VAR>inst✝¹ : (X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl<VAR>inst✝ : PreservesPullbacksOfInclusions Gl<VAR>this✝ : PreservesColimitsOfSize.{?u.89276, ?u.89275, v, v'', u, u''} Gl<VAR>X Y : D<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>this : (Z : C) → (i : Discrete WalkingPair) → (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt) → PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl<GOAL>IsVanKampenColimit ((Cocones.precompose (isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ (pair X Y).rightUnitor).hom).obj c)
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>inst✝⁷ : HasFiniteCoproducts D<VAR>inst✝⁶ : HasPullbacksOfInclusions D<VAR>inst✝⁵ : FinitaryExtensive C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)<VAR>inst✝¹ : (X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl<VAR>inst✝ : PreservesPullbacksOfInclusions Gl<VAR>this✝ : PreservesColimitsOfSize.{?u.89276, ?u.89275, v, v'', u, u''} Gl<VAR>X Y : D<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>this : (Z : C) → (i : Discrete WalkingPair) → (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt) → PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl<GOAL>IsColimit (Gl.mapCocone (colimit.cocone (pair X Y ⋙ Gr)))
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>inst✝⁷ : HasFiniteCoproducts D<VAR>inst✝⁶ : HasPullbacksOfInclusions D<VAR>inst✝⁵ : FinitaryExtensive C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)<VAR>inst✝¹ : (X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl<VAR>inst✝ : PreservesPullbacksOfInclusions Gl<VAR>this✝ : PreservesColimitsOfSize.{?u.89276, ?u.89275, v, v'', u, u''} Gl<VAR>X Y : D<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>this : (Z : C) → (i : Discrete WalkingPair) → (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt) → PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl<GOAL>IsColimit ((Cocones.precompose (isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ (pair X Y).rightUnitor).hom).obj c)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>a b : P<GOAL>(lineMap a b) (1 / 2) = midpoint R a b
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : CommRing 𝔸<VAR>inst✝³ : TopologicalSpace 𝔸<VAR>inst✝² : TopologicalRing 𝔸<VAR>inst✝¹ : Algebra 𝕂 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>A : Matrix m m 𝔸<GOAL>exp 𝕂 Aᵀ = (exp 𝕂 A)ᵀ
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<GOAL>(B.domRestrict₁₂ W W).Nondegenerate
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<GOAL>(B.domRestrict₁₂ W W).SeparatingLeft
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<VAR>x : M<VAR>hx : x ∈ W<VAR>b₁ : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0<GOAL>⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<VAR>x : M<VAR>hx : x ∈ W<VAR>b₁ : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0<GOAL>x ∈ ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<VAR>x : M<VAR>hx : x ∈ W<VAR>b₁ : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0<VAR>y : M<VAR>hy : y ∈ W<GOAL>B.IsOrtho y x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<VAR>x : M<VAR>hx : x ∈ W<VAR>y : M<VAR>hy : y ∈ W<VAR>b₁ : ((B.domRestrict₁₂ W W) ⟨x, hx⟩) ⟨y, hy⟩ = 0<GOAL>B.IsOrtho y x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<VAR>x : M<VAR>hx : x ∈ W<VAR>y : M<VAR>hy : y ∈ W<VAR>b₁ : (B x) y = 0<GOAL>B.IsOrtho y x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<VAR>x : M<VAR>hx : x ∈ W<VAR>y : M<VAR>hy : y ∈ W<VAR>b₁ : (B x) y = 0<GOAL>B.IsOrtho x y
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : ¬p ^ (k + 1) = 2<GOAL>hζ.toInteger - 1 ∣ ↑↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : ¬p ^ (k + 1) = 2<VAR>this : NumberField K<GOAL>hζ.toInteger - 1 ∣ ↑↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : ¬p ^ (k + 1) = 2<VAR>this : NumberField K<VAR>H : (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ 0 - 1) = ↑↑p ^ ↑p ^ 0<GOAL>hζ.toInteger - 1 ∣ ↑↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : ¬p ^ (k + 1) = 2<VAR>this : NumberField K<VAR>H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p ^ 1<GOAL>hζ.toInteger - 1 ∣ ↑↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : ¬p ^ (k + 1) = 2<VAR>this : NumberField K<VAR>H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p ^ 1<GOAL>↑↑p ^ 1 ∣ ↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : ¬p ^ (k + 1) = 2<VAR>this : NumberField K<VAR>H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p ^ 1<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>h0 : p ∅<VAR>hU : q U<VAR>hμU : μ U ≠ ⊤<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ U, p K ∧ μ U < μ K + ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>h0 : p ∅<VAR>hU : q U<VAR>hμU : μ U ≠ ⊤<VAR>hε : ε ≠ 0<VAR>h₀ : μ U = 0<GOAL>∃ K ⊆ U, p K ∧ μ U < μ K + ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>h0 : p ∅<VAR>hU : q U<VAR>hμU : μ U ≠ ⊤<VAR>hε : ε ≠ 0<VAR>h₀ : μ U ≠ 0<GOAL>∃ K ⊆ U, p K ∧ μ U < μ K + ε
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<VAR>c : R<GOAL>(A.updateColumn i fun k => A k i + c • A k j).det = A.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<VAR>c : R<GOAL>(Aᵀ.updateRow i fun k => A k i + c • A k j).det = Aᵀ.det
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c : C<VAR>γ : c ⟶ c<VAR>hγ : γ ∈ S.arrows c c<GOAL>𝟙 c ∈ S.arrows c c
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c : C<VAR>γ : c ⟶ c<VAR>hγ : γ ∈ S.arrows c c<GOAL>𝟙 c = γ ≫ Groupoid.inv γ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>n : ℕ<VAR>x : ↑(Ioi 0)<GOAL>(volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>n : ℕ<VAR>x : ↑(Ioi 0)<VAR>hr₀ : 0 ≤ ↑x<GOAL>(volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>n : ℕ<VAR>x : ↑(Ioi 0)<VAR>hr₀ : 0 ≤ ↑x<GOAL>ENNReal.ofReal (∫ (x : ℝ) in 0 ..↑x, x ^ n) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>n : ℕ<VAR>x : ↑(Ioi 0)<VAR>hr₀ : 0 ≤ ↑x<GOAL>0 ≤ᶠ[ae (volume.restrict (Ioc 0 ↑x))] fun x => x ^ n
<VAR>p : ℕ<VAR>h : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hp : p ≠ 2<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p a = (-1) ^ (filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)).card
<VAR>p : ℕ<VAR>h : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha0 : ↑a ≠ 0<VAR>hp : Odd p<GOAL>legendreSym p a = (-1) ^ (filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)).card
<VAR>p : ℕ<VAR>h : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha0 : ↑a ≠ 0<VAR>hp : Odd p<VAR>this : ↑(legendreSym p a) = ↑((-1) ^ (filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)).card)<GOAL>legendreSym p a = (-1) ^ (filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)).card
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>𝟙 (e.inverse.obj Y) = 𝟙 (e.inverse.obj ((𝟭 D).obj Y))
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c d₁ d₂ : α<VAR>ha : a ≠ 0<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>hc : c = d₁ * d₂<VAR>hd₁ : d₁ ∣ a<VAR>h1 : IsUnit (gcd (d₁ ^ k) b)<GOAL>d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c d₁ d₂ : α<VAR>ha : a ≠ 0<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>hc : c = d₁ * d₂<VAR>hd₁ : d₁ ∣ a<VAR>h1 : IsUnit (gcd (d₁ ^ k) b)<VAR>h2 : d₁ ^ k ∣ a * b<GOAL>d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c d₁ d₂ : α<VAR>ha : a ≠ 0<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>hc : c = d₁ * d₂<VAR>hd₁ : d₁ ∣ a<VAR>h1 : IsUnit (gcd (d₁ ^ k) b)<VAR>h2 : d₁ ^ k ∣ b * a<GOAL>d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c d₁ d₂ : α<VAR>ha : a ≠ 0<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>hc : c = d₁ * d₂<VAR>hd₁ : d₁ ∣ a<VAR>h1 : IsUnit (gcd (d₁ ^ k) b)<VAR>h2 : d₁ ^ k ∣ b * a<VAR>h3 : d₁ ^ k ∣ a<GOAL>d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c d₁ d₂ : α<VAR>ha : a ≠ 0<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>hc : c = d₁ * d₂<VAR>hd₁ : d₁ ∣ a<VAR>h1 : IsUnit (gcd (d₁ ^ k) b)<VAR>h2 : d₁ ^ k ∣ b * a<VAR>h3 : d₁ ^ k ∣ a<VAR>h4 : d₁ ^ k ≠ 0<GOAL>d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
<VAR>M : Type u_1<VAR>inst✝⁶ : Monoid M<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : MulSemiringAction M R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : MulSemiringAction M S<VAR>G : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : MulSemiringAction G S<VAR>g : G<VAR>f : S[X]<VAR>x : S<GOAL>eval x (g • f) = g • eval (g⁻¹ • x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((κ.map f hf) a) s = (κ a) (f ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>⇑(monomial R 0) = ⇑(C R)
<VAR>X : TopCat<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>x : ↑X<VAR>hx : x ∈ iSup U<GOAL>∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
<VAR>X : TopCat<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>x : ↑X<VAR>hx : x ∈ iSup U<VAR>i : ι<VAR>hxi : x ∈ U i<GOAL>∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R✝ : Type u_3<VAR>S✝ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : OrderedRing S<VAR>abv : AbsoluteValue R S<VAR>a b : R<GOAL>abv a ≤ abv (a - b) + abv b
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : x ≠ 0 ∨ 0 < y<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (x, y)
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : x ≠ 0 ∨ 0 < y<VAR>this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (x, y)
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : x ≠ 0 ∨ 0 < y<VAR>this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)<GOAL>ContinuousAt (toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)) (x, y)
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : x ≠ 0 ∨ 0 < y<VAR>this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)<GOAL>ContinuousAt (fun p => p.1 ^ p.2) (↑(x, y).1, (x, y).2)
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : x ≠ 0 ∨ 0 < y<VAR>this : (fun p => p.1 ^ p.2) = toNNReal ∘ (fun p => p.1 ^ p.2) ∘ fun p => (↑p.1, p.2)<GOAL>ContinuousAt (fun p => (↑p.1, p.2)) (x, y)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>n : ℕ<VAR>ha : 0 ≤ 0<GOAL>⌊0⌋₊ = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<GOAL>Tendsto (fun x => f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s.toFinset ⊂ t.toFinset ↔ s ⊂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝¹ : HasLeftDual X<VAR>inst✝ : HasLeftDual Y<VAR>f : X ⟶ Y<VAR>g : ᘁX ⟶ Z<GOAL>((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ≫ g = 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝¹ : HasLeftDual X<VAR>inst✝ : HasLeftDual Y<VAR>f : X ⟶ Y<VAR>g : ᘁX ⟶ Z<GOAL>𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z = (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (g ⊗ f) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝¹ : HasLeftDual X<VAR>inst✝ : HasLeftDual Y<VAR>f : X ⟶ Y<VAR>g : ᘁX ⟶ Z<GOAL>𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (g ▷ (Y ⊗ ᘁY) ≫ Z ◁ ε_ (ᘁY) Y) ⊗≫ 𝟙 Z = (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f ≫ g ▷ Y) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : b ≤ a<GOAL>a - b + c = a + c - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<GOAL>s.ncard = 1 ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s.ncard = 1<GOAL>∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s.ncard = 1<VAR>hft : Fintype ↑s<GOAL>∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hft : Fintype ↑s<VAR>h : ∃ a, s.toFinset = {a}<GOAL>∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hft : Fintype ↑s<VAR>h : ∃ a, s.toFinset = {a}<VAR>a : α<VAR>ha : s.toFinset = {a}<GOAL>s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hft : Fintype ↑s<VAR>h : ∃ a, s.toFinset = {a}<VAR>a : α<VAR>ha : s.toFinset = {a}<GOAL>∀ (x : α), x ∈ s ↔ x = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hft : Fintype ↑s<VAR>h : ∃ a, s.toFinset = {a}<VAR>a : α<VAR>ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a<GOAL>∀ (x : α), x ∈ s ↔ x = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<GOAL>eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ (ν a) univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>x : γ<GOAL>‖κ.densityProcess ν n a x s‖ ≤ 1