ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ Function.Exact ⇑S.f ⇑S.g
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>LinearMap.range S.f = LinearMap.ker S.g ↔ LinearMap.ker S.g = LinearMap.range S.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q : ℕ<GOAL>Q (q + 1) = Q q - P q ≫ Hσ q
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q : ℕ<GOAL>𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → ℂ<VAR>s a : ℂ<GOAL>mellin (fun t => f t / a) s = mellin f s / a
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(l.balanceR x r).dual = r.dual.balanceL x l.dual
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : WSeq α<GOAL>(map (ret ∘ f) s).join ~ʷ map f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : WSeq α<GOAL>(map ret (map f s)).join ~ʷ map f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : IsClosedMap f<VAR>s : Set β<VAR>t : Set ↑(f ⁻¹' s)<GOAL>IsClosed t → IsClosed (s.restrictPreimage f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : IsClosedMap f<VAR>s : Set β<VAR>t : Set ↑(f ⁻¹' s)<GOAL>∀ (u : Set α), IsClosed u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k n : ℕ<GOAL>∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k n : ℕ<VAR>C : ℝ<VAR>hC : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C<GOAL>∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a : E<GOAL>dist 1 a = ‖a‖
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>hB : TopologicalSpace.IsTopologicalBasis {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<GOAL>∀ (j : J), TopologicalSpace.IsTopologicalBasis ((fun j => {W | IsClopen W}) j)
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<GOAL>∀ (i j : J) (f : i ⟶ j), ∀ V ∈ (fun j => {W | IsClopen W}) j, ⇑((F ⋙ toTopCat).map f) ⁻¹' V ∈ (fun j => {W | IsClopen W}) i
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>hB : TopologicalSpace.IsTopologicalBasis {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<VAR>hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<VAR>hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)<VAR>hsU : U ⊆ ⋃ i, (fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<VAR>hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)<VAR>hsU : U ⊆ ⋃ i, (fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i<VAR>this : ∃ t, U ⊆ ⋃ i ∈ t, (fun s => ⇑(C.π.app (j s)) ⁻¹' V s) i<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<VAR>hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)<VAR>hsU : U ⊆ ⋃ i, (fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i<VAR>G : Finset ↑S<VAR>hG : U ⊆ ⋃ i ∈ G, (fun s => ⇑(C.π.app (j s)) ⁻¹' V s) i<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<VAR>hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)<VAR>hsU : U ⊆ ⋃ i, (fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i<VAR>G : Finset ↑S<VAR>hG : U ⊆ ⋃ i ∈ G, (fun s => ⇑(C.π.app (j s)) ⁻¹' V s) i<VAR>j0 : J<VAR>hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : IsLimit C<VAR>hU : IsClopen U<VAR>S : Set (Set ↑(toTopCat.mapCone C).pt)<VAR>hS : S ⊆ {U | ∃ j, ∃ V ∈ (fun j => {W | IsClopen W}) j, U = ⇑((toTopCat.mapCone C).π.app j) ⁻¹' V}<VAR>h : U = ⋃₀ S<VAR>j : ↑S → J := fun s => Exists.choose ⋯<VAR>V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s => ⋯.choose<VAR>hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(C.π.app (j s)) ⁻¹' V s<VAR>hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)<VAR>hsU : U ⊆ ⋃ i, (fun s => (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i<VAR>G : Finset ↑S<VAR>hG : U ⊆ ⋃ i ∈ G, (fun s => ⇑(C.π.app (j s)) ⁻¹' V s) i<VAR>j0 : J<VAR>hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)<VAR>f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => ⋯.some<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : ¬p = 0<VAR>a✝ : Nontrivial R<GOAL>p.mirror.natDegree = p.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp : ¬p = 0<VAR>a✝ : Nontrivial R<GOAL>p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h₀ : x = abs ⟨a, f⟩<VAR>h₁ : ∀ (i : (P F).B a), p (f i)<GOAL>Liftp p x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h₀ : x = abs ⟨a, f⟩<VAR>h₁ : ∀ (i : (P F).B a), p (f i)<GOAL>Subtype.val <$> abs ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h₀ : x = abs ⟨a, f⟩<VAR>h₁ : ∀ (i : (P F).B a), p (f i)<GOAL>abs ((P F).map Subtype.val ⟨a, fun i => ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : (t ∩ mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Summable fun n => ↑|n| ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Summable fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>(fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))) =O[atTop] fun n => ↑n ^ k * rexp (-1 * ↑n)
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>(fun x => rexp (-π * (T * ↑x ^ 2 - 2 * S * ↑x))) =O[atTop] fun x => rexp (-1 * ↑x)
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Tendsto ((fun x => -π * (T * ↑x ^ 2 - 2 * S * ↑x)) - fun x => -1 * ↑x) atTop atBot
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Tendsto (fun x => -(-π * (T * ↑x ^ 2 - 2 * S * ↑x) - -1 * ↑x)) atTop atTop
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Tendsto (fun n => ↑n * (π * T * ↑n - (2 * π * S + 1))) atTop atTop
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Tendsto (fun n => π * T * ↑n) atTop atTop
<VAR>p n pow : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : p ^ pow ∣ n<VAR>c : ℕ<VAR>hc : n = p ^ pow * c<GOAL>pow ≤ p.maxPowDiv n
<VAR>p n pow : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : p ^ pow ∣ n<VAR>c : ℕ<VAR>hc : n = p ^ pow * c<VAR>this : 0 < c<GOAL>pow ≤ p.maxPowDiv n
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>rightHomologyMap φ ≫ h₂.rightHomologyIso.hom = h₁.rightHomologyIso.hom ≫ γ.φH
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X × Y<GOAL>map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X × Y<VAR>s : Set Y<VAR>hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)<GOAL>s ∈ 𝓝 x.2
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set Y<VAR>x : X<VAR>y : Y<VAR>hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))<GOAL>s ∈ 𝓝 (x, y).2
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set Y<VAR>x : X<VAR>y : Y<VAR>hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}<GOAL>s ∈ 𝓝 (x, y).2
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set Y<VAR>x : X<VAR>y : Y<VAR>u : Set X<VAR>hu : u ∈ 𝓝 x<VAR>v : Set Y<VAR>hv : v ∈ 𝓝 y<VAR>H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}<GOAL>s ∈ 𝓝 (x, y).2
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set Y<VAR>x : X<VAR>y : Y<VAR>u : Set X<VAR>hu : u ∈ 𝓝 x<VAR>v : Set Y<VAR>hv : v ∈ 𝓝 y<VAR>H : ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s<GOAL>s ∈ 𝓝 (x, y).2
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p n ≤ count p (n + 1)
<VAR>m n✝ n : ℕ<VAR>x : ZMod (n + 1)<GOAL>x.valMinAbs = 0 ↔ x = 0
<VAR>m n✝ n : ℕ<VAR>x : ZMod (n + 1)<GOAL>x.valMinAbs = valMinAbs 0 ↔ x = 0
<VAR>n : ℕ<GOAL>(∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
<GOAL>(∃ x y, 0 = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q 0)
<VAR>n : ℕ<VAR>hn₀ : n > 0<GOAL>(∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
<VAR>n : ℕ<VAR>hn₀ : n > 0<GOAL>(∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
<VAR>x y : ℤ[i]<GOAL>(toComplex (x / y)).re = ↑(round (toComplex x / toComplex y).re)
<VAR>x y : ℤ[i]<GOAL>(toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }).re = ↑(round (toComplex x / toComplex y).re)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : Semiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>P : Type u_4<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M<VAR>v' : ι → M'<VAR>v : ι → M<VAR>i₁ i₂ : ι<VAR>heq : v i₁ = v i₂<VAR>hne : i₁ ≠ i₂<GOAL>f v = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>s : Set M<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.total M M R id) l = 0 → l = 0
<VAR>a b c : ℕ<GOAL>Fintype.card ↑(Set.Iio b) = b
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ memPartitionSet f n a
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (range (F.map f)).Finite<VAR>j i : J<VAR>hi : i ⟶ j<VAR>hf : (range (F.map hi)).Finite<GOAL>∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ j), range (F.map f) ⊆ range (F.map g)
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝¹ j✝ k : J<VAR>s : Set (F.obj i✝¹)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (range (F.map f)).Finite<VAR>j i✝ : J<VAR>hi : i✝ ⟶ j<VAR>hf : (range (F.map hi)).Finite<VAR>m : Finset (F.obj j)<VAR>hmin : ∀ x ∈ {s | ∃ i f, ↑s = range (F.map f)}, ¬x < m<VAR>i : J<VAR>f : i ⟶ j<VAR>hm : ↑m = range (F.map f)<GOAL>∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ j), range (F.map f) ⊆ range (F.map g)
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝¹ j✝ k✝ : J<VAR>s : Set (F.obj i✝¹)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (range (F.map f)).Finite<VAR>j i✝ : J<VAR>hi : i✝ ⟶ j<VAR>hf : (range (F.map hi)).Finite<VAR>m : Finset (F.obj j)<VAR>hmin : ∀ x ∈ {s | ∃ i f, ↑s = range (F.map f)}, ¬x < m<VAR>i : J<VAR>f : i ⟶ j<VAR>hm : ↑m = range (F.map f)<VAR>k : J<VAR>g : k ⟶ j<GOAL>∀ a ∈ range fun f => range (F.map f.snd), a ≤ (fun f => range (F.map f.snd)) ⟨i, f⟩ → (fun f => range (F.map f.snd)) ⟨i, f⟩ ≤ a
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝¹ j✝ k✝ : J<VAR>s : Set (F.obj i✝¹)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (range (F.map f)).Finite<VAR>j i✝ : J<VAR>hi : i✝ ⟶ j<VAR>hf : (range (F.map hi)).Finite<VAR>m : Finset (F.obj j)<VAR>hmin : ∀ x ∈ {s | ∃ i f, ↑s = range (F.map f)}, ¬x < m<VAR>i : J<VAR>f : i ⟶ j<VAR>hm : ↑m = range (F.map f)<VAR>k : J<VAR>g : k ⟶ j<VAR>k' : J<VAR>g' : k' ⟶ j<VAR>hl : (fun f => range (F.map f.snd)) ⟨k', g'⟩ ≤ (fun f => range (F.map f.snd)) ⟨i, f⟩<GOAL>(fun f => range (F.map f.snd)) ⟨i, f⟩ ≤ (fun f => range (F.map f.snd)) ⟨k', g'⟩
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝¹ j✝ k✝ : J<VAR>s : Set (F.obj i✝¹)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (range (F.map f)).Finite<VAR>j i✝ : J<VAR>hi : i✝ ⟶ j<VAR>hf : (range (F.map hi)).Finite<VAR>m : Finset (F.obj j)<VAR>hmin : ∀ x ∈ {s | ∃ i f, ↑s = range (F.map f)}, ¬x < m<VAR>i : J<VAR>f : i ⟶ j<VAR>hm : ↑m = range (F.map f)<VAR>k : J<VAR>g : k ⟶ j<VAR>k' : J<VAR>g' : k' ⟶ j<VAR>hl : (fun f => range (F.map f.snd)) ⟨k', g'⟩ ≤ (fun f => range (F.map f.snd)) ⟨i, f⟩<GOAL>¬(fun f => range (F.map f.snd)) ⟨k', g'⟩ < (fun f => range (F.map f.snd)) ⟨i, f⟩
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝¹ j✝ k✝ : J<VAR>s : Set (F.obj i✝¹)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (range (F.map f)).Finite<VAR>j i✝ : J<VAR>hi : i✝ ⟶ j<VAR>hf : (range (F.map hi)).Finite<VAR>m : Finset (F.obj j)<VAR>hmin : ∀ x ∈ {s | ∃ i f, ↑s = range (F.map f)}, ¬x < m<VAR>i : J<VAR>f : i ⟶ j<VAR>hm : ↑m = range (F.map f)<VAR>k : J<VAR>g : k ⟶ j<VAR>k' : J<VAR>g' : k' ⟶ j<VAR>hl : (fun f => range (F.map f.snd)) ⟨k', g'⟩ ≤ (fun f => range (F.map f.snd)) ⟨i, f⟩<VAR>this : ¬⋯.toFinset < m<GOAL>¬(fun f => range (F.map f.snd)) ⟨k', g'⟩ < (fun f => range (F.map f.snd)) ⟨i, f⟩
<VAR>α : Type w<VAR>inst✝ : Finite α<VAR>X : α → CompHaus<VAR>a : α<VAR>x y : (forget CompHaus).obj (X a)<VAR>hxy : (ι X a) x = (ι X a) y<GOAL>x = y
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : IsNoetherian R₁ ↥↑I<VAR>hx : ¬x = 0<GOAL>IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : IsNoetherian R₁ ↥↑I<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<GOAL>IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : IsNoetherian R₁ ↥↑I<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<VAR>h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0<GOAL>IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)