ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type ?u.54871<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁶ : LinearOrder ι✝<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Free R M<VAR>Q : QuadraticMap R M N<VAR>ι : Type u_2<VAR>b : Basis ι R M<GOAL>∃ a, a.toQuadraticMap = Q
<VAR>ι✝ : Type ?u.54871<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁶ : LinearOrder ι✝<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Free R M<VAR>Q : QuadraticMap R M N<VAR>ι : Type u_2<VAR>b : Basis ι R M<VAR>this : LinearOrder ι := IsWellOrder.linearOrder WellOrderingRel<GOAL>∃ a, a.toQuadraticMap = Q
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g : NormedAddGroupHom V₁ V₂<VAR>f : V₁ →+ V₂<VAR>C : ℝ<VAR>h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖<VAR>x : V₁<GOAL>C ≤ max C 0
<VAR>x✝ y✝ x y : ℂ<GOAL>sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasStrictDerivAt f^[n] (f' ^ n) x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<VAR>this : HasStrictFDerivAt f^[n] (smulRight 1 f' ^ n) x<GOAL>HasStrictDerivAt f^[n] (f' ^ n) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u✝ : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b x : α<VAR>h : s.OrdConnected<VAR>u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u✝ : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b x : α<VAR>h : s.OrdConnected<VAR>u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y<VAR>huopen : IsOpen u<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u✝ : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b x : α<VAR>h : s.OrdConnected<VAR>u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y<VAR>huopen : IsOpen u<VAR>humeas : MeasurableSet u<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u✝ : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b x : α<VAR>h : s.OrdConnected<VAR>u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y<VAR>huopen : IsOpen u<VAR>humeas : MeasurableSet u<VAR>hfinite : (s \ u).Finite<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u✝ : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b x : α<VAR>h : s.OrdConnected<VAR>u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y<VAR>huopen : IsOpen u<VAR>humeas : MeasurableSet u<VAR>hfinite : (s \ u).Finite<VAR>this : u ⊆ s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u✝ : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b x : α<VAR>h : s.OrdConnected<VAR>u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y<VAR>huopen : IsOpen u<VAR>humeas : MeasurableSet u<VAR>hfinite : (s \ u).Finite<VAR>this : u ⊆ s<GOAL>MeasurableSet (u ∪ s \ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 ((κ a) univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 ((κ a) univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>Tendsto (fun m => ((κ a) (univ ×ˢ seq m)).toReal) atTop (𝓝 ((κ a) univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)<GOAL>Tendsto (fun m => ((κ a) (univ ×ˢ seq m)).toReal) atTop (𝓝 ((κ a) univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>{a | a ≠ ⊤} ∈ 𝓝 ((κ a) univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)<GOAL>Tendsto (fun m => (κ a) (univ ×ˢ seq m)) atTop (𝓝 ((κ a) univ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)<VAR>h : Tendsto (⇑(κ a) ∘ fun m => univ ×ˢ seq m) atTop (𝓝 ((κ a) (⋃ n, univ ×ˢ seq n)))<GOAL>Tendsto (fun m => (κ a) (univ ×ˢ seq m)) atTop (𝓝 ((κ a) univ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)<GOAL>Monotone fun m => univ ×ˢ seq m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)<VAR>h : Tendsto (⇑(κ a) ∘ fun m => univ ×ˢ seq m) atTop (𝓝 ((κ a) (⋃ n, univ ×ˢ seq n)))<GOAL>univ = ⋃ n, univ ×ˢ seq n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)<VAR>h : Tendsto (⇑(κ a) ∘ fun m => univ ×ˢ seq m) atTop (𝓝 ((κ a) (⋃ n, univ ×ˢ seq n)))<GOAL>univ = univ ×ˢ univ
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>m n : ℕ<GOAL>iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsComplex<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsComplex<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B<VAR>this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w => if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsComplex<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B<VAR>this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w => if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)<VAR>a : 𝓞 K<VAR>h_nz : a ≠ 0<VAR>h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)<VAR>h_le₀ : |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧ |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)
<VAR>C : Type u_1<VAR>D : Type ?u.35289<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{?u.35297, ?u.35289} D<VAR>K : Coverage C<VAR>X : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>hS : K.Saturate X S<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : S.arrows g<GOAL>K.Saturate Y (Sieve.pullback g T)
<VAR>C : Type u_1<VAR>D : Type ?u.35289<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{?u.35297, ?u.35289} D<VAR>K : Coverage C<VAR>X : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>hS : K.Saturate X S<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : S.arrows g<GOAL>K.Saturate Y ⊤
<VAR>C : Type u_1<VAR>D : Type ?u.35289<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{?u.35297, ?u.35289} D<VAR>K : Coverage C<VAR>X : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>hS : K.Saturate X S<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : S.arrows g<GOAL>S.arrows g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<VAR>I : PrimeSpectrum R<GOAL>I ∈ (zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<VAR>I : PrimeSpectrum R<GOAL>f ∉ ↑I.asIdeal ↔ f ∉ I.asIdeal
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<GOAL>#β ≤ #↑(range f)
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<GOAL>#β ≤ #↑(range f)
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<VAR>h : ¬#β ≤ #↑(range f)<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<VAR>h : #↑(range f) < #β<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<VAR>h : #↑(range f) < #β<VAR>u : ∀ (b : β), ∃ a, b ∈ f a := fun b => Eq.mp (Eq.trans Mathlib.Order.SetNotation._auxLemma.3 (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.6))) (Eq.ge w (mem_univ b))<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<VAR>h : #↑(range f) < #β<VAR>u : ∀ (b : β), ∃ a, b ∈ f a := fun b => Eq.mp (Eq.trans Mathlib.Order.SetNotation._auxLemma.3 (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.6))) (Eq.ge w (mem_univ b))<VAR>u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<VAR>h : #↑(range f) < #β<VAR>u : ∀ (b : β), ∃ a, b ∈ f a := fun b => Eq.mp (Eq.trans Mathlib.Order.SetNotation._auxLemma.3 (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.6))) (Eq.ge w (mem_univ b))<VAR>u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩<VAR>v' : ∀ (a : α), u' ⁻¹' {⟨f a, ⋯⟩} ≤ ↑(f a)<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Infinite β<VAR>f : α → Finset β<VAR>w : ⋃ a, ↑(f a) = ⊤<VAR>k : Infinite ↑(range f)<VAR>h : #↑(range f) < #β<VAR>u : ∀ (b : β), ∃ a, b ∈ f a := fun b => Eq.mp (Eq.trans Mathlib.Order.SetNotation._auxLemma.3 (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.6))) (Eq.ge w (mem_univ b))<VAR>u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩<VAR>v' : ∀ (a : α), u' ⁻¹' {⟨f a, ⋯⟩} ≤ ↑(f a)<VAR>a : α<VAR>p : Infinite ↑(u' ⁻¹' {⟨f a, ⋯⟩})<GOAL>False
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : Part α →o Part α<VAR>hc : Continuous f<VAR>x✝ : Chain (Unit → Part α)<GOAL>f (Part.ωSup (x✝.map (Pi.evalOrderHom PUnit.unit))) = Part.ωSup ((x✝.map (toUnitMono f)).map (Pi.evalOrderHom PUnit.unit))
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : Part α →o Part α<VAR>hc : Continuous f<VAR>x✝ : Chain (Unit → Part α)<GOAL>ωSup (x✝.map (f.comp (Pi.evalOrderHom PUnit.unit))) = Part.ωSup (x✝.map (f.comp (Pi.evalOrderHom PUnit.unit)))
<VAR>x y : ℝ*<GOAL>x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → (ι → ℝ) → E<VAR>g : α → F<VAR>h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)<GOAL>HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>α : Type u_1<VAR>f : α → (ι → ℝ) → E<VAR>g : α → F<VAR>h : ∀ i ∈ ∅, HasIntegral I l (f i) vol (g i)<GOAL>HasIntegral I l (fun x => ∑ i ∈ ∅, f i x) vol (∑ i ∈ ∅, g i)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>α : Type u_1<VAR>f : α → (ι → ℝ) → E<VAR>g : α → F<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)<VAR>h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)<GOAL>HasIntegral I l (fun x => ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a s, g i)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>α : Type u_1<VAR>f : α → (ι → ℝ) → E<VAR>g : α → F<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)<VAR>h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)<GOAL>HasIntegral I l (fun x => f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>α : Type u_1<VAR>f : α → (ι → ℝ) → E<VAR>g : α → F<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)<VAR>h : HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)<GOAL>HasIntegral I l (fun x => f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)
<VAR>a b : ℤ<GOAL>IsCoprime a b ↔ a.natAbs.Coprime b.natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : β →ₛ γ<VAR>g : α → β<VAR>hgm : Measurable g<GOAL>↑(f.comp g hgm).range ⊆ ↑f.range
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<GOAL>DevosMulRel x y ↔ (x.1 * x.2).card < (y.1 * y.2).card ∨ (x.1 * x.2).card = (y.1 * y.2).card ∧ y.1.card + y.2.card < x.1.card + x.2.card ∨ (x.1 * x.2).card = (y.1 * y.2).card ∧ x.1.card + x.2.card = y.1.card + y.2.card ∧ x.1.card < y.1.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a✝ b✝ c d : α<VAR>p : β → β → Prop<VAR>a b : α<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → ReflTransGen p (f a) (f b)<VAR>hab : ReflTransGen r a b<GOAL>ReflTransGen p (f a) (f b)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f a - f (∅.piecewise b a) = ∑ i ∈ ∅, f fun j => if j ∈ ∅ → j < i then a j else if i = j then a j - b j else b j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b : (i : ι) → M₁ i<VAR>s✝ : Finset ι<VAR>k : ι<VAR>s : Finset ι<VAR>hk : ∀ x ∈ s, k < x<VAR>ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j<GOAL>f a - f ((insert k s).piecewise b a) = ∑ i ∈ insert k s, f fun j => if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b : (i : ι) → M₁ i<VAR>s✝ : Finset ι<VAR>k : ι<VAR>s : Finset ι<VAR>hk : ∀ x ∈ s, k < x<VAR>ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j<GOAL>(f (update (s.piecewise b a) k (s.piecewise b a k - b k)) + ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j) = (f fun j => if j ∈ insert k s → j < k then a j else if k = j then a j - b j else b j) + ∑ x ∈ s, f fun j => if j ∈ insert k s → j < x then a j else if x = j then a j - b j else b j