ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>a : ℝ<VAR>hfi : IntegrableOn f (Ioi a) μ<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Iic (b i)<VAR>hφ : AECover (μ.restrict (Ioi a)) l φ<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>a : ℝ<VAR>hfi : IntegrableOn f (Ioi a) μ<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Iic (b i)<VAR>hφ : AECover (μ.restrict (Ioi a)) l φ<GOAL>(fun i => ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a)) =ᶠ[l] fun i => ∫ (x : ℝ) in a..b i, f x ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>a : ℝ<VAR>hfi : IntegrableOn f (Ioi a) μ<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Iic (b i)<VAR>hφ : AECover (μ.restrict (Ioi a)) l φ<VAR>i : ι<VAR>hbi : a ≤ b i<GOAL>∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a) = ∫ (x : ℝ) in a..b i, f x ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>a : ℝ<VAR>hfi : IntegrableOn f (Ioi a) μ<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Iic (b i)<VAR>hφ : AECover (μ.restrict (Ioi a)) l φ<VAR>i : ι<VAR>hbi : a ≤ b i<GOAL>∫ (x : ℝ) in Ioi a ∩ φ i, f x ∂μ = ∫ (x : ℝ) in Ioc a (b i), f x ∂μ
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c₀ : Chain (α →𝒄 β)<VAR>c₁ : Chain α<VAR>z : β<GOAL>(∀ (j i : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module R F<VAR>inst✝³ : (x : B) → AddCommMonoid (E x)<VAR>inst✝² : (x : B) → Module R (E x)<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : Trivialization.IsLinear R e<VAR>inst✝ : Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>y : F<GOAL>(coordChangeL R e e' b) y = (↑e' (↑e.symm (b, y))).2
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Preorder α<VAR>a b✝ c b : α<GOAL>⋃ a, Icc a b = Iic b
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>↑((P.sparsePairs G ε).biUnion fun x => match x with | (U, V) => G.interedges U V).card ≤ ε * (↑A.card + ↑P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>∑ UV ∈ P.sparsePairs G ε, ↑(G.interedges UV.1 UV.2).card ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (↑UV.1.card * ↑UV.2.card)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>∑ i ∈ P.parts.offDiag, ↑i.1.card * ↑i.2.card ≤ (↑A.card + ↑P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>∑ x ∈ P.parts.offDiag, x.1.card * x.2.card ≤ (A.card + P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>∀ x ∈ P.parts.offDiag, (fun i => i.1.card * i.2.card) x ≤ (A.card / P.parts.card + 1) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>P.parts.offDiag.card • (A.card / P.parts.card + 1) ^ 2 ≤ (P.parts.card * (A.card / P.parts.card) + P.parts.card) ^ 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Exact ⇑f ⇑g<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>r : Submodule R P<VAR>hpq : p ≤ comap f q<VAR>hqr : q ≤ comap g r<GOAL>Exact ⇑(p.mapQ q f hpq) ⇑(q.mapQ r g hqr) ↔ range g ⊓ r ≤ map g q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Exact ⇑f ⇑g<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>r : Submodule R P<VAR>hpq : p ≤ comap f q<VAR>hqr : q ≤ comap g r<GOAL>comap q.mkQ (ker (q.mapQ r g hqr)) = comap q.mkQ (range (p.mapQ q f hpq)) ↔ range g ⊓ r ≤ map g q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Exact ⇑f ⇑g<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>r : Submodule R P<VAR>hpq : p ≤ comap f q<VAR>hqr : q ≤ comap g r<GOAL>comap q.mkQ (ker (q.liftQ (r.mkQ ∘ₗ g) ⋯)) = comap q.mkQ (range (p.liftQ (q.mkQ ∘ₗ f) ⋯)) ↔ range g ⊓ r ≤ map g q
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<GOAL>image compl s = sᶜˢ
<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>f : X → A<VAR>g : FreeAlgebra R X →ₐ[R] A<GOAL>⇑g ∘ ι R = f ↔ g = (lift R) f
<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>f : X → A<VAR>g : FreeAlgebra R X →ₐ[R] A<GOAL>⇑g ∘ ι R = f ↔ { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm g = f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f ∈ g.cycleFactorsFinset<GOAL>(g * f⁻¹).Disjoint f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a<GOAL>(g * f⁻¹).Disjoint f
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsClosed s<GOAL>IsClosed (Sigma.mk i '' s)
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsClosed s<GOAL>∀ (i_1 : ι), IsClosed (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsClosed s<VAR>j : ι<GOAL>IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>j : ι<VAR>s : Set (σ j)<VAR>hs : IsClosed s<GOAL>IsClosed (Sigma.mk j ⁻¹' (Sigma.mk j '' s))
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>i : ι<VAR>s : Set (σ i)<VAR>hs : IsClosed s<VAR>j : ι<VAR>hne : j ≠ i<GOAL>IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
<VAR>α✝ : Sort ?u.57203<VAR>inst✝ : DecidableEq α✝<VAR>α : Type u_1<VAR>x : α<VAR>l : List α<VAR>n : Nat<VAR>h : n ≤ l.length<GOAL>insertNth n x l ~ x :: l
<VAR>E : Type u_1<VAR>p : ℝ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hp : 0 < p<GOAL>μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>p : ℝ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hp : 0 < p<VAR>hE : Subsingleton E<GOAL>μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>p : ℝ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hp : 0 < p<VAR>hE : Nontrivial E<GOAL>μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>ω.cof ≤ ℵ₀
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>ω.cof ≤ ω.card
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.ε.app X) = (F.map (λ_ n).inv).app X ≫ (F.μIso (𝟙_ M) n).inv.app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.ε.app X) = 𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X)) ≫ (F.map (λ_ n).inv).app X ≫ (F.μIso (𝟙_ M) n).inv.app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.ε.app X) ≫ inv ((F.μIso (𝟙_ M) n).inv.app X) ≫ inv ((F.map (λ_ n).inv).app X) = 𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>e_1✝ : ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X)) = ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj X)<VAR>e_5✝ : (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) = (F.obj n).obj X<GOAL>inv ((F.μIso (𝟙_ M) n).inv.app X) = (F.μ (𝟙_ M) n).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>e_1✝ : ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X)) = ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj X)<VAR>e_5✝ : (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) = (F.obj n).obj X<GOAL>inv ((F.map (λ_ n).inv).app X) = (F.map (λ_ n).hom).app X
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>f : (AlgebraicClosureAux k)[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>∃ x, eval x f = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>f : (AlgebraicClosureAux k)[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<VAR>this : ∃ n p, map (ofStep k n) p = f<GOAL>∃ x, eval x f = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>p : (Step k n)[X]<VAR>hfm : (map (ofStep k n) p).Monic<VAR>hfi : Irreducible (map (ofStep k n) p)<GOAL>∃ x, eval x (map (ofStep k n) p) = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>p : (Step k n)[X]<VAR>hfm : p.Monic<VAR>hfi : Irreducible (map (ofStep k n) p)<GOAL>∃ x, eval x (map (ofStep k n) p) = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>p : (Step k n)[X]<VAR>hfm : p.Monic<VAR>hfi : Irreducible (map (ofStep k n) p)<VAR>this : Irreducible p<GOAL>∃ x, eval x (map (ofStep k n) p) = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>p : (Step k n)[X]<VAR>hfm : p.Monic<VAR>hfi : Irreducible (map (ofStep k n) p)<VAR>this : Irreducible p<VAR>x : Step k (n + 1)<VAR>hx : eval₂ (toStepSucc k n) x p = 0<GOAL>∃ x, eval x (map (ofStep k n) p) = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>p : (Step k n)[X]<VAR>hfm : p.Monic<VAR>hfi : Irreducible (map (ofStep k n) p)<VAR>this : Irreducible p<VAR>x : Step k (n + 1)<VAR>hx : eval₂ (toStepSucc k n) x p = 0<GOAL>eval ((ofStep k (n + 1)) x) (map (ofStep k n) p) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set M<VAR>hf : IsLocalDiffeomorphOn I J n f s<GOAL>IsLocalHomeomorphOn f s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set M<VAR>hf : IsLocalDiffeomorphOn I J n f s<GOAL>∀ x ∈ s, ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<GOAL>∃ f, (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>this : IsSymm E fun x y => 1 ≤ ‖x - y‖<GOAL>∃ f, (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>this : IsSymm E fun x y => 1 ≤ ‖x - y‖<GOAL>∀ (s : Finset E), (∀ x ∈ s, ‖x‖ ≤ R) → ∃ y, ‖y‖ ≤ R ∧ ∀ x ∈ s, 1 ≤ ‖x - y‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>this : IsSymm E fun x y => 1 ≤ ‖x - y‖<VAR>s : Finset E<GOAL>∃ y, ‖y‖ ≤ R ∧ ∀ x ∈ s, 1 ≤ ‖x - y‖
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : GroupWithZero α<VAR>s✝ t s : Set α<GOAL>0 / s ⊆ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>m n : ℕ<GOAL>(s.get? m).Terminates → (s.get? m).Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>m n m' : ℕ<VAR>a✝ : m.le m'<VAR>IH : (s.get? m').Terminates → (s.get? m).Terminates<GOAL>(s.get? m'.succ).Terminates → (s.get? m).Terminates
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>x y : M<GOAL>y ∈ span R {x} ↔ y ∈ range (toSpanSingleton R M x)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>x y : M<GOAL>y ∈ span R {x} ↔ ∃ y_1, (toSpanSingleton R M x) y_1 = y
<VAR>k m : ℕ+<GOAL>k ∣ m ↔ m.mod k = k
<VAR>k m : ℕ+<GOAL>↑k ∣ ↑m ↔ m.mod k = k
<VAR>k m : ℕ+<GOAL>↑m % ↑k = 0 ↔ m.mod k = k
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<GOAL>⋃ x, descSet hc {x} = Set.univ
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<GOAL>∀ (j : J) (x : K.obj j), lc.ι.app j { down := x } ∈ Set.univ ↔ c.ι.app j x ∈ ⋃ x, descSet hc {x}
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>j : J<VAR>x : K.obj j<GOAL>lc.ι.app j { down := x } ∈ Set.univ ↔ c.ι.app j x ∈ ⋃ x, descSet hc {x}
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>j : J<VAR>x : K.obj j<GOAL>∃ i, c.ι.app j x ∈ descSet hc {i}
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>j : J<VAR>x : K.obj j<GOAL>c.ι.app j x ∈ descSet hc {lc.ι.app j { down := x }}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>x✝ : E × F<GOAL>x✝ ∈ extremePoints 𝕜 (s ×ˢ t) ↔ x✝ ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>x✝ : E × F<VAR>hx : x✝ ∈ s ×ˢ t<VAR>h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝<GOAL>(∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1) ∧ ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>x✝ : E × F<VAR>hx : x✝ ∈ s ×ˢ t<VAR>h : (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → x✝.1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.1 ∧ x₂ = x✝.1) ∧ ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → x✝.2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝.2 ∧ x₂ = x✝.2<GOAL>∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → x✝ ∈ openSegment 𝕜 x₁ x₂ → x₁ = x✝ ∧ x₂ = x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderTop β<VAR>a b : α<VAR>f : α ≃o β<VAR>ha : Codisjoint a b<GOAL>Codisjoint (f a) (f b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderTop β<VAR>a b : α<VAR>f : α ≃o β<VAR>ha : Codisjoint a b<GOAL>f ⊤ ≤ f (a ⊔ b)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>he : autoParam (e ∈ M.E) _auto✝<GOAL>e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>he : autoParam (e ∈ M.E) _auto✝<GOAL>¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
<VAR>α : Type u_1<VAR>l : Array (Array α)<GOAL>(foldl (fun x x_1 => x ++ x_1) #[] l 0).data = (List.map data l.data).join
<VAR>α : Type u_1<VAR>l : Array (Array α)<GOAL>(List.foldl (fun x x_1 => x ++ x_1) #[] l.data).data = (List.map data l.data).join
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<VAR>hv : v ≠ 0<VAR>hr : r ≠ 0<GOAL>SameRay R (-v) (r • v) ↔ r < 0