ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : LeftInvOn f' f s<GOAL>f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : LeftInvOn f' f s<GOAL>f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : LeftInvOn f' f s<GOAL>f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : LeftInvOn f' f s<VAR>x : α<VAR>hx : x ∈ s<VAR>h₁ : f x ∈ f' ⁻¹' s₁<GOAL>f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(cosh ↑x).im = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : SemilatticeSup β<VAR>ι : Sort u_4<VAR>S : Set (Set α)<VAR>f✝ : ι → Set α<VAR>s t : Set α<VAR>a✝ : α<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupHomClass F α β<VAR>hs : SupClosed s<VAR>f : F<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>f a ⊔ f b ∈ ⇑f '' s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : SemilatticeSup β<VAR>ι : Sort u_4<VAR>S : Set (Set α)<VAR>f✝ : ι → Set α<VAR>s t : Set α<VAR>a✝ : α<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupHomClass F α β<VAR>hs : SupClosed s<VAR>f : F<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>f (a ⊔ b) ∈ ⇑f '' s
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>h : M.Base B<GOAL>M✶.Base (M.E \ B)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L : Ideal R<VAR>x y : R<VAR>I J : Ideal R<GOAL>span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ
<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<VAR>c : n → R<GOAL>(eval c) (M.toMvPolynomial i) = (M *ᵥ c) i
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>a : R<GOAL>a / 2 - a = -(a / 2)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>ha : a ∉ s<GOAL>insert a s ⊆ insert a t ↔ s ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>ha : a ∉ s<VAR>h : insert a s ⊆ insert a t<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>ha : x ∉ s<VAR>h : insert x s ⊆ insert x t<GOAL>x ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>ha : a ∉ s<VAR>h : insert a s ⊆ insert a t<VAR>x : α<VAR>hx : x ∈ s<VAR>hxt : x ∈ t<GOAL>x ∈ t
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>normSq (star a) = normSq a
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α<VAR>a b c d : α<GOAL>a ⊓ b ≤ b ∧ b ≤ a ⊓ b ↔ b ≤ a
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsAlgClosed K<VAR>h : ∀ a ∈ S, NeZero ↑↑a<GOAL>IsCyclotomicExtension S K K
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsAlgClosed K<VAR>h : ∀ a ∈ S, NeZero ↑↑a<VAR>a : ℕ+<VAR>ha : a ∈ S<GOAL>∃ r, IsPrimitiveRoot r ↑a
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsAlgClosed K<VAR>h : ∀ a ∈ S, NeZero ↑↑a<VAR>a : ℕ+<VAR>ha : a ∈ S<VAR>r : K<VAR>hr : (aeval r) (cyclotomic (↑a) K) = 0<GOAL>∃ r, IsPrimitiveRoot r ↑a
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsAlgClosed K<VAR>h : ∀ a ∈ S, NeZero ↑↑a<VAR>a : ℕ+<VAR>ha : a ∈ S<VAR>r : K<VAR>hr : (aeval r) (cyclotomic (↑a) K) = 0<VAR>this : NeZero ↑↑a<GOAL>IsPrimitiveRoot r ↑a
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<GOAL>0 < z * z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<GOAL>0 < x ^ 2 + y ^ 2
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hc' : x.gcd y ≠ 0<GOAL>0 < x ^ 2 + y ^ 2
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hc' : x.gcd y ≠ 0<VAR>hxz : x ≠ 0<GOAL>0 < x ^ 2 + y ^ 2
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hc' : x.gcd y ≠ 0<VAR>hyz : y ≠ 0<GOAL>0 < x ^ 2 + y ^ 2
<VAR>α : Type u<VAR>app : List α → List α<VAR>inv : ∀ (l : List α), app l = app [] ++ l<GOAL>(fun x => app [] ++ x) = app
<VAR>α : Type u<VAR>app : List α → List α<VAR>inv : ∀ (l : List α), app l = app [] ++ l<VAR>x : List α<GOAL>app [] ++ x = app x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>hs : IsClosed s<VAR>a : α<GOAL>a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>max a b = if a ≤ b then b else a
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : MonoidalCategory C<VAR>P : C → Prop<VAR>inst✝² : MonoidalPredicate P<VAR>P' : C → Prop<VAR>inst✝¹ : MonoidalPredicate P'<VAR>inst✝ : BraidedCategory C<VAR>h : ∀ ⦃X : C⦄, P X → P' X<VAR>X Y : FullSubcategory P<GOAL>(fullMonoidalSubcategory.map h).map (β_ X Y).hom = inv ((fullMonoidalSubcategory.map h).μ X Y) ≫ (β_ ((fullMonoidalSubcategory.map h).obj X) ((fullMonoidalSubcategory.map h).obj Y)).hom ≫ (fullMonoidalSubcategory.map h).μ Y X
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : MonoidalCategory C<VAR>P : C → Prop<VAR>inst✝² : MonoidalPredicate P<VAR>P' : C → Prop<VAR>inst✝¹ : MonoidalPredicate P'<VAR>inst✝ : BraidedCategory C<VAR>h : ∀ ⦃X : C⦄, P X → P' X<VAR>X Y : FullSubcategory P<GOAL>(fullMonoidalSubcategory.map h).μ X Y ≫ (fullMonoidalSubcategory.map h).map (β_ X Y).hom = (β_ ((fullMonoidalSubcategory.map h).obj X) ((fullMonoidalSubcategory.map h).obj Y)).hom ≫ (fullMonoidalSubcategory.map h).μ Y X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : OrderedCommGroup α<VAR>inst✝ : OrderedCommGroup β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<GOAL>Antivary f g⁻¹ ↔ Monovary f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>C : Ordinal.{u_4} → Sort u_5<VAR>o : Ordinal.{u_4}<VAR>H₁ : C 0<VAR>H₂ : (o : Ordinal.{u_4}) → C o → C (succ o)<VAR>H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o<VAR>h : o.IsLimit<GOAL>o.limitRecOn H₁ H₂ H₃ = H₃ o h fun x _h => x.limitRecOn H₁ H₂ H₃
<VAR>d₁ d₂ n₁ n₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b : α<VAR>inst✝ : OrderTop α<GOAL>succ ⊤ = ⊤
<VAR>m : ℤ<VAR>p : ↥(Submonoid.powers 2)<GOAL>dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = ↑m * powHalf (Submonoid.log p)
<VAR>m : ℤ<VAR>p : ↥(Submonoid.powers 2)<GOAL>dyadicMap (Localization.mk m p) = ↑m * powHalf (Submonoid.log p)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<VAR>hf : f.ker ≤ H<GOAL>H.index ∣ (map f H).index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<VAR>hf : f.ker ≤ H<GOAL>H.index ∣ H.index * f.range.index
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : (⨁ f) ⊗ X ⟶ Y<VAR>w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : (⨁ f) ⊗ X ⟶ Y<VAR>w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h<GOAL>(rightDistributor f X).inv ≫ g = (rightDistributor f X).inv ≫ h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : (⨁ f) ⊗ X ⟶ Y<VAR>w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h<VAR>j✝ : J<GOAL>biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g = biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : (⨁ f) ⊗ X ⟶ Y<VAR>w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h<VAR>j✝ : J<GOAL>biproduct.ι f j✝ ▷ X ≫ g = biproduct.ι f j✝ ▷ X ≫ h
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅⊥, N⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅⊥, N⁆ ≤ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>m : M<VAR>x : L<VAR>n : ↥N<VAR>hx : x ∈ ⊥<VAR>hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m<GOAL>⁅↑⟨x, hx⟩, ↑n⁆ ∈ ↑⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>m : M<VAR>x : L<VAR>n : ↥N<VAR>hx✝ : x ∈ ⊥<VAR>hx : x = 0<VAR>hn : ⁅↑⟨x, hx✝⟩, ↑n⁆ = m<GOAL>⁅↑⟨x, hx✝⟩, ↑n⁆ ∈ ↑⊥
<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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>∃ r, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ ↥⊤.direction = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>∃ r, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ ↥⊤.direction = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>ps ⊆ ↑⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Nontrivial S<VAR>h : IsAdjoinRootMonic S f<VAR>x : R<VAR>i : ℕ<GOAL>h.coeff ((algebraMap R S) x) i = Pi.single 0 x i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Nontrivial S<VAR>h : IsAdjoinRootMonic S f<VAR>x : R<VAR>i : ℕ<GOAL>x * Pi.single 0 1 i = Pi.single 0 x i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Nontrivial S<VAR>h : IsAdjoinRootMonic S f<VAR>x : R<VAR>i : ℕ<GOAL>∀ (i : ℕ), (fun x_1 y => x * y) i 0 = 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' (Ici x) x<VAR>hr : ‖f'‖ < r<GOAL>∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' (Ici x) x<VAR>hr : ‖f'‖ < r<VAR>this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r<GOAL>∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' (Ici x) x<VAR>hr : ‖f'‖ < r<VAR>this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r<VAR>z : ℝ<VAR>hxz : x < z<VAR>hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r<GOAL>(z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<VAR>h : NeZero ↑0<GOAL>False
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<GOAL>o.oangle x (-x) = ↑π
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<VAR>h : ↑u = a<GOAL>a * ↑u⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hMpos : 0 < M<VAR>hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : a < b<VAR>hcd : c < d<VAR>this : MulPosStrictMono α<GOAL>a * c < b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring α<VAR>a b d : α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : a < b<VAR>this : MulPosStrictMono α<VAR>hcd : 0 < d<GOAL>a * 0 < b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : a < b<VAR>hcd : c < d<VAR>this : MulPosStrictMono α<VAR>hc : 0 < c<GOAL>a * c < b * d
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ✝ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure (E × ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>ν : Measure E := addHaar<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ✝ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure (E × ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>ν : Measure E := addHaar<VAR>A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ✝ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure (E × ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>ν : Measure E := addHaar<VAR>A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ<VAR>Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ✝ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure (E × ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>ν : Measure E := addHaar<VAR>A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ<VAR>Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)<VAR>Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ✝ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure (E × ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>ν : Measure E := addHaar<VAR>A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ<VAR>Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)<VAR>Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)<VAR>Hfg : Integrable (fun x => (B (f x)) (g x)) (ν.prod volume)<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ