ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>z : ℂ<VAR>hz : 1 + -z ∈ slitPlane<GOAL>log (1 + -z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹
<VAR>z : ℂ<VAR>hz : 1 + -z ∈ slitPlane<GOAL>log (1 + -z) = -z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹
<VAR>z : ℂ<VAR>hz : 1 + -z ∈ slitPlane<VAR>x✝ : ℝ<GOAL>1 - x✝ • z = 1 + x✝ • -z
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i : ℕ<VAR>a : α<VAR>b : β a<VAR>hh : b ∈ approx (⇑f) i a<GOAL>b ∈ Part.fix (⇑f) a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i : ℕ<VAR>a : α<VAR>b : β a<VAR>hh : b ∈ approx (⇑f) i a<GOAL>∃ i, b ∈ approx (⇑f) i a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓟 {a} ↔ s ∈ pure a
<VAR>V : Type (u + 1)<VAR>inst✝³ : LargeCategory V<VAR>G✝ : MonCat<VAR>W : Type (u + 1)<VAR>inst✝² : LargeCategory W<VAR>inst✝¹ : MonoidalCategory V<VAR>inst✝ : MonoidalCategory W<VAR>F : MonoidalFunctor V W<VAR>G : MonCat<VAR>X Y : Action V G<GOAL>(inv ((F.mapAction G).μ X Y)).hom = inv (F.μ X.V Y.V)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Nontrivial R<VAR>ι : Type v<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>#ι ≤ Module.rank R M
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges
<VAR>x : ℂ<GOAL>sin (x + ↑π / 2) = cos x
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<VAR>v w : V<GOAL>(fromEdgeSet Set.univ).Adj v w ↔ ⊤.Adj v w
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : s ∈ 𝓝 x<GOAL>HasFDerivAt f f' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<GOAL>(⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hL : L ≤ 𝓝 x<VAR>h : HasFDerivAtFilter f f' x L<GOAL>Tendsto f L (𝓝 (f x))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hL : L ≤ 𝓝 x<VAR>h : HasFDerivAtFilter f f' x L<VAR>this : Tendsto (fun x' => f x' - f x) L (𝓝 0)<GOAL>Tendsto f L (𝓝 (f x))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hL : L ≤ 𝓝 x<VAR>h : HasFDerivAtFilter f f' x L<VAR>this✝ : Tendsto (fun x' => f x' - f x) L (𝓝 0)<VAR>this : Tendsto (fun x_1 => f x_1 - f x + f x) L (𝓝 (0 + f x))<GOAL>Tendsto f L (𝓝 (f x))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hL : L ≤ 𝓝 x<VAR>h : HasFDerivAtFilter f f' x L<VAR>this✝ : Tendsto (fun x' => f x' - f x) L (𝓝 0)<VAR>this : Tendsto (fun x_1 => f x_1 - f x + f x) L (𝓝 (f x))<GOAL>Tendsto f L (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<GOAL>TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<GOAL>(∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : DivInvMonoid M<VAR>inst✝ : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>x : M<VAR>hx : x ∈ K<VAR>n : ℕ<GOAL>x ^ ↑n ∈ K
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : DivInvMonoid M<VAR>inst✝ : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>x : M<VAR>hx : x ∈ K<VAR>n : ℕ<GOAL>x ^ n ∈ K
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : DivInvMonoid M<VAR>inst✝ : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>x : M<VAR>hx : x ∈ K<VAR>n : ℕ<GOAL>x ^ -[n+1] ∈ K
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : DivInvMonoid M<VAR>inst✝ : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>x : M<VAR>hx : x ∈ K<VAR>n : ℕ<GOAL>(x ^ (n + 1))⁻¹ ∈ K
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : Nontrivial R<GOAL>IsAlgebraic R 1
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : Nontrivial R<GOAL>IsAlgebraic R ((algebraMap R A) 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = a ↔ a ∆ b = a ∆ ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = a ∆ ⊥ ↔ b = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G✝ H : SimpleGraph α<VAR>n✝ : ℕ<VAR>a b c : α<VAR>s : Finset α<VAR>G : SimpleGraph α<VAR>e : α ≃ β<VAR>n : ℕ<GOAL>(SimpleGraph.map e.toEmbedding G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G✝ H : SimpleGraph α<VAR>n : ℕ<VAR>a b c : α<VAR>s : Finset α<VAR>G : SimpleGraph α<VAR>e : α ≃ β<GOAL>(SimpleGraph.map e.toEmbedding G).cliqueSet 1 = map e.toEmbedding '' G.cliqueSet 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G✝ H : SimpleGraph α<VAR>n✝ : ℕ<VAR>a b c : α<VAR>s : Finset α<VAR>G : SimpleGraph α<VAR>e : α ≃ β<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>(SimpleGraph.map e.toEmbedding G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : ∀ (p : ℕ), n.factorization p ≤ 1<GOAL>Squarefree n
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : ∀ (p : ℕ), n.factorization p ≤ 1<GOAL>∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : ∀ (p : ℕ), n.factorization p ≤ 1<VAR>a : ℕ<GOAL>List.count a n.primeFactorsList ≤ 1
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : ∀ (p : ℕ), n.factorization p ≤ 1<VAR>a : ℕ<GOAL>n.factorization a ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a✝ : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>x : α × α<VAR>a : α<VAR>x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}<VAR>b : α × α<VAR>hb : b ∈ mulAntidiagonal hs ht a<GOAL>a ∈ s * t
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a✝ : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>x : α × α<VAR>a : α<VAR>x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}<VAR>b : α × α<VAR>hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a<GOAL>a ∈ s * t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedSemiring α<VAR>inst✝⁴ : LinearOrderedSemiring β<VAR>inst✝³ : FloorSemiring α<VAR>inst✝² : FloorSemiring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a✝ : α<VAR>b : β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<VAR>n : ℕ<GOAL>f a ≤ ↑n ↔ a ≤ ↑n
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<GOAL>G.maxDegree < Fintype.card V
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>v : V<VAR>hv : G.maxDegree = G.degree v<GOAL>G.maxDegree < Fintype.card V
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>v : V<VAR>hv : G.maxDegree = G.degree v<GOAL>G.degree v < Fintype.card V
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>X X' : C<VAR>Y : D<VAR>f : X ⟶ X'<VAR>g : X' ⟶ (rightAdjointOfEquiv e he).obj Y<GOAL>(e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>X X' : C<VAR>Y : D<VAR>f : X ⟶ X'<VAR>g : X' ⟶ (rightAdjointOfEquiv e he).obj Y<GOAL>f ≫ g = (e X Y) (F.map f ≫ (e X' Y).symm g)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>X : C<VAR>Y Y' : D<VAR>g : F.obj X ⟶ Y<VAR>h : Y ⟶ Y'<GOAL>(e X Y') (g ≫ h) = (e X Y) g ≫ (rightAdjointOfEquiv e he).map h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<GOAL>(fun a => ↑(condCDF ρ a) ↑r) =ᶠ[ae ρ.fst] fun a => (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>r : ℚ<GOAL>(fun a => ↑(stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), a)) ↑r) =ᶠ[ae ρ.fst] fun a => (preCDF ρ r a).toReal
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F G : LaxMonoidalFunctor C D<VAR>H K : LaxMonoidalFunctor D E<VAR>α : MonoidalNatTrans F G<VAR>β : MonoidalNatTrans H K<GOAL>K.ε ≫ K.map F.ε ≫ K.map (α.app (𝟙_ C)) = K.ε ≫ K.map G.ε
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F G : LaxMonoidalFunctor C D<VAR>H K : LaxMonoidalFunctor D E<VAR>α : MonoidalNatTrans F G<VAR>β : MonoidalNatTrans H K<VAR>X Y : C<GOAL>(β.app (F.obj X) ⊗ β.app (F.obj Y)) ≫ K.μ (F.obj X) (F.obj Y) ≫ K.map (F.μ X Y) ≫ K.map (α.app (X ⊗ Y)) = (β.app (F.obj X) ⊗ β.app (F.obj Y)) ≫ K.μ (F.obj X) (F.obj Y) ≫ K.map (α.app X ⊗ α.app Y) ≫ K.map (G.μ X Y)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)
<VAR>α : Type u_1<VAR>inst✝ : SemilatticeSup α<VAR>f : ℕ → α<VAR>a : α<GOAL>a ∈ upperBounds (Set.range ⇑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
<VAR>α : Type u_1<VAR>inst✝ : SemilatticeSup α<VAR>f : ℕ → α<VAR>a : α<GOAL>(∀ (i k : ℕ), k ≤ i → f k ≤ a) ↔ ∀ (i : ℕ), f i ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>((κ ⊗ₖ η) a) s = κ.compProdFun η a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>({ toFun := fun a => Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯, measurable' := ⋯ } a) s = κ.compProdFun η a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>IsSFiniteKernel κ ∧ IsSFiniteKernel η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>(Measure.ofMeasurable (fun s x => κ.compProdFun η a s) ⋯ ⋯) s = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>κ.compProdFun η a s = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝⁷ : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝⁶ : NonAssocSemiring S<VAR>inst✝⁵ inst✝⁴ : NonAssocSemiring T<VAR>s : Subsemiring R<VAR>σR : Type u_1<VAR>σS : Type u_2<VAR>inst✝³ : SetLike σR R<VAR>inst✝² : SetLike σS S<VAR>inst✝¹ : SubsemiringClass σR R<VAR>inst✝ : SubsemiringClass σS S<VAR>f : R →+* S<GOAL>↑f.rangeS = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑(μ.withDensityᵥ 0) s = ↑0 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, 0 ∂μ = ↑0 s
<VAR>a b k m n p a✝ : ℕ<GOAL>a✝ ∈ primeFactors 1 ↔ a✝ ∈ ∅
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>x✝ : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := -↑x, im := ↑y } * { re := ↑z, im := ↑w }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>x✝ : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑z, im := ↑w } * { re := -↑x, im := ↑y }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>x✝ : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } * { re := ↑z, im := ↑w }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>x✝ : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑z, im := ↑w } * { re := ↑x, im := -↑y }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>({ re := -↑x, im := ↑y } * { re := -↑z, im := ↑w }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>{ re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>({ re := -↑x, im := ↑y } * { re := ↑z, im := -↑w }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>{ re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } * { re := -↑z, im := ↑w }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>{ re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } * { re := ↑z, im := -↑w }).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>hb✝ : b.Nonneg<VAR>x y z w : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>{ re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>S : Sieve X<VAR>s : Cocone S.arrows.diagram<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>hf₁ : S.arrows f₁<VAR>hf₂ : S.arrows f₂<VAR>hgf : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>(yoneda.obj s.pt).map g₁.op (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) = (yoneda.obj s.pt).map g₂.op (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>S : Sieve X<VAR>s : Cocone S.arrows.diagram<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>hf₁ : S.arrows f₁<VAR>hf₂ : S.arrows f₂<VAR>hgf : g₁ ≫ f₁ = g₂ ≫ f₂<VAR>Hs : ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y), S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f<GOAL>(yoneda.obj s.pt).map g₁.op (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) = (yoneda.obj s.pt).map g₂.op (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>S : Sieve X<VAR>s : Cocone S.arrows.diagram<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>hf₁ : S.arrows f₁<VAR>hf₂ : S.arrows f₂<VAR>hgf : g₁ ≫ f₁ = g₂ ≫ f₂<VAR>Hs : ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y), S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f<GOAL>g₁ ≫ S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁ = g₂ ≫ S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>S : Sieve X<VAR>s : Cocone S.arrows.diagram<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>hf₁ : S.arrows f₁<VAR>hf₂ : S.arrows f₂<VAR>hgf : g₁ ≫ f₁ = g₂ ≫ f₂<VAR>Hs : ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y), S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f<GOAL>g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>S : Sieve X<VAR>s : Cocone S.arrows.diagram<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>hf₁ : S.arrows f₁<VAR>hf₂ : S.arrows f₂<VAR>hgf : g₁ ≫ f₁ = g₂ ≫ f₂<VAR>Hs : ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y), S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f<VAR>hgf₁ : S.arrows (g₁ ≫ f₁)<GOAL>g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>S : Sieve X<VAR>s : Cocone S.arrows.diagram<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>hf₁ : S.arrows f₁<VAR>hf₂ : S.arrows f₂<VAR>hgf : g₁ ≫ f₁ = g₂ ≫ f₂<VAR>Hs : ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y), S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f<VAR>hgf₁ : S.arrows (g₁ ≫ f₁)<VAR>hgf₂ : S.arrows (g₂ ≫ f₂)<GOAL>g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<GOAL>‖(adjoint A).comp A‖ = ‖A‖ * ‖A‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<GOAL>‖(adjoint A).comp A‖ ≤ ‖A‖ * ‖A‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<GOAL>‖A‖ * ‖A‖ ≤ ‖(adjoint A).comp A‖