ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 : Continuous f<GOAL>Embedding f ↔ ∀ (x : ι), Embedding ((U x).carrier.restrictPreimage f)
<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 : Continuous f<GOAL>IsOpen (range f) ↔ ∀ (x : ι), IsOpen (range ((U x).carrier.restrictPreimage f))
<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>x : R<VAR>m : ↥M<GOAL>x • mk' S 1 m = mk' S x m
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>H : p ≠ 0<GOAL>p.natDegree ∈ p.support
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>H : p ≠ 0<GOAL>p.coeff p.natDegree ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DivisionMonoid α<VAR>s t : Finset α<GOAL>s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
<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>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<VAR>h : ∃ i, p i<GOAL>a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁶ : Traversable t<VAR>inst✝⁵ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>inst✝ : Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<VAR>α✝ : Type u<VAR>x✝ : t' α✝<GOAL>traverse pure x✝ = x✝
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝¹⁰ : Traversable t<VAR>inst✝⁹ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝⁸ : Applicative F<VAR>inst✝⁷ : Applicative G<VAR>inst✝⁶ : LawfulApplicative F<VAR>inst✝⁵ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>inst✝⁴ : Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<VAR>F✝ G✝ : Type u → Type u<VAR>inst✝³ : Applicative F✝<VAR>inst✝² : Applicative G✝<VAR>inst✝¹ : LawfulApplicative F✝<VAR>inst✝ : LawfulApplicative G✝<VAR>α✝ β✝ γ✝ : Type u<VAR>x✝² : β✝ → F✝ γ✝<VAR>x✝¹ : α✝ → G✝ β✝<VAR>x✝ : t' α✝<GOAL>traverse (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝¹⁰ : Traversable t<VAR>inst✝⁹ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝⁸ : Applicative F<VAR>inst✝⁷ : Applicative G<VAR>inst✝⁶ : LawfulApplicative F<VAR>inst✝⁵ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>inst✝⁴ : Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<VAR>F✝ G✝ : Type u → Type u<VAR>inst✝³ : Applicative F✝<VAR>inst✝² : Applicative G✝<VAR>inst✝¹ : LawfulApplicative F✝<VAR>inst✝ : LawfulApplicative G✝<VAR>α✝ β✝ γ✝ : Type u<VAR>x✝² : β✝ → F✝ γ✝<VAR>x✝¹ : α✝ → G✝ β✝<VAR>x✝ : t' α✝<GOAL>Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁶ : Traversable t<VAR>inst✝⁵ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>inst✝ : Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<VAR>α✝ β✝ : Type u<VAR>x✝¹ : α✝ → β✝<VAR>x✝ : t' α✝<GOAL>traverse (pure ∘ x✝¹) x✝ = id.mk (x✝¹ <$> x✝)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁶ : Traversable t<VAR>inst✝⁵ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>inst✝ : Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<VAR>α✝ β✝ : Type u<VAR>x✝¹ : α✝ → β✝<VAR>x✝ : t' α✝<GOAL>pure (Equiv.map eqv x✝¹ x✝) = id.mk (Equiv.map eqv x✝¹ x✝)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝¹⁰ : Traversable t<VAR>inst✝⁹ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝⁸ : Applicative F<VAR>inst✝⁷ : Applicative G<VAR>inst✝⁶ : LawfulApplicative F<VAR>inst✝⁵ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>inst✝⁴ : Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<VAR>F✝ G✝ : Type u → Type u<VAR>inst✝³ : Applicative F✝<VAR>inst✝² : Applicative G✝<VAR>inst✝¹ : LawfulApplicative F✝<VAR>inst✝ : LawfulApplicative G✝<VAR>x✝⁴ : ApplicativeTransformation F✝ G✝<VAR>x✝³ x✝² : Type u<VAR>x✝¹ : x✝³ → F✝ x✝²<VAR>x✝ : t' x✝³<GOAL>(fun {α} => x✝⁴.app α) (traverse x✝¹ x✝) = traverse ((fun {α} => x✝⁴.app α) ∘ x✝¹) x✝
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<GOAL>∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>this : ∀ (z : ↑Γ(X, X.basicOpen f)), ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1<GOAL>∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>this : ∀ (z : ↑Γ(X, X.basicOpen f)), ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1<VAR>y : ↑Γ(X, U)<VAR>n : ℕ<VAR>d : x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1<GOAL>∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>this : ∀ (z : ↑Γ(X, X.basicOpen f)), ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1<VAR>y : ↑Γ(X, U)<VAR>n : ℕ<VAR>d : x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1<GOAL>(y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>this : ∀ (z : ↑Γ(X, X.basicOpen f)), ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1<VAR>y : ↑Γ(X, U)<VAR>n : ℕ<VAR>d : x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1<GOAL>(X.presheaf.map (homOfLE ⋯).op) y = (X.presheaf.map (homOfLE ⋯).op) f ^ n * x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝ : CommGroupWithZero G₀<VAR>s : Finset ι<VAR>f : ι → G₀<VAR>h : ∏ i ∈ s, f i ≠ 0<GOAL>mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f ↑i) ⋯
<VAR>z : ℍ<GOAL>↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
<VAR>z : ℍ<VAR>h1 : ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) = -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))<GOAL>↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
<VAR>z : ℍ<VAR>h1 : ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) = -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))<GOAL>-↑π * I * (2 * ∑' (i : ℕ), cexp (2 * ↑π * I * ↑z) ^ i - 1) = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h₁ : b = ⊤ → a ≠ 0<VAR>h₂ : a = ⊤ → b ≠ 0<GOAL>a⁻¹ ≤ b ↔ 1 ≤ a * b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h₁ : b = ⊤ → a ≠ 0<VAR>h₂ : a = ⊤ → b ≠ 0<GOAL>a ≠ 0 ∨ b ≠ ⊤
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h₁ : b = ⊤ → a ≠ 0<VAR>h₂ : a = ⊤ → b ≠ 0<GOAL>a ≠ ⊤ ∨ b ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<VAR>bc : ¬b = c<GOAL>swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.Icc 0 1)<GOAL>IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.uIcc 0 1)<GOAL>IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<GOAL>g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>hf : Multipliable fun b => (f b)⁻¹<GOAL>Multipliable f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<GOAL>Even a ↔ 2 ∣ a
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f✝ : ℕ → α<VAR>a : α<VAR>β : α → Type u_3<VAR>f : (x : α) × β x → ℝ≥0<GOAL>(Summable fun i => ↑(f i)) ↔ (∀ (x : α), Summable fun y => (fun i => ↑(f i)) ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), (fun i => ↑(f i)) ⟨x, y⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 ≤ b<VAR>hc : 0 ≤ c<VAR>h : a ≤ c * b<GOAL>a / b ≤ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a c d e : α<VAR>m n : ℤ<VAR>hc : 0 ≤ c<VAR>hb : 0 ≤ 0<VAR>h : a ≤ c * 0<GOAL>a / 0 ≤ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 ≤ b<VAR>hc : 0 ≤ c<VAR>h : a ≤ c * b<VAR>hb' : 0 < b<GOAL>a / b ≤ c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<GOAL>⋂ l, {x | ∃ y ∈ s, l x ≤ l y} = s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<GOAL>{x | ∀ (i : E →L[ℝ] ℝ), ∃ y ∈ s, i x ≤ i y} = s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x✝ y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<VAR>x : E<VAR>hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y ∈ s, i x ≤ i y}<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x✝ y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<VAR>x : E<VAR>hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y ∈ s, i x ≤ i y}<VAR>h : x ∉ s<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsClosed s✝<VAR>x : E<VAR>hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y ∈ s✝, i x ≤ i y}<VAR>h : x ∉ s✝<VAR>l : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hlA : ∀ a ∈ s✝, l a < s<VAR>hl : s < l x<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x✝ y✝ : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsClosed s✝<VAR>x : E<VAR>hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y ∈ s✝, i x ≤ i y}<VAR>h : x ∉ s✝<VAR>l : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hlA : ∀ a ∈ s✝, l a < s<VAR>hl : s < l x<VAR>y : E<VAR>hy : y ∈ s✝<VAR>hxy : l x ≤ l y<GOAL>False
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<GOAL>PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>s : Stream'.Seq (Pair K)<VAR>inst✝ : DivisionRing K<GOAL>convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<GOAL>ContinuousAt φ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<GOAL>ContinuousAt φ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<GOAL>∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<GOAL>φ ⁻¹' V' ∈ 𝓝 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<GOAL>φ ⁻¹' V' ∈ 𝓝 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<VAR>V₂ : Set β<VAR>V₂_in : V₂ ∈ 𝓝 b<VAR>V₂_op : IsOpen V₂<VAR>hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'<GOAL>φ ⁻¹' V' ∈ 𝓝 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<VAR>V₂ : Set β<VAR>V₂_in : V₂ ∈ 𝓝 b<VAR>V₂_op : IsOpen V₂<VAR>hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'<GOAL>∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<VAR>V₂ : Set β<VAR>V₂_in : V₂ ∈ 𝓝 b<VAR>V₂_op : IsOpen V₂<VAR>hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'<VAR>x : β<VAR>x_in₁ : x ∈ V₁<VAR>x_in₂ : x ∈ V₂<GOAL>φ x ∈ V'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<VAR>V₂ : Set β<VAR>V₂_in : V₂ ∈ 𝓝 b<VAR>V₂_op : IsOpen V₂<VAR>hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'<VAR>x : β<VAR>x_in₁ : x ∈ V₁<VAR>x_in₂ : x ∈ V₂<VAR>hV₂x : V₂ ∈ 𝓝 x<GOAL>φ x ∈ V'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<VAR>V₂ : Set β<VAR>V₂_in : V₂ ∈ 𝓝 b<VAR>V₂_op : IsOpen V₂<VAR>hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'<VAR>x : β<VAR>x_in₁ : x ∈ V₁<VAR>x_in₂ : x ∈ V₂<VAR>hV₂x : V₂ ∈ 𝓝 x<GOAL>∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)<VAR>φ : β → γ := di.extend f<VAR>this : ∀ (b : β), (comap i (𝓝 b)).NeBot<VAR>V' : Set γ<VAR>V'_in : V' ∈ 𝓝 (φ b)<VAR>V'_closed : IsClosed V'<VAR>V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}<VAR>V₁_in : V₁ ∈ 𝓝 b<VAR>V₂ : Set β<VAR>V₂_in : V₂ ∈ 𝓝 b<VAR>V₂_op : IsOpen V₂<VAR>hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'<VAR>x : β<VAR>x_in₁ : x ∈ V₁<VAR>x_in₂ : x ∈ V₂<VAR>hV₂x : V₂ ∈ 𝓝 x<GOAL>V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x | (fun x => f x ∈ V') x}
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>hb : b ∈ doset a ↑H ↑K<GOAL>doset b ↑H ↑K = doset a ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a h : G<VAR>hh : h ∈ ↑H<VAR>k : G<VAR>hk : k ∈ ↑K<VAR>hb : h * a * k ∈ doset a ↑H ↑K<GOAL>doset (h * a * k) ↑H ↑K = doset a ↑H ↑K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : V<GOAL>(ofBaseChange A Q) ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x))) = (ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : t ⊆ s<VAR>hs : 𝒜.Shatters s<VAR>v : Finset α<VAR>hv : v ∈ 𝒜<VAR>hu : s ∩ v ⊆ t<GOAL>∃ u ∈ 𝒜, t ∩ u = s ∩ v