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>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<VAR>hp : p ∈ support R M<GOAL>annihilator R M ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<VAR>hp : p ∈ support R M<VAR>m : M<VAR>hm : (Submodule.span R {m}).annihilator ≤ p.asIdeal<GOAL>annihilator R M ≤ p.asIdeal
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<GOAL>(fun s => ↑((haarContent K₀).toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑((haarContent K₀).toFun s)) K
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>image (fun s => s.erase a) (filter (fun s => a ∈ s) (𝒜 ∩ ℬ)) = image (fun s => s.erase a) (filter (fun s => a ∈ s) 𝒜) ∩ image (fun s => s.erase a) (filter (fun s => a ∈ s) ℬ)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>↑(filter (fun s => a ∈ s) 𝒜) ∪ ↑(filter (fun s => a ∈ s) ℬ) ⊆ {s | a ∈ s}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>ι : Type u_1<VAR>f : ι → R<GOAL>⨆ i, basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>ι : Type u_1<VAR>f : ι → R<GOAL>⋃ i, ↑(basicOpen (f i)) = ↑⊤ ↔ Ideal.span (Set.range f) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>ι : Type u_1<VAR>f : ι → R<GOAL>(zeroLocus (⋃ i, {f i}))ᶜ = Set.univ ↔ Ideal.span (Set.range f) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>ι : Type u_1<VAR>f : ι → R<GOAL>zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (z * x + y)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (y + z * x)<GOAL>IsCoprime x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a c d : α<VAR>n : ℤ<GOAL>1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : 0 < b<GOAL>1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Finite α<GOAL>IsCyclic α ↔ ∃ g, orderOf g = Nat.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Finite α<VAR>h : ∃ g, orderOf g = Nat.card α<GOAL>IsCyclic α
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Finite α<VAR>g : α<VAR>hg : orderOf g = Nat.card α<GOAL>IsCyclic α
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Finite α<VAR>g : α<VAR>hg : orderOf g = Nat.card α<VAR>val✝ : Fintype α<GOAL>IsCyclic α
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Finite α<VAR>g : α<VAR>hg : orderOf g = Nat.card α<VAR>val✝ : Fintype α<GOAL>orderOf g = Fintype.card α
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t : ℝ<VAR>ht : 0 ≤ t<VAR>x : E<GOAL>‖t • x‖ = t * ‖x‖
<VAR>A B : CommRingCat<VAR>f : A ⟶ B<VAR>M : ModuleCat ↑B<VAR>D : M.Derivation f<VAR>b : ↑B<VAR>this✝ : Algebra ↑A ↑B := RingHom.toAlgebra f<VAR>this : Module ↑A ↑M := Module.compHom (↑M) f<GOAL>D.desc (CommRingCat.KaehlerDifferential.d b) = D.d b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>hf : IntegrableAtFilter f l μ<VAR>hg : IntegrableAtFilter g l μ<GOAL>IntegrableAtFilter (f - g) l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>hf : IntegrableAtFilter f l μ<VAR>hg : IntegrableAtFilter g l μ<GOAL>IntegrableAtFilter (f + -g) l μ
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n✝ : ℕ<VAR>x : M<VAR>hn : 0 < n✝<VAR>h : x < 1<VAR>n : ℕ<VAR>x✝ : Nat.succ 0 ≤ n<VAR>ih : x ^ n < 1<GOAL>x ^ (n + 1) < 1
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n✝ : ℕ<VAR>x : M<VAR>hn : 0 < n✝<VAR>h : x < 1<VAR>n : ℕ<VAR>x✝ : Nat.succ 0 ≤ n<VAR>ih : x ^ n < 1<GOAL>x ^ n * x < 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>U : ι → Set X<VAR>hU : ∀ i ∈ t, IsOpen (U i)<VAR>hsC : s ⊆ ⋃ i ∈ t, U i<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>ι : Type u_3<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hU : ∀ i ∈ ∅, IsOpen (U i)<VAR>hsC : s ⊆ ⋃ i ∈ ∅, U i<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ ∅, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x✝ y : X<VAR>ι : Type u_3<VAR>x : ι<VAR>t : Finset ι<VAR>hx : x ∉ t<VAR>ih : ∀ {s : Set X}, IsCompact s → ∀ (U : ι → Set X), (∀ i ∈ t, IsOpen (U i)) → s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hU : ∀ i ∈ insert x t, IsOpen (U i)<VAR>hsC : s ⊆ ⋃ i ∈ insert x t, U i<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x✝ y : X<VAR>ι : Type u_3<VAR>x : ι<VAR>t : Finset ι<VAR>hx : x ∉ t<VAR>ih : ∀ {s : Set X}, IsCompact s → ∀ (U : ι → Set X), (∀ i ∈ t, IsOpen (U i)) → s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hU : ∀ i ∈ insert x t, IsOpen (U i)<VAR>hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x✝ y : X<VAR>ι : Type u_3<VAR>x : ι<VAR>t : Finset ι<VAR>hx : x ∉ t<VAR>ih : ∀ {s : Set X}, IsCompact s → ∀ (U : ι → Set X), (∀ i ∈ t, IsOpen (U i)) → s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x<VAR>hU : IsOpen (U x) ∧ ∀ x ∈ t, IsOpen (U x)<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x✝ y : X<VAR>ι : Type u_3<VAR>x : ι<VAR>t : Finset ι<VAR>hx : x ∉ t<VAR>ih : ∀ {s : Set X}, IsCompact s → ∀ (U : ι → Set X), (∀ i ∈ t, IsOpen (U i)) → s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x<VAR>hU : IsOpen (U x) ∧ ∀ x ∈ t, IsOpen (U x)<VAR>hU' : ∀ i ∈ t, IsOpen (U i)<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x✝ y : X<VAR>ι : Type u_3<VAR>x : ι<VAR>t : Finset ι<VAR>hx : x ∉ t<VAR>ih : ∀ {s : Set X}, IsCompact s → ∀ (U : ι → Set X), (∀ i ∈ t, IsOpen (U i)) → s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x<VAR>hU : IsOpen (U x) ∧ ∀ x ∈ t, IsOpen (U x)<VAR>hU' : ∀ i ∈ t, IsOpen (U i)<VAR>K₁ K₂ : Set X<VAR>h1K₁ : IsCompact K₁<VAR>h1K₂ : IsCompact K₂<VAR>h2K₁ : K₁ ⊆ U x<VAR>h2K₂ : K₂ ⊆ ⋃ i ∈ fun i => i ∈ t.val, U i<VAR>hK : s = K₁ ∪ K₂<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
<VAR>x✝ y x : ℂ<VAR>hx : cos x ≠ 0<GOAL>tan x * cos x = sin x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f f' : StructuredArrow S T<VAR>g : f.right ⟶ f'.right<VAR>w : autoParam (f.hom ≫ T.map g = f'.hom) _auto✝<GOAL>𝟙 S ≫ f'.hom = f.hom ≫ T.map g
<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>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>S : Set ι<GOAL>induced S.restrict topologicalSpace = ⨅ i ∈ S, induced (eval i) (T i)
<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>⊥ < ker 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>⊥ < ker 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 : ¬⊥ < ker f<GOAL>¬LinearMap.det f = 0
<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 : IsUnit f<GOAL>¬LinearMap.det f = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hs : ∀ f ∈ s, Continuous f<VAR>c : Chain α<GOAL>(sSup s) (ωSup c) = ωSup (c.map (sSup s))
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hs : ∀ f ∈ s, Continuous f<VAR>c : Chain α<GOAL>∀ (c_1 : β), (sSup s) (ωSup c) ≤ c_1 ↔ ωSup (c.map (sSup s)) ≤ c_1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hs : ∀ f ∈ s, Continuous f<VAR>c : Chain α<VAR>z : β<GOAL>(sSup s) (ωSup c) ≤ z ↔ ωSup (c.map (sSup s)) ≤ z
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hs : ∀ f ∈ s, Continuous f<VAR>c : Chain α<VAR>z : β<GOAL>(∀ f ∈ s, ∀ (n : ℕ), f (c n) ≤ z) ↔ ∀ (n : ℕ), ∀ f ∈ s, f (c n) ≤ z
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x ^ 2 - a * y ^ 2<GOAL>↑p ∣ x ∧ ↑p ∣ y
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ℤ<VAR>hxy : ↑(x ^ 2 - a * y ^ 2) = 0<GOAL>↑x = 0 ∧ ↑y = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ℤ<VAR>hxy : ↑x ^ 2 - ↑a * ↑y ^ 2 = 0<GOAL>↑x = 0 ∧ ↑y = 0
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype p<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : CommSemigroup R<VAR>A : Matrix m n R<VAR>B : Matrix n m R<GOAL>(A * B).trace = (B * A).trace
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : β → γ<VAR>F : Filter α<VAR>G : Filter β<GOAL>F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<GOAL>Measurable fun p => fderiv 𝕜 (f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<VAR>s : Set (E →L[𝕜] F)<VAR>hs : IsClosed s<GOAL>MeasurableSet ((fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<VAR>s : Set (E →L[𝕜] F)<VAR>hs : IsClosed s<VAR>this : (fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s = {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪ {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}<GOAL>MeasurableSet ((fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<VAR>s : Set (E →L[𝕜] F)<VAR>hs : IsClosed s<VAR>this : (fun p => fderiv 𝕜 (f p.1) p.2) ⁻¹' s = {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪ {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}<GOAL>MeasurableSet ({p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪ {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s})
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>x y z : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = {k, m, n}
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>x y z : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>{k, m, n} ⊆ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support
<VAR>f✝ f g : ℝ → ℝ<VAR>hg : GrowsPolynomially g<VAR>hf : f ~[atTop] g<VAR>this : f = g + (f - g)<GOAL>GrowsPolynomially (g + (f - g))
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>degree 1 ≤ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>(C 1).degree ≤ 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>z₃ : Cochain K L n₃<VAR>h₁₂ : n₁ + n₂ = n₁₂<VAR>h₂₃ : n₂ + n₃ = n₂₃<VAR>h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃<GOAL>n₁ + n₂₃ = n₁₂₃
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₃ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>z₃ : Cochain K L n₃<VAR>p q : ℤ<VAR>hpq : p + (n₁ + n₂ + n₃) = q<GOAL>((z₁.comp z₂ ⋯).comp z₃ ⋯).v p q hpq = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<GOAL>x ^ y ≤ x ^ z ↔ z ≤ y
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<VAR>v : V<GOAL>⊤.degree v = Fintype.card V - 1
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x : ↑F F.M<GOAL>x.fst = (M.mk x).dest.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>K ⊓ Kᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>K ⊓ Kᗮ ≤ ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x : E<GOAL>x ∈ K ⊓ Kᗮ → x ∈ ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x : E<GOAL>x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball x δ / s = x • thickening δ s⁻¹
<VAR>G : Type u<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝¹ : Monoid M₁<VAR>inst✝ : Monoid M₂<GOAL>exponent (M₁ × M₂) = GCDMonoid.lcm (exponent M₁) (exponent M₂)
<VAR>G : Type u<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝¹ : Monoid M₁<VAR>inst✝ : Monoid M₂<GOAL>exponent (M₁ × M₂) ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
<VAR>G : Type u<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝¹ : Monoid M₁<VAR>inst✝ : Monoid M₂<GOAL>exponent M₁ ∣ exponent (M₁ × M₂)
<VAR>G : Type u<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝¹ : Monoid M₁<VAR>inst✝ : Monoid M₂<GOAL>exponent M₂ ∣ exponent (M₁ × M₂)
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<VAR>h : c < ℵ₀<GOAL>succ c = c + 1
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<VAR>h : c < ℵ₀<VAR>n : ℕ<VAR>hn : c = ↑n<GOAL>succ c = c + 1
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<GOAL>interior t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' interior s
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<GOAL>⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' interior t ⊆ interior s
<VAR>f : ℝ → ℝ<VAR>hf : GrowsPolynomially f<GOAL>(∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝ : HasColimit (E ⋙ F)<VAR>k : K<GOAL>ι (E ⋙ F) k ≫ pre F E = ι F (E.obj k)
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝ : HasColimit (E ⋙ F)<VAR>k : K<GOAL>(Cocone.whisker E (cocone F)).ι.app k = ι F (E.obj k)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<GOAL>IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>εa : α<VAR>εa0 : εa > 0<VAR>ia : ℕ<VAR>ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j<VAR>εb : α<VAR>εb0 : εb > 0<VAR>ib : ℕ<VAR>hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j<GOAL>a ⊔ b < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>εa : α<VAR>εa0 : εa > 0<VAR>ia : ℕ<VAR>ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j<VAR>εb : α<VAR>εb0 : εb > 0<VAR>ib : ℕ<VAR>hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j<VAR>i : ℕ<VAR>hi : i ≥ ia ⊔ ib<GOAL>εa ⊓ εb ≤ ↑(c - a ⊔ b) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>εa : α<VAR>εa0 : εa > 0<VAR>ia : ℕ<VAR>ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j<VAR>εb : α<VAR>εb0 : εb > 0<VAR>ib : ℕ<VAR>hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j<VAR>i : ℕ<VAR>hi : i ≥ ia ⊔ ib<VAR>this : min εa εb ≤ min (↑(c - a) i) (↑(c - b) i)<GOAL>εa ⊓ εb ≤ ↑(c - a ⊔ b) i
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>r : M₀<GOAL>inverse r ^ 0 = inverse (r ^ 0)