ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f : E →ₗ[ℝ] E<VAR>hf : LinearMap.det f ≠ 0<VAR>s : Set E<GOAL>(ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ) s = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, IsRatStieltjesPoint f (a, t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>t : β<VAR>ht_top : Tendsto (f (a, t)) atTop (𝓝 1)<VAR>ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)<VAR>ht_iInf : ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q<VAR>h_mono : Monotone (f (a, t))<GOAL>IsRatStieltjesPoint f (a, t)
<VAR>f : ℕ →. ℕ<VAR>h : _root_.Partrec fun v => f v.head<VAR>v : ℕ<GOAL>f (ofFn fun i => id v).head = f v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>this✝¹ : MeasurableSpace (β × β) := borel (β × β)<VAR>this✝ : BorelSpace (β × β)<GOAL>MeasurableSet {a | f a ≤ g a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>s.encard = ↑s.toFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>inst✝ : Fintype ↑s<VAR>h : s.Finite<GOAL>s.encard = ↑s.toFinset.card
<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>a b c : α<GOAL>b < a⁻¹ * c ↔ a * b < c
<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>a b c : α<GOAL>a * b < a * (a⁻¹ * c) ↔ a * b < c
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t K : Set X<VAR>hK : IsCompact K<VAR>l : Filter X<GOAL>l ⊓ 𝓝ˢ K = ⨆ x ∈ K, l ⊓ 𝓝 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>x : α<GOAL>insert (f x) (f '' {x}ᶜ) = range f
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>x✝ : CharacterModule (A ⊗[R] B)<VAR>z : A ⊗[R] B<GOAL>((uncurry ∘ₗ curry) x✝) z = (LinearMap.id x✝) z
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>δ : ℝ<VAR>E : Set X<VAR>h : Bornology.IsBounded E<GOAL>Bornology.IsBounded (thickening δ E)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>δ : ℝ<VAR>h : Bornology.IsBounded ∅<GOAL>Bornology.IsBounded (thickening δ ∅)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>δ : ℝ<VAR>E : Set X<VAR>h : Bornology.IsBounded E<VAR>x : X<VAR>hx : x ∈ E<GOAL>Bornology.IsBounded (thickening δ E)
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ
<VAR>z τ : ℂ<GOAL>∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ) c) (-z) τ = jacobiTheta₂ z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>jacobiTheta₂_term ((Equiv.neg ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>z : M ⧸ torsion R M<VAR>x : M<VAR>x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)<VAR>a : ↥R⁰<VAR>hax : a • Quotient.mk'' x = 0<GOAL>Quotient.mk'' x ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>z : M ⧸ torsion R M<VAR>x : M<VAR>x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)<VAR>a : ↥R⁰<VAR>hax : a • x ∈ torsion R M<GOAL>Quotient.mk'' x ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>z : M ⧸ torsion R M<VAR>x : M<VAR>x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)<VAR>a : ↥R⁰<VAR>hax : a • x ∈ torsion R M<GOAL>x ∈ torsion R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>z : M ⧸ torsion R M<VAR>x : M<VAR>x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)<VAR>a b : ↥R⁰<VAR>h : b • a • x = 0<GOAL>x ∈ torsion R M
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<GOAL>(p * X).coeff (n + 1) = p.coeff n
<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>s t u : Set α<VAR>hf : InjOn f u<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>f '' (s ∩ t) = f '' s ∩ f '' t
<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>s t u : Set α<VAR>hf : InjOn f u<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>f '' s ∩ f '' t ⊆ f '' (s ∩ t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : MulZeroOneClass α<VAR>inst✝² : MulZeroOneClass β<VAR>inst✝¹ : MulZeroOneClass γ<VAR>inst✝ : MulZeroOneClass δ<VAR>f✝ g✝ f g : α →*₀o β<VAR>h : f.toOrderMonoidHom = g.toOrderMonoidHom<GOAL>∀ (a : α), f a = g a
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-y ⧏ x ↔ -x ⧏ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MulZeroOneClass A<VAR>inst✝¹ : FunLike F ℕ A<VAR>inst✝ : MonoidWithZeroHomClass F ℕ A<VAR>f g : F<VAR>h_pos : ∀ {n : ℕ}, 0 < n → f n = g n<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MulZeroOneClass A<VAR>inst✝¹ : FunLike F ℕ A<VAR>inst✝ : MonoidWithZeroHomClass F ℕ A<VAR>f g : F<VAR>h_pos : ∀ {n : ℕ}, 0 < n → f n = g n<GOAL>∀ (x : ℕ), f x = g x
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>l : List ℕ<GOAL>commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l)
<VAR>r : ℝ<GOAL>0 ≤ r.sign * r
<VAR>r : ℝ<VAR>hn : r < 0<GOAL>0 ≤ r.sign * r
<VAR>r : ℝ<VAR>hp : 0 < r<GOAL>0 ≤ r.sign * r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>a ^ (m - n) * a ^ n = a ^ m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M : Matrix n n R<VAR>i j : n<GOAL>(fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Injective (preimage f) ↔ Surjective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Injective (preimage f)<VAR>y : β<GOAL>∃ a, f a = y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Injective (preimage f)<VAR>y : β<VAR>x : α<VAR>hx : x ∈ f ⁻¹' {y}<GOAL>∃ a, f a = y
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>ha : a ≠ 0<GOAL>(a • p).roots = p.roots
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s t : Set X<VAR>x : ↑s<GOAL>𝓝[Subtype.val ⁻¹' t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r✝ s r : ℝ<VAR>hr : r ≠ 0<GOAL>IsOpen (closedBall x r)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>a b : α × β<GOAL>a < b → Prod.map f g a < Prod.map f g b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>a b : α × β<GOAL>a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 → (Prod.map f g a).1 < (Prod.map f g b).1 ∧ (Prod.map f g a).2 ≤ (Prod.map f g b).2 ∨ (Prod.map f g a).1 ≤ (Prod.map f g b).1 ∧ (Prod.map f g a).2 < (Prod.map f g b).2
<VAR>f : ℝ → ℝ<VAR>f' : ℝ<VAR>s : Set ℝ<VAR>a b : ℝ<GOAL>1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in 𝓝[>] a, x ∈ s
<VAR>f : ℝ → ℝ<VAR>f' : ℝ<VAR>s : Set ℝ<VAR>a b : ℝ<GOAL>(∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Ioo x y)<VAR>h : ∀ w ∈ Ioo x y, deriv f w ≠ 0<GOAL>∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Ioo x y)<VAR>h : ∀ w ∈ Ioo x y, deriv f w ≠ 0<VAR>A : DifferentiableOn ℝ f (Ioo x y)<GOAL>∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Ioo x y)<VAR>h : ∀ w ∈ Ioo x y, deriv f w ≠ 0<VAR>A : DifferentiableOn ℝ f (Ioo x y)<VAR>a : ℝ<VAR>ha : deriv f a = (f y - f x) / (y - x)<VAR>hxa : x < a<VAR>hay : a < y<GOAL>∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Ioo x y)<VAR>h : ∀ w ∈ Ioo x y, deriv f w ≠ 0<VAR>A : DifferentiableOn ℝ f (Ioo x y)<VAR>a : ℝ<VAR>ha : deriv f a = (f y - f x) / (y - x)<VAR>hxa : x < a<VAR>hay : a < y<VAR>b : ℝ<VAR>hxb : x < b<VAR>hba : b < a<GOAL>∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<GOAL>compactOpen = ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<GOAL>⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen ≤ compactOpen
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set Y<VAR>hU : U ∈ {U | IsOpen U}<GOAL>IsOpen {f | MapsTo (⇑f) K U}
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set Y<VAR>hU : U ∈ {U | IsOpen U}<GOAL>{f | MapsTo (⇑f) K U} = restrict K ⁻¹' {f | MapsTo (⇑f) univ U}
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P✝ : PrelocalPredicate T<VAR>P : LocalPredicate T<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))<VAR>sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf<VAR>sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)<VAR>sf'_comp : (X.presheafToTypes T).IsCompatible U sf'<GOAL>∃! s, (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P✝ : PrelocalPredicate T<VAR>P : LocalPredicate T<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))<VAR>sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf<VAR>sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)<VAR>sf'_comp : (X.presheafToTypes T).IsCompatible U sf'<VAR>gl : (forget (Type v)).obj ((X.sheafToTypes T).val.obj (op (iSup U)))<VAR>gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl<VAR>gl_uniq : ∀ (y : (forget (Type v)).obj ((X.sheafToTypes T).val.obj (op (iSup U)))), (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl<GOAL>∃! s, (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>↑s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>↑s i - ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>∀ (i_1 : ℕ), MeasurableSet (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>Pairwise (Disjoint on fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∃ n, restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>k : ℕ := Nat.find hn<VAR>hk₂ : restrict s (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l ⊆ i
<VAR>R : Type u_1<VAR>inst✝¹ : PseudoMetricSpace R<VAR>inst✝ : Sub R<VAR>K : ℝ≥0<VAR>lip : LipschitzWith K fun p => p.1 - p.2<VAR>s t : Set R<VAR>s_bdd : Bornology.IsBounded s<VAR>t_bdd : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s - t)
<VAR>R : Type u_1<VAR>inst✝¹ : PseudoMetricSpace R<VAR>inst✝ : Sub R<VAR>K : ℝ≥0<VAR>lip : LipschitzWith K fun p => p.1 - p.2<VAR>s t : Set R<VAR>s_bdd : Bornology.IsBounded s<VAR>t_bdd : Bornology.IsBounded t<VAR>bdd : Bornology.IsBounded (s ×ˢ t)<GOAL>Bornology.IsBounded (s - t)
<VAR>R : Type u_1<VAR>inst✝¹ : PseudoMetricSpace R<VAR>inst✝ : Sub R<VAR>K : ℝ≥0<VAR>lip : LipschitzWith K fun p => p.1 - p.2<VAR>s t : Set R<VAR>s_bdd : Bornology.IsBounded s<VAR>t_bdd : Bornology.IsBounded t<VAR>bdd : Bornology.IsBounded (s ×ˢ t)<GOAL>s - t = (fun p => p.1 - p.2) '' s ×ˢ t
<VAR>R : Type u_1<VAR>inst✝¹ : PseudoMetricSpace R<VAR>inst✝ : Sub R<VAR>K : ℝ≥0<VAR>lip : LipschitzWith K fun p => p.1 - p.2<VAR>s t : Set R<VAR>s_bdd : Bornology.IsBounded s<VAR>t_bdd : Bornology.IsBounded t<VAR>bdd : Bornology.IsBounded (s ×ˢ t)<VAR>p : R<GOAL>p ∈ s - t ↔ p ∈ (fun p => p.1 - p.2) '' s ×ˢ t
<VAR>R : Type u_1<VAR>inst✝¹ : PseudoMetricSpace R<VAR>inst✝ : Sub R<VAR>K : ℝ≥0<VAR>lip : LipschitzWith K fun p => p.1 - p.2<VAR>s t : Set R<VAR>s_bdd : Bornology.IsBounded s<VAR>t_bdd : Bornology.IsBounded t<VAR>bdd : Bornology.IsBounded (s ×ˢ t)<VAR>p : R<GOAL>p ∈ s - t ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q : ℚ<VAR>x y : α<GOAL>inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q : ℚ<VAR>x y : α<GOAL>sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>M : o → Matrix m n α<VAR>N : o → Matrix n p α<VAR>i : m<VAR>k : o<VAR>j : p<VAR>k' : o<GOAL>blockDiagonal (fun k => M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>M : o → Matrix m n α<VAR>N : o → Matrix n p α<VAR>i : m<VAR>k : o<VAR>j : p<VAR>k' : o<GOAL>(if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0) = ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>S : Set α<VAR>V : Set (α × α)<VAR>x_in : x ∈ S<VAR>V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)<GOAL>ball x V ∈ 𝓝[S] x