ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>hk : 1 < k<GOAL>(hasseDeriv k) X = 0
<VAR>f : ℕ → ℕ → ℕ<VAR>hf : Primrec' fun v => f v.head v.tail.head<VAR>n : ℕ<VAR>g h : Vector ℕ n → ℕ<VAR>hg : Primrec' g<VAR>hh : Primrec' h<GOAL>Primrec' fun v => f (g v) (h v)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>𝕜 : Type u_7<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : Module 𝕜 M<VAR>f : M →ₗ[𝕜] M<VAR>hf : LinearMap.det f = 0<GOAL>range f < ⊤
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>𝕜 : Type u_7<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : Module 𝕜 M<VAR>f : M →ₗ[𝕜] M<VAR>hf : LinearMap.det f = 0<VAR>this : FiniteDimensional 𝕜 M<GOAL>range f < ⊤
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>𝕜 : Type u_7<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : Module 𝕜 M<VAR>f : M →ₗ[𝕜] M<VAR>this : FiniteDimensional 𝕜 M<VAR>hf : ¬range f < ⊤<GOAL>¬LinearMap.det f = 0
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Nonempty X<VAR>inst✝¹ : MeasurableSpace X<VAR>s : Set X<VAR>inst✝ : MeasurableSpace.CountablySeparated ↑s<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hs : ∀ᵐ (x : α) ∂μ, g x ∈ s<VAR>hgm : NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<GOAL>∃ c, g =ᶠ[ae μ] const α c
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Nonempty X<VAR>inst✝¹ : MeasurableSpace X<VAR>s : Set X<VAR>inst✝ : MeasurableSpace.CountablySeparated ↑s<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hs : ∀ᵐ (x : α) ∂μ, g x ∈ s<VAR>hgm : NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<GOAL>∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Nonempty X<VAR>inst✝¹ : MeasurableSpace X<VAR>s : Set X<VAR>inst✝ : MeasurableSpace.CountablySeparated ↑s<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hs : ∀ᵐ (x : α) ∂μ, g x ∈ s<VAR>hgm : NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<VAR>U : Set X<VAR>hU : MeasurableSet U<GOAL>f ⁻¹' (g ⁻¹' U) =ᶠ[ae μ] g ⁻¹' U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Nonempty X<VAR>inst✝¹ : MeasurableSpace X<VAR>s : Set X<VAR>inst✝ : MeasurableSpace.CountablySeparated ↑s<VAR>f : α → α<VAR>g : α → X<VAR>h : QuasiErgodic f μ<VAR>hs : ∀ᵐ (x : α) ∂μ, g x ∈ s<VAR>hgm : NullMeasurable g μ<VAR>hg_eq : g ∘ f =ᶠ[ae μ] g<VAR>U : Set X<VAR>hU : MeasurableSet U<VAR>x : α<VAR>hx : (g ∘ f) x = g x<GOAL>x ∈ f ⁻¹' (g ⁻¹' U) ↔ x ∈ g ⁻¹' U
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t s : Set α<VAR>ht : NullMeasurableSet t μ<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_1<VAR>inst✝¹ : AddCommGroupWithOne α<VAR>inst✝ : CharZero α<VAR>a b : ℤ<VAR>n : ℕ<GOAL>↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (sinh ↑x) = sinh ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s'✝ : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>s' : Set α<GOAL>(𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : D<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>hB : ‖B‖ ≤ 1<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : D<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>hB : ‖B‖ ≤ 1<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) univ x‖ ≤ ∑ x_1 ∈ Finset.range (n + 1), ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).Ψ₃ = Polynomial.map (↑f) (W.baseChange A).Ψ₃
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>(𝓝 x).lift g = (𝓤 α).lift fun s => g (ball x s)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>(𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun s => g (ball x s)
<VAR>R : Type u<VAR>ι : Type v<VAR>n : ℕ<VAR>M : Fin n.succ → Type w<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>M₄ : Type w₄<VAR>inst✝¹⁸ : Semiring R<VAR>inst✝¹⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹⁴ : AddCommMonoid M₂<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>inst✝¹² : AddCommMonoid M₄<VAR>inst✝¹¹ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝¹⁰ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁹ : (i : ι) → Module R (M₁' i)<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : Module R M₃<VAR>inst✝⁶ : Module R M₄<VAR>inst✝⁵ : (i : Fin n.succ) → TopologicalSpace (M i)<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)<VAR>inst✝³ : (i : ι) → TopologicalSpace (M₁' i)<VAR>inst✝² : TopologicalSpace M₂<VAR>inst✝¹ : TopologicalSpace M₃<VAR>inst✝ : TopologicalSpace M₄<VAR>f✝ f'✝ f f' : ContinuousMultilinearMap R M₁ M₂<GOAL>f = f' ↔ ∀ (x : (i : ι) → M₁ i), f x = f' x
<VAR>R : Type u<VAR>ι : Type v<VAR>n : ℕ<VAR>M : Fin n.succ → Type w<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>M₄ : Type w₄<VAR>inst✝¹⁸ : Semiring R<VAR>inst✝¹⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹⁴ : AddCommMonoid M₂<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>inst✝¹² : AddCommMonoid M₄<VAR>inst✝¹¹ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝¹⁰ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁹ : (i : ι) → Module R (M₁' i)<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : Module R M₃<VAR>inst✝⁶ : Module R M₄<VAR>inst✝⁵ : (i : Fin n.succ) → TopologicalSpace (M i)<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)<VAR>inst✝³ : (i : ι) → TopologicalSpace (M₁' i)<VAR>inst✝² : TopologicalSpace M₂<VAR>inst✝¹ : TopologicalSpace M₃<VAR>inst✝ : TopologicalSpace M₄<VAR>f✝ f'✝ f f' : ContinuousMultilinearMap R M₁ M₂<GOAL>(∀ (x : (i : ι) → M₁ i), f.toMultilinearMap x = f'.toMultilinearMap x) ↔ ∀ (x : (i : ι) → M₁ i), f x = f' x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m m₁ m₂ : Multiset α<VAR>h : m₁.toEnumFinset ⊆ m₂.toEnumFinset<GOAL>m₁ ≤ m₂
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<VAR>C : VariableChange R<GOAL>{ a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s), a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2), a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t), a₄ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 * (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 - 2 * φ C.s * φ C.t), a₆ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 * (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 - φ C.r * φ C.t * φ W.a₁) } = { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)), a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)), a₄ := φ (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)), a₆ := φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>a : Set α<VAR>σ✝ : Type u_5<VAR>F✝ : CFilter (Set α) σ✝<GOAL>a ∈ F✝.toFilter ↔ ∃ b, { σ := σ✝, F := F✝, eq := ⋯ }.F.f b ⊆ a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r✝ : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>r : ι → ι → Prop<VAR>hwf : WellFounded r<VAR>x y : (i : ι) → β i<VAR>hlt : x < y<GOAL>Pi.Lex r (fun i x x_1 => x < x_1) x y
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r✝ : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>r : ι → ι → Prop<VAR>hwf : WellFounded r<VAR>x y : (i : ι) → β i<VAR>hlt : x < y<GOAL>∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>a % 0 = a
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>C.dTo j = (C.xPrevIso r).hom ≫ C.d i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>j : ι<VAR>r : c.Rel (c.prev j) j<GOAL>C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j
<GOAL>StrictConcaveOn ℝ (Icc 0 π) sin
<VAR>x : ℝ<VAR>hx : x ∈ interior (Icc 0 π)<GOAL>deriv^[2] sin x < 0
<VAR>x : ℝ<VAR>hx : x ∈ Ioo 0 π<GOAL>deriv^[2] sin x < 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<GOAL>ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<GOAL>(∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔ ∀ (a : X) (b : Y), (a, b) ∈ Prod.map mk mk ⁻¹' s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R<VAR>n : ℕ<GOAL>(C a).divX.coeff n = coeff 0 n
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>(M ↾ R).Basis I X ↔ M.Basis I (X ∩ M.E) ∧ X ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>X ⊆ R → (M.Basis' I (X ∩ R) ∧ I ⊆ R ↔ M.Basis' I X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hXR : X ⊆ R<GOAL>M.Basis' I (X ∩ R) ∧ I ⊆ R ↔ M.Basis' I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hXR : X ⊆ R<GOAL>M.Basis' I X → I ⊆ R
<VAR>α : Type u_1<VAR>p : PosNum<VAR>this : (↑p).bit0 = (ZNum.pos p).bit0<GOAL>↑p.bit0 = ZNum.pos p.bit0
<VAR>α : Type u_1<VAR>p : PosNum<VAR>this : (↑p).bit1 = (ZNum.pos p).bit1<GOAL>↑p.bit1 = ZNum.pos p.bit1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atBot.IsMeasurablyGenerated<VAR>inst✝ : OrderTop α<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atBot.IsMeasurablyGenerated<VAR>inst✝ : OrderTop α<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<GOAL>StronglyMeasurableAtFilter f atBot μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l✝ l' la : Filter α<VAR>lb l : Filter β<VAR>f : α → β<GOAL>(comap f l).smallSets = comap (image f) l.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l✝ l' la : Filter α<VAR>lb l : Filter β<VAR>f : α → β<GOAL>∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟
<VAR>m n : Num<GOAL>m ∣ n ↔ n % m = 0
<VAR>m n : Num<GOAL>↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β✝ : Type u_7<VAR>inst✝¹ : SeminormedAddCommGroup β✝<VAR>T✝ T' : Set α → β✝<VAR>C✝ C' : ℝ<VAR>β : Type u_8<VAR>inst✝ : NormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs_zero : μ s = 0<GOAL>T s = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β✝ : Type u_7<VAR>inst✝¹ : SeminormedAddCommGroup β✝<VAR>T✝ T' : Set α → β✝<VAR>C✝ C' : ℝ<VAR>β : Type u_8<VAR>inst✝ : NormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs_zero : μ s = 0<GOAL>‖T s‖ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β✝ : Type u_7<VAR>inst✝¹ : SeminormedAddCommGroup β✝<VAR>T✝ T' : Set α → β✝<VAR>C✝ C' : ℝ<VAR>β : Type u_8<VAR>inst✝ : NormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs_zero : μ s = 0<GOAL>C * (μ s).toReal = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<GOAL>Disjoint (univ.pi fun i => Ioc (x i) (update y i₀ m i)) (univ.pi fun i => Ioc (update x i₀ m i) (y i))
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<GOAL>∀ ⦃a : (i : ι) → α i⦄, (a ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)) → a ∉ univ.pi fun i => Ioc (update x i₀ m i) (y i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>z : (i : ι) → α i<VAR>h₁ : z ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)<VAR>h₂ : z ∈ univ.pi fun i => Ioc (update x i₀ m i) (y i)<GOAL>False
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>z : (i : ι) → α i<VAR>h₁ : z ∈ univ.pi fun i => Ioc (x i) (update y i₀ m i)<VAR>h₂ : z ∈ univ.pi fun i => Ioc (update x i₀ m i) (y i)<GOAL>update y i₀ m i₀ < z i₀
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>o.card = ↑n ↔ o = ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>ha' : 0 < a<VAR>hb' : 0 < b<GOAL>a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>ha' : 0 < a<VAR>hb' : 0 < b<VAR>hy : x ∈ s<GOAL>a • x + b • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>ha' : 0 < a<VAR>hb' : 0 < b<VAR>hxy : x ≠ y<GOAL>a • x + b • y ∈ s
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<VAR>hx : x ∈ C0 C ho<VAR>i : I<GOAL>Proj (fun x => ord I x < o) x i = x i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<VAR>hx : x ∈ C0 C ho<VAR>i : I<GOAL>o ≤ ord I i → false = x i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<VAR>hx : x ∈ C0 C ho<VAR>i : I<VAR>hi : o ≤ ord I i<GOAL>false = x i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<VAR>hx : x ∈ C0 C ho<VAR>i : I<VAR>hi : o < ord I i ∨ o = ord I i<GOAL>false = x i
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>𝔸 : Type u_3<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝔸<VAR>inst✝³ : NormedCommRing 𝔸'<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>inst✝¹ : NormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x<GOAL>ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h : 0 < n<GOAL>∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h : 0 < n<VAR>a₁ b₁ : ℕ<VAR>ha₁ : 0 < a₁<VAR>hb₁ : 0 < b₁<VAR>hab₁ : b₁ ^ 2 * a₁ = n<VAR>hab₂ : Squarefree a₁<GOAL>∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w x y : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).support.tail ~r c.support.tail
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w x y : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>((c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail) ~r c.support.tail
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w x y : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>((c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail) ~r c.support.tail