ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : NormalSpace X<VAR>inst✝³ : ParacompactSpace X<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>t : X → Set E<VAR>ht : ∀ (x : X), Convex ℝ (t x)<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<VAR>g : X → X → E<VAR>hgc : ∀ (x : X), ContinuousOn (g x) (U x)<VAR>hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y<VAR>f : PartitionOfUnity X X<VAR>hf : f.IsSubordinate fun x => interior (U x)<VAR>x i : X<VAR>hi : (f i) x ≠ 0<GOAL>x ∈ U i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Icc 0 1<GOAL>x + t • (y - x) ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Icc 0 1<GOAL>t • (y - x) + x ∈ s
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid N✝<VAR>N : Submonoid M<GOAL>FG ↥N ↔ N.FG
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid N✝<VAR>N : Submonoid M<GOAL>FG ↥N ↔ (Submonoid.map N.subtype ⊤).FG
<VAR>α : Type u_1<VAR>a : Lists α<VAR>l0 l₂ : Lists' α true<VAR>a✝ a'✝ : Lists α<VAR>e : a✝ ~ a'✝<VAR>h : a ∈ (a✝.snd.cons' l0).toList<VAR>m : a'✝ ∈ l₂.toList<VAR>s : l0.Subset l₂<GOAL>a ∈ l₂
<VAR>α : Type u_1<VAR>a : Lists α<VAR>l0 l₂ : Lists' α true<VAR>a✝ a'✝ : Lists α<VAR>e : a✝ ~ a'✝<VAR>m : a'✝ ∈ l₂.toList<VAR>s : l0.Subset l₂<VAR>h : a = a✝ ∨ a ∈ l0.toList<GOAL>a ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<GOAL>s.toJordanDecomposition.toSignedMeasure = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i<VAR>hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ<VAR>hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂<VAR>hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃<GOAL>s.toJordanDecomposition.toSignedMeasure = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i<VAR>hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ<VAR>hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂<VAR>hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃<VAR>k : Set α<VAR>hk : MeasurableSet k<GOAL>↑((s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure) k = ↑s k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i<VAR>hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ<VAR>hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂<VAR>hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃<VAR>k : Set α<VAR>hk : MeasurableSet k<GOAL>(↑⟨↑s (i ∩ k), ⋯⟩).toReal - (↑⟨-↑s (iᶜ ∩ k), ⋯⟩).toReal = ↑s k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i<VAR>hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ<VAR>hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂<VAR>hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃<VAR>k : Set α<VAR>hk : MeasurableSet k<GOAL>↑s (i ∩ k) + ↑s (iᶜ ∩ k) = ↑s k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i<VAR>hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ<VAR>hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂<VAR>hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃<VAR>k : Set α<VAR>hk : MeasurableSet k<GOAL>Disjoint (i ∩ k) (iᶜ ∩ k)
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>∃ t, s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<VAR>this : 2 * s.card ≤ Fintype.card α<GOAL>∃ t, s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<VAR>this : s.card ≤ Fintype.card α / 2<GOAL>∃ t, s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s✝ : Finset α<VAR>this : s✝.card ≤ Fintype.card α / 2<VAR>s : Finset α<VAR>ih : ∀ {t₂ : Finset α}, t₂.card ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting<VAR>_hcard : s.card ≤ Fintype.card α / 2<VAR>hs : (↑s).Intersecting<VAR>t : Finset α<VAR>ht : (↑t).Intersecting<VAR>hst : s ⊆ t ∧ s ≠ t<GOAL>∃ t, s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s✝ : Finset α<VAR>this : s✝.card ≤ Fintype.card α / 2<VAR>s : Finset α<VAR>ih : ∀ {t₂ : Finset α}, t₂.card ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting<VAR>_hcard : s.card ≤ Fintype.card α / 2<VAR>hs : (↑s).Intersecting<VAR>t : Finset α<VAR>ht : (↑t).Intersecting<VAR>hst : s ⊆ t ∧ s ≠ t<GOAL>t.card ≤ Fintype.card α / 2
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s✝ : Finset α<VAR>this : s✝.card ≤ Fintype.card α / 2<VAR>s : Finset α<VAR>ih : ∀ {t₂ : Finset α}, t₂.card ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting<VAR>_hcard : s.card ≤ Fintype.card α / 2<VAR>hs : (↑s).Intersecting<VAR>t : Finset α<VAR>ht : (↑t).Intersecting<VAR>hst : s ⊆ t ∧ s ≠ t<GOAL>2 * t.card ≤ Fintype.card α
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h✝ : IsRelPrime x y<VAR>z : R<VAR>h : IsRelPrime x y<GOAL>IsRelPrime (x + y * z + y * -z) y
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>integer : ∏ i ∈ n.divisors, cyclotomic i ℤ = X ^ n - 1<GOAL>∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : OplaxNatTrans F G<VAR>θ : OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g h : a ⟶ b<VAR>β : g ⟶ h<GOAL>f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ θ.naturality h = f ◁ θ.naturality g ≫ f ◁ θ.app a ◁ H.map₂ β
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a⁻¹ < b ↔ b⁻¹ < a
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<GOAL>(map ι f) x = -x ↔ LinearMap.det ↑f < 0
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<VAR>h✝ : IsEmpty ι<GOAL>(map ι f) x = -x ↔ LinearMap.det ↑f < 0
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<VAR>h✝ : Nonempty ι<GOAL>(map ι f) x = -x ↔ LinearMap.det ↑f < 0
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<VAR>h✝ : Nonempty ι<VAR>H : 0 < finrank R M<GOAL>(map ι f) x = -x ↔ LinearMap.det ↑f < 0
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<VAR>h✝ : Nonempty ι<VAR>H : 0 < finrank R M<VAR>this : FiniteDimensional R M<GOAL>(map ι f) x = -x ↔ LinearMap.det ↑f < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>inst✝¹ : One F<VAR>inst✝ : NormOneClass F<VAR>c : E<VAR>l : Filter α<GOAL>IsBigOWith ‖c‖ l (fun _x => c) fun _x => 1
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>hg : Injective ⇑g<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<GOAL>(lift hg) (mk' K x y) = g x / g ↑y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Cardinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>lift.{u, u} #ι < c
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹ : Monoid M<VAR>a : M<VAR>S : Submonoid M<VAR>inst✝ : Fintype ↥S<VAR>h : card ↥S ≤ 1<VAR>x : M<VAR>hx : x ∈ S<GOAL>x = 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>U : Type u_2<VAR>inst✝¹ : CommRing U<VAR>inst✝ : Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>e : T ≃ₐ[R] U<VAR>a : S<GOAL>(h.aequiv (h'.ofEquiv e)) a = ((h.aequiv h').trans e) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>inst✝² : Fintype ↑(G.neighborSet x.1)<VAR>inst✝¹ : Fintype ↑(H.neighborSet x.2)<VAR>inst✝ : Fintype ↑((G □ H).neighborSet x)<GOAL>(G □ H).degree x = G.degree x.1 + H.degree x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>inst✝² : Fintype ↑(G.neighborSet x.1)<VAR>inst✝¹ : Fintype ↑(H.neighborSet x.2)<VAR>inst✝ : Fintype ↑((G □ H).neighborSet x)<GOAL>(G.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card = (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>i j j' : C<VAR>f : i ⟶ j<VAR>f' : i ⟶ j'<VAR>K : C<VAR>G : j ⟶ K<VAR>G' : j' ⟶ K<VAR>h✝ : True<VAR>k : C<VAR>e : K ⟶ k<VAR>he : (f ≫ G) ≫ e = (f' ≫ G') ≫ e<GOAL>f ≫ G ≫ e = f' ≫ G' ≫ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>ι' : Type u_8<VAR>μ : ι → ι' → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum fun n => sum (μ n)) s = (sum fun m => sum fun n => μ n m) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>ι' : Type u_8<VAR>μ : ι → ι' → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∑' (i : ι) (i_1 : ι'), (μ i i_1) s = ∑' (i : ι') (i_1 : ι), (μ i_1 i) s
<VAR>R : Type u<VAR>ι : Type v<VAR>n : ℕ<VAR>M✝ : Fin n.succ → Type w<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>M₄ : Type w₄<VAR>M : Type u_1<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ContinuousMul R<VAR>inst✝ : ContinuousSMul R M<VAR>x✝ : ι → R<GOAL>(ContinuousMultilinearMap.mkPiRing R ι 0) x✝ = 0 x✝
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>dual A K I = dual A K 1 * I⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>dual A K I ≤ dual A K 1 * I⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>dual A K 1 * I⁻¹ ≤ dual A K I
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>F : C ⥤ B<VAR>R : A ⥤ B<VAR>F' : C ⥤ A<VAR>adj₁ : F ⊣ U<VAR>adj₂ : F' ⊣ R ⋙ U<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (X : B) → RegularEpi (adj₁.counit.app X)<VAR>Y : A<VAR>X : B<VAR>f : F'.obj (U.obj X) ⟶ Y<GOAL>F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f ↔ U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>F : C ⥤ B<VAR>R : A ⥤ B<VAR>F' : C ⥤ A<VAR>adj₁ : F ⊣ U<VAR>adj₂ : F' ⊣ R ⋙ U<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (X : B) → RegularEpi (adj₁.counit.app X)<VAR>Y : A<VAR>X : B<VAR>f : F'.obj (U.obj X) ⟶ Y<GOAL>U.map (F.map (adj₂.unit.app (U.toPrefunctor.1 X)) ≫ F.map (U.map (R.map f)) ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ adj₂.unit.app (U.obj ((𝟭 B).obj X)) ≫ (R ⋙ U).map f ↔ U.map (F.map (adj₂.unit.app (U.obj X)) ≫ F.map ((R ⋙ U).map f) ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ adj₂.unit.app (U.obj X) ≫ (R ⋙ U).map f
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>F : C ⥤ B<VAR>R : A ⥤ B<VAR>F' : C ⥤ A<VAR>adj₁ : F ⊣ U<VAR>adj₂ : F' ⊣ R ⋙ U<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (X : B) → RegularEpi (adj₁.counit.app X)<VAR>Y : A<VAR>X : B<VAR>g : U.obj X ⟶ U.obj (R.obj Y)<GOAL>U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g ↔ F.map (U.map (adj₁.counit.app X)) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g = adj₁.counit.app (F.obj (U.obj X)) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>F : C ⥤ B<VAR>R : A ⥤ B<VAR>F' : C ⥤ A<VAR>adj₁ : F ⊣ U<VAR>adj₂ : F' ⊣ R ⋙ U<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (X : B) → RegularEpi (adj₁.counit.app X)<VAR>Y : A<VAR>X : B<VAR>g : U.obj X ⟶ U.obj (R.obj Y)<GOAL>adj₁.counit.app (F.obj (U.obj X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) = F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app ((𝟭 B).obj (R.obj Y)) ↔ F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) = adj₁.counit.app (F.obj (U.obj X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y)
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>∑' (n : ℕ), { toFun := fun n => χ ↑n * ↑n ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } n = ∑' (n : ℕ), if n = 0 then 0 else χ ↑n / ↑n ^ s
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>{ toFun := fun n => χ ↑n * ↑n ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } n = if n = 0 then 0 else χ ↑n / ↑n ^ s
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>{ toFun := fun n => χ ↑n * ↑n ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } 0 = if 0 = 0 then 0 else χ ↑0 / ↑0 ^ s
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>{ toFun := fun n => χ ↑n * ↑n ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } n = if n = 0 then 0 else χ ↑n / ↑n ^ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x - y) (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x + -y) (s + -t)
<VAR>X : Type u_2<VAR>Y : Sort u_3<VAR>Z : Type u_1<VAR>f : X → Y<VAR>g : Z → Y<VAR>p₁ p₂ : Pullback f g<VAR>he : (p₁, p₂).1.snd = (p₁, p₂).2.snd<GOAL>⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd
<VAR>X : Type u_2<VAR>Y : Sort u_3<VAR>Z : Type u_1<VAR>f : X → Y<VAR>g : Z → Y<VAR>p₁ p₂ : Pullback f g<VAR>he : (p₁, p₂).1.snd = (p₁, p₂).2.snd<GOAL>⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ (↑(fst ⟨(p₁, p₂), he⟩)).1 = (↑(snd ⟨(p₁, p₂), he⟩)).1 ∧ (↑(fst ⟨(p₁, p₂), he⟩)).2 = (↑(snd ⟨(p₁, p₂), he⟩)).2
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>ht : ∀ (x : M), Convex ℝ (t x)<VAR>U : M → Set M<VAR>hU : ∀ (x : M), U x ∈ 𝓝 x<VAR>g : M → M → F<VAR>hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) n (g x) (U x)<VAR>hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y<GOAL>∃ g, ∀ (x : M), g x ∈ t x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>ht : ∀ (x : M), Convex ℝ (t x)<VAR>U : M → Set M<VAR>hU : ∀ (x : M), U x ∈ 𝓝 x<VAR>g : M → M → F<VAR>hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) n (g x) (U x)<VAR>hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => interior (U x)<GOAL>∃ g, ∀ (x : M), g x ∈ t x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>ht : ∀ (x : M), Convex ℝ (t x)<VAR>U : M → Set M<VAR>hU : ∀ (x : M), U x ∈ 𝓝 x<VAR>g : M → M → F<VAR>hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) n (g x) (U x)<VAR>hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => interior (U x)<VAR>x i : M<VAR>hi : (f i) x ≠ 0<GOAL>x ∈ U i
<VAR>α β : Type u<VAR>c✝ : Cardinal.{?u.245881}<VAR>b c a : Cardinal.{u}<VAR>h : c < b<GOAL>a ^ c ≤ a ^< b
<VAR>α β : Type u<VAR>c✝ : Cardinal.{?u.245881}<VAR>b c a : Cardinal.{u}<VAR>h : c < b<GOAL>BddAbove (range fun y => a ^ ↑y)
<VAR>α β : Type u<VAR>c✝ : Cardinal.{?u.245881}<VAR>b c a : Cardinal.{u}<VAR>h : c < b<GOAL>BddAbove (HPow.hPow a '' Iio b)