ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<VAR>h : lift.{max w w', w} #↑(⇑Equiv.ulift '' s') = lift.{w, max w w'} #↑s'<GOAL>lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<VAR>h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'<GOAL>lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<VAR>h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'<GOAL>#↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')) = #↑(⇑Equiv.ulift '' s')
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<VAR>h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'<GOAL>max ℵ₀ (lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s') + lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i)) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<VAR>h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'<GOAL>ℵ₀ ≤ #↑s' ∧ #↑(s ∪ ⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s') ∧ lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<VAR>h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'<GOAL>ℵ₀ ≤ lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s')
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t A B : Set β<VAR>a : α<VAR>x : β<GOAL>a • sᶜ = (a • s)ᶜ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>p2 : P<VAR>hp2 : p2 ∈ s<VAR>v2 : V<VAR>hv2 : v2 ∈ vectorSpan k s<VAR>hv2p : p = v2 +ᵥ p2<GOAL>v +ᵥ p ∈ spanPoints k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>v : V<VAR>hv : v ∈ vectorSpan k s<VAR>p2 : P<VAR>hp2 : p2 ∈ s<VAR>v2 : V<VAR>hv2 : v2 ∈ vectorSpan k s<VAR>hv2p : p = v2 +ᵥ p2<GOAL>v + v2 +ᵥ p2 ∈ spanPoints k s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m (s ∪ t) ≤ m s + m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m s + m (t \ s) ≤ m s + m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>Disjoint s (t \ s)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_zero : f 0 = 0<GOAL>seminormFromBounded' f 0 = 0
<GOAL>Tendsto W atTop (𝓝 (π / 2))
<GOAL>Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<GOAL>Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<GOAL>Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<GOAL>Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<VAR>h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)<GOAL>Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<VAR>h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)<GOAL>Tendsto (fun i => 1 - 1 / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<VAR>h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)<GOAL>Tendsto (fun i => 2 * ↑i + 2) atTop atTop
<VAR>this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))<VAR>h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)<GOAL>Tendsto (fun i => 2 * ↑i) atTop atTop
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>decomposeFin.symm (p, Equiv.refl (Fin n)) = swap 0 p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Fintype I<VAR>e : I → R<VAR>he : CompleteOrthogonalIdempotents e<GOAL>Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : Ring K<VAR>inst✝⁵ : StrongRankCondition K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>inst✝² : Finite K<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<GOAL>#V < ℵ₀
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : Ring K<VAR>inst✝⁵ : StrongRankCondition K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>inst✝² : Finite K<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<GOAL>lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<GOAL>Subsingleton (Quotient s) ↔ s = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<GOAL>(∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → s.Rel x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<VAR>a : α<GOAL>(∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → s.Rel a y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<VAR>a b : α<GOAL>Quotient.mk' a = Quotient.mk' b ↔ ⊤ → s.Rel a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<VAR>a b : α<GOAL>Setoid.r a b ↔ s.Rel a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>c : ℝ≥0∞<GOAL>∫⁻ (x : α) in s, c ∂μ = c * μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s t u : Finset α<VAR>a b : α<GOAL>_root_.Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic R<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>φ : R →+* S<VAR>inst✝ : IsDomain R<VAR>h0 : P.toPoly ≠ 0<VAR>x : R<GOAL>x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic R<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>φ : R →+* S<VAR>inst✝ : IsDomain R<VAR>h0 : P.toPoly ≠ 0<VAR>x : R<GOAL>eval x (C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hx h2x : x ∈ e.source<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hx : x ∈ e.source<VAR>h2x : x ∈ (e.extend I).source<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hx : x ∈ e.source<VAR>h2x : x ∈ (e.extend I).source<GOAL>ContinuousWithinAt (fun x => f (↑e.symm x)) (↑e.symm ⁻¹' s) (↑e x) ∧ ContDiffWithinAt 𝕜 n (fun x_1 => ↑I' (↑(chartAt H' (f x)) (f (↑e.symm (↑I.symm x_1))))) (↑I.symm ⁻¹' (↑e.symm ⁻¹' s) ∩ range ↑I) (↑I (↑e x)) ↔ ContinuousWithinAt (fun x => f (↑e.symm x)) (↑e.symm ⁻¹' s) (↑e x) ∧ ContDiffWithinAt 𝕜 n (fun x_1 => ↑I' (↑(chartAt H' (f x)) (f (↑(e.extend I).symm x_1)))) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : HomotopyEquiv C D<GOAL>(quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : HomotopyEquiv C D<GOAL>(quotient V c).map (f.hom ≫ f.inv) = (quotient V c).map (𝟙 C)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : HomotopyEquiv C D<GOAL>(quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : HomotopyEquiv C D<GOAL>(quotient V c).map (f.inv ≫ f.hom) = (quotient V c).map (𝟙 D)
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>f₁ f₂ : MvPolynomial σ K<VAR>h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ<VAR>F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁<GOAL>p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>f₁ f₂ : MvPolynomial σ K<VAR>h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ<VAR>F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁<VAR>this : ∑ b : Bool, (F b).totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>inst✝ : HasDerivedCategory C<VAR>a b : ℕ<VAR>α : Ext X Y a<VAR>β : Ext Y Z b<VAR>c : ℕ<VAR>h : a + b = c<GOAL>(α.comp β h).hom = α.hom.comp β.hom ⋯
<VAR>c d : ℝ<VAR>hc : 1 ≤ c ^ 2<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>r ⟨z, hz⟩ ≤ Complex.abs (↑c * ↑⟨z, hz⟩ + ↑d)
<VAR>c d : ℝ<VAR>hc : 1 ≤ c ^ 2<VAR>z : ℂ<VAR>hz : 0 < z.im<VAR>H1 : z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)<GOAL>r ⟨z, hz⟩ ≤ Complex.abs (↑c * ↑⟨z, hz⟩ + ↑d)
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<GOAL>Algebra.adjoin R s = ((lift R) Subtype.val).range
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : Mul α<VAR>inst✝² : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : Preorder α<GOAL>PosMulMono α ↔ MulPosMono α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>a : α<VAR>l : List α<GOAL>(a :: l).tails = (map reverse (a :: l).reverse.inits).reverse
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → σ →₀ ℕ<VAR>a : R<GOAL>(monomial (∑ i ∈ s, f i)) a = C a * ∏ i ∈ s, (monomial (f i)) 1
<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>M : Type u_7<VAR>N : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Invertible 2<VAR>inst✝³ : Lattice β<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊔ y = ⅟2 • (x + y + |y - x|)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>Function.Surjective ⇑S.moduleCatToCycles ↔ Function.Surjective ⇑S.moduleCatToCycles
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a✝ a₁ a₂ b b₁ b₂ c x a : α<GOAL>Injective (uIcc a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : FirstCountableTopology β<VAR>inst✝ : OrderTopology β<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f) _auto✝<GOAL>μ {y | essSup f μ < f y} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : FirstCountableTopology β<VAR>inst✝ : OrderTopology β<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f) _auto✝<GOAL>μ {y | ¬f y ≤ essSup f μ} = 0
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<GOAL>eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s) = eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<GOAL>s = ⇑ofDual '' (⇑ofDual ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<GOAL>diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<GOAL>(max (max (edist x y) (edist x z)) (edist y z)).toReal = max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal
<VAR>V : Type u<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<GOAL>(adjMatrix α G ^ 2) v w = (k • 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w
<VAR>V : Type u<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<GOAL>↑(Fintype.card { x // x.length = 2 }) = (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0
<VAR>V : Type u<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<GOAL>↑(Fintype.card ↑(G.commonNeighbors v w)) = (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0
<VAR>V : Type u<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v : V<GOAL>↑(Fintype.card ↑(G.commonNeighbors v v)) = (k • 1 v v + ℓ • if G.Adj v v then 1 else 0) + μ • if v ≠ v ∧ ¬G.Adj v v then 1 else 0
<VAR>V : Type u<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>hn : v ≠ w<GOAL>↑(Fintype.card ↑(G.commonNeighbors v w)) = (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))