ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<GOAL>Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (⨆ i, μ (Accumulate f i)))
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this : ProperSpace E<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<VAR>x : E<VAR>hx : x ≠ 0<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<VAR>x : E<VAR>hx : x ≠ 0<VAR>H₁ : IsCompact (sphere 0 ‖x‖)<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<VAR>x : E<VAR>hx : x ≠ 0<VAR>H₁ : IsCompact (sphere 0 ‖x‖)<VAR>H₂ : (sphere 0 ‖x‖).Nonempty<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<VAR>x : E<VAR>hx : x ≠ 0<VAR>H₁ : IsCompact (sphere 0 ‖x‖)<VAR>H₂ : (sphere 0 ‖x‖).Nonempty<VAR>x₀ : E<VAR>hx₀' : x₀ ∈ sphere 0 ‖x‖<VAR>hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this✝ : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<VAR>x : E<VAR>hx : x ≠ 0<VAR>H₁ : IsCompact (sphere 0 ‖x‖)<VAR>H₂ : (sphere 0 ‖x‖).Nonempty<VAR>x₀ : E<VAR>hx₀' : x₀ ∈ sphere 0 ‖x‖<VAR>hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀<VAR>hx₀ : ‖x₀‖ = ‖x‖<VAR>this : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>this✝ : ProperSpace E<VAR>T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint<VAR>x : E<VAR>hx : x ≠ 0<VAR>H₁ : IsCompact (sphere 0 ‖x‖)<VAR>H₂ : (sphere 0 ‖x‖).Nonempty<VAR>x₀ : E<VAR>hx₀' : x₀ ∈ sphere 0 ‖x‖<VAR>hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀<VAR>hx₀ : ‖x₀‖ = ‖x‖<VAR>this : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>hx₀_ne : x₀ ≠ 0<GOAL>HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁✝ G₂✝ : G.Subgraph<VAR>a b : V<VAR>G₁ G₂ : G.Subgraph<VAR>h : (fun G' => (G'.verts, G'.spanningCoe)) G₁ = (fun G' => (G'.verts, G'.spanningCoe)) G₂<GOAL>G₁ = G₂
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁✝ G₂✝ : G.Subgraph<VAR>a b : V<VAR>G₁ G₂ : G.Subgraph<VAR>h : ((fun G' => (G'.verts, G'.spanningCoe)) G₁).1 = ((fun G' => (G'.verts, G'.spanningCoe)) G₂).1 ∧ ((fun G' => (G'.verts, G'.spanningCoe)) G₁).2 = ((fun G' => (G'.verts, G'.spanningCoe)) G₂).2<GOAL>G₁ = G₂
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>(∃ i, ∃ (hi : i < o), o.nfpBFamily f a ≤ f i hi b) ↔ o.nfpBFamily f a ≤ b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>(¬∃ i, ∃ (hi : i < o), o.nfpBFamily f a ≤ f i hi b) ↔ ¬o.nfpBFamily f a ≤ b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a) ↔ b < o.nfpBFamily f a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → LinearOrder (α i)<VAR>x y z a : (i : ι) → α i<VAR>hay : a ∉ univ.pi fun i => Ioc (y i) (z i)<VAR>hax : x ≤ a<VAR>haz : a ≤ z<GOAL>a ∈ ⋃ i, Icc x (update z i (y i))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝¹ : Category.{max v u, w} D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : C<VAR>W : (J.Cover X)ᵒᵖ<VAR>i : ((unop W).index Q).R<GOAL>(Multiequalizer.ι ((unop W).index P) (((unop W).index Q).fstTo i) ≫ η.app (op (((unop W).index Q).fstTo i).Y)) ≫ ((unop W).index Q).fst i = (Multiequalizer.ι ((unop W).index P) (((unop W).index Q).sndTo i) ≫ η.app (op (((unop W).index Q).sndTo i).Y)) ≫ ((unop W).index Q).snd i
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝¹ : Category.{max v u, w} D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : C<VAR>W : (J.Cover X)ᵒᵖ<VAR>i : ((unop W).index Q).R<GOAL>Multiequalizer.ι ((unop W).index P) (((unop W).index P).sndTo i) ≫ ((unop W).index P).snd i ≫ η.app (op i.r.Z) = Multiequalizer.ι ((unop W).index P) (((unop W).index Q).sndTo i) ≫ P.map i.r.g₂.op ≫ η.app (op i.r.Z)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<GOAL>C (C 2) * Y + C (C (map W f).toAffine.a₁ * X + C (map W f).toAffine.a₃) = Polynomial.map (mapRingHom f) (C (C 2) * Y + C (C W.a₁ * X + C W.a₃))
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>s : Opens M<VAR>hs : Nonempty ↥s<VAR>G : StructureGroupoid H<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' : PartialHomeomorph (↥s) H<VAR>he' : e' ∈ atlas H ↥s<GOAL>(e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>s : Opens M<VAR>hs : Nonempty ↥s<VAR>G : StructureGroupoid H<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' : PartialHomeomorph (↥s) H<VAR>he' : e' ∈ atlas H ↥s<VAR>x : ↥s<VAR>this : e' = (chartAt H ↑x).subtypeRestr hs<GOAL>(e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>s : Opens M<VAR>hs : Nonempty ↥s<VAR>G : StructureGroupoid H<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' : PartialHomeomorph (↥s) H<VAR>he' : e' ∈ atlas H ↥s<VAR>x : ↥s<VAR>this : e' = (chartAt H ↑x).subtypeRestr hs<GOAL>(e.subtypeRestr hs).symm ≫ₕ (chartAt H ↑x).subtypeRestr hs ∈ G ∧ ((chartAt H ↑x).subtypeRestr hs).symm ≫ₕ e.subtypeRestr hs ∈ G
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<GOAL>C (C (map W f).toAffine.a₁) * Y - C (C 3 * X ^ 2 + C (2 * (map W f).toAffine.a₂) * X + C (map W f).toAffine.a₄) = Polynomial.map (mapRingHom f) (C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : 0 < a + b<GOAL>f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : 0 < a + b<GOAL>a / (a + b) + b / (a + b) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) < a • f x + b • f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∉ closure s<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hx : 𝓝[s] x = ⊥<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hx : 𝓝[s] x = ⊥<GOAL>Tendsto f ⊥ (𝓝 (f x))
<VAR>x y : ℝ<GOAL>↑(rexp (-x)) = ↑(rexp x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ℕ → α<VAR>k : ℕ<GOAL>⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ℕ → α<VAR>k : ℕ<VAR>hf : Monotone fun n => ⨅ i, ⨅ (_ : i ≥ n), f i<GOAL>⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ℕ → α<VAR>k : ℕ<VAR>hf : Monotone fun n => ⨅ i, ⨅ (_ : i ≥ n), f i<GOAL>⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P✝ : Type u_3<VAR>inst✝¹ : CommSemiring P✝<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S P<VAR>hze : 0 = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P✝ : Type u_3<VAR>inst✝¹ : CommSemiring P✝<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S P<VAR>hze : (algebraMap R S) 0 = (algebraMap R S) 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P✝ : Type u_3<VAR>inst✝¹ : CommSemiring P✝<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S P<VAR>hze : (algebraMap R S) 0 = (algebraMap R S) 1<VAR>t : ↥P.primeCompl<VAR>ht : ↑t * 0 = ↑t * 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P✝ : Type u_3<VAR>inst✝¹ : CommSemiring P✝<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S P<VAR>hze : (algebraMap R S) 0 = (algebraMap R S) 1<VAR>t : ↥P.primeCompl<VAR>ht : ↑t * 0 = ↑t * 1<VAR>htz : ↑t = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>s : Multiset α<VAR>hs : ∀ a ∈ s, Irreducible a<GOAL>normalizedFactors s.prod = Multiset.map (⇑normalize) s
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>hs : ∀ a ∈ 0, Irreducible a<GOAL>normalizedFactors (Multiset.prod 0) = Multiset.map (⇑normalize) 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>s : Multiset α<VAR>ih : (∀ a ∈ s, Irreducible a) → normalizedFactors s.prod = Multiset.map (⇑normalize) s<VAR>hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1<GOAL>normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize) (a ::ₘ s)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝² : Group W<VAR>inst✝¹ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>G : Type u_5<VAR>inst✝ : Group G<VAR>f : B → G<VAR>hf : M.IsLiftable f<VAR>i i' : B<GOAL>(FreeGroup.lift f) (uncurry M.relation (i, i')) = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝² : Group W<VAR>inst✝¹ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>G : Type u_5<VAR>inst✝ : Group G<VAR>f : B → G<VAR>hf : M.IsLiftable f<VAR>i i' : B<GOAL>(f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>Ω n = 1 ↔ Nat.Prime n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h : Ω n = 1<GOAL>Nat.Prime n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h : Ω (n + 1) = 1<GOAL>Nat.Prime (n + 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h : Ω (n + 1) = 1<VAR>x : ℕ<VAR>hx : (n + 1).primeFactorsList = [x]<GOAL>Nat.Prime (n + 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h : Ω (n + 1) = 1<VAR>x : ℕ<VAR>hx : (n + 1).primeFactorsList = [x]<GOAL>Nat.Prime x
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h : Ω (n + 1) = 1<VAR>x : ℕ<VAR>hx : (n + 1).primeFactorsList = [x]<GOAL>x ∈ ?succ.intro.n.primeFactorsList
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h : Ω (n + 1) = 1<VAR>x : ℕ<VAR>hx : (n + 1).primeFactorsList = [x]<GOAL>ℕ
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>inst✝¹ : Algebra R Q<VAR>inst✝ : IsLocalization M Q<VAR>f : S →+* Q<VAR>hf : f.comp (algebraMap R S) = algebraMap R Q<GOAL>f = ↑(algEquiv M S Q)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>inst✝¹ : Algebra R Q<VAR>inst✝ : IsLocalization M Q<VAR>f : S →+* Q<VAR>hf : f.comp (algebraMap R S) = algebraMap R Q<GOAL>f.comp (algebraMap R S) = (↑(algEquiv M S Q)).comp (algebraMap R S)
<VAR>x y : ℂ<GOAL>tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>h : Fix F α → β<VAR>hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)<VAR>x : Fix F α<GOAL>rec g x = h x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>h : Fix F α → β<VAR>hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)<VAR>x : Fix F α<GOAL>∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>h : Fix F α → β<VAR>hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)<VAR>x✝ : Fix F α<VAR>x : F (α ::: Fix F α)<VAR>hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x<GOAL>rec g (mk x) = h (mk x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly.leadingCoeff = P.d
<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>x ≤ sin x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>x : R<VAR>n : ℤ<GOAL>(algebraMap R A) (eval x (U R n)) = eval ((algebraMap R A) x) (U A n)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_3}<GOAL>a ≤ b + a
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set H<VAR>hs : IsOpen s<VAR>h's : IsOpen (↑I.symm ⁻¹' s)<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set H<VAR>hs : IsOpen s<VAR>h's : IsOpen (↑I.symm ⁻¹' s)<VAR>f : E → ℝ<VAR>f_supp : support f = ↑I.symm ⁻¹' s<VAR>f_diff : ContDiff ℝ ⊤ f<VAR>f_range : range f ⊆ Icc 0 1<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>f g : (i : ι) → α i<GOAL>(g ∈ univ.pi fun i => {f i}) ↔ g ∈ {f}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<GOAL>Dense ↑S ∨ ∃ a, S = closure {a}
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>h : ¬∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<GOAL>∃ a, S = closure {a}
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>ε : G<VAR>ε0 : ε > 0<VAR>hε : ∀ g ∈ S, g ∉ Ioo 0 ε<GOAL>∃ a, S = closure {a}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.21217, u_1} A<VAR>J : GrothendieckTopology C<VAR>S : C<VAR>E : PreOneHypercover S<VAR>inst✝ : E.HasPullbacks<VAR>mem₀ : E.sieve₀ ∈ J.sieves S<VAR>mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J.sieves (Limits.pullback (E.f i₁) (E.f i₂))<VAR>i₁ i₂ : E.I₀<VAR>W : C<VAR>p₁ : W ⟶ E.X i₁<VAR>p₂ : W ⟶ E.X i₂<VAR>w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂<GOAL>E.sieve₁ p₁ p₂ ∈ J.sieves W
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.21217, u_1} A<VAR>J : GrothendieckTopology C<VAR>S : C<VAR>E : PreOneHypercover S<VAR>inst✝ : E.HasPullbacks<VAR>mem₀ : E.sieve₀ ∈ J.sieves S<VAR>mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J.sieves (Limits.pullback (E.f i₁) (E.f i₂))<VAR>i₁ i₂ : E.I₀<VAR>W : C<VAR>p₁ : W ⟶ E.X i₁<VAR>p₂ : W ⟶ E.X i₂<VAR>w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂<GOAL>Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) ∈ J.sieves W
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0∞<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<VAR>a : α<GOAL>a ∈ (ofFinset f s h h').support ↔ a ∈ ↑s ∩ Function.support f
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<VAR>f : α → β<GOAL>map (fun x => (x, f x)) l = l.zip (map f l)