ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>inst✝¹ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp₁ : p ≠ 2<VAR>hp₂ : ringChar F ≠ p<VAR>h : (quadraticChar F) ↑(Fintype.card (ZMod p)) = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))<GOAL>(quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝⁴ : DecidableEq ι<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : DecidableEq M<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubmonoidClass S M<VAR>A : ι → S<VAR>x : ⨁ (i : ι), ↥(A i)<GOAL>(DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x => ↑x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝⁴ : DecidableEq ι<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : DecidableEq M<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubmonoidClass S M<VAR>A : ι → S<VAR>x : ⨁ (i : ι), ↥(A i)<GOAL>(DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x
<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>p : ℕ<VAR>hp : p ∈ filter Nat.Prime (Ico (m + 1) (m + n + 1))<GOAL>p ∣ (m + n).choose m
<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>p : ℕ<VAR>hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p<GOAL>p ∣ (m + n).choose m
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>S : Type v<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P✝ : Ideal S<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsNoetherian R S<VAR>inst✝ : p.IsMaximal<VAR>P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }<GOAL>inertiaDeg (algebraMap R S) p ↑P ≠ 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>S : Type v<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P✝ : Ideal S<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsNoetherian R S<VAR>inst✝ : p.IsMaximal<VAR>P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }<GOAL>finrank (R ⧸ p) (S ⧸ ↑P) ≠ 0
<VAR>ι : Type u<VAR>γ✝ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>γ : Type w<VAR>α : Type x<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>s : Finset α<VAR>g : α → Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<GOAL>∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<GOAL>u ~[l] 0 ↔ u =ᶠ[l] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<GOAL>u =o[l] 0 ↔ u =ᶠ[l] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>this : Fact (m ≤ m0)<GOAL>↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>this : Fact (m ≤ m0)<VAR>h_mem : indicatorConstLp 2 ⋯ hμs c ∈ lpMeas E 𝕜 m 2 μ<GOAL>↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>this : Fact (m ≤ m0)<VAR>h_mem : indicatorConstLp 2 ⋯ hμs c ∈ lpMeas E 𝕜 m 2 μ<VAR>ind : ↥(lpMeas E 𝕜 m 2 μ) := ⟨indicatorConstLp 2 ⋯ hμs c, h_mem⟩<VAR>h_coe_ind : ↑ind = indicatorConstLp 2 ⋯ hμs c<GOAL>↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>this : Fact (m ≤ m0)<VAR>h_mem : indicatorConstLp 2 ⋯ hμs c ∈ lpMeas E 𝕜 m 2 μ<VAR>ind : ↥(lpMeas E 𝕜 m 2 μ) := ⟨indicatorConstLp 2 ⋯ hμs c, h_mem⟩<VAR>h_coe_ind : ↑ind = indicatorConstLp 2 ⋯ hμs c<VAR>h_orth_mem : (orthogonalProjection (lpMeas E 𝕜 m 2 μ)) ↑ind = ind<GOAL>↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Multiset α<VAR>l : List α<GOAL>(map f (Quot.mk Setoid.r l)).dedup = map f (dedup (Quot.mk Setoid.r l))
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hb0 : b ≠ 0 ∨ c ≠ ⊤<VAR>hbt : b ≠ ⊤ ∨ c ≠ 0<GOAL>a / b ≤ c ↔ a ≤ c * b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hb0 : b ≠ 0 ∨ c ≠ ⊤<VAR>hbt : b ≠ ⊤ ∨ c ≠ 0<GOAL>a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℤ<GOAL>padicNorm p ↑m < 1 ↔ ↑p ∣ m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℤ<GOAL>¬padicNorm p ↑m < 1 ↔ padicNorm p ↑m ≤ 1 ∧ ¬padicNorm p ↑m < 1
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>H : Subgroup Gˣ<VAR>x : G<GOAL>x ∈ H.ofUnits ↔ toUnits x ∈ H
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>a : R<GOAL>eval₂ (C.comp f) X ((monomial n) a) = (monomial n) (f a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>a : R<GOAL>(C.comp f) a * X ^ n = C (f a) * X ^ n
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>F : Type u_2<VAR>inst✝ : Field F<VAR>f : F[X]<VAR>hu : ¬IsUnit f<VAR>hf : ¬f = 0<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>F : Type u_2<VAR>inst✝ : Field F<VAR>f : F[X]<VAR>hu : ¬IsUnit f<VAR>hf✝ : ¬f = 0<VAR>g : F[X]<VAR>hi : Irreducible g<VAR>hf : g ∣ f<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>F : Type u_2<VAR>inst✝ : Field F<VAR>f : F[X]<VAR>hu : ¬IsUnit f<VAR>hf✝ : ¬f = 0<VAR>g : F[X]<VAR>hi : Irreducible g<VAR>hf : g ∣ f<VAR>ha : Associated g (g * C g.leadingCoeff⁻¹)<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>p : LTSeries β<VAR>f : α → β<VAR>comap : ∀ ⦃x y : α⦄, f x < f y → x < y<VAR>surjective : Function.Surjective f<VAR>i j : Fin (p.length + 1)<VAR>h : i < j<GOAL>f ((fun i => ⋯.choose) i) < f ((fun i => ⋯.choose) j)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : TangentBundle I H<GOAL>↑(chartAt (ModelProd H E) p) = ⇑(TotalSpace.toProd H E)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : TangentBundle I H<GOAL>↑(TotalSpace.toProd H E).toPartialEquiv = ⇑(TotalSpace.toProd H E)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>G'.Adj (f u) (f v)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>f u ∈ ⇑f '' H.verts
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>Relation.Map H.Adj (⇑f) (⇑f) (f v) (f u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α × β → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α × β → E<VAR>hf : StronglyMeasurable (uncurry (Function.curry f))<GOAL>StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Ioc a b) = Ioc ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Ioc ↑a ↑b)) = Ioc ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : x ∈ Ioc ↑a ↑b<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : ↑a < x ∧ x ≤ ↑b<GOAL>p x
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<GOAL>∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<GOAL>∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>this : ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ gauge s x<GOAL>∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<GOAL>∀ (x : ↥f.domain), ↑f x ≤ gauge s ↑x
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>x : E<VAR>hx : x ∈ f.domain<GOAL>↑f ⟨x, hx⟩ ≤ gauge s ↑⟨x, hx⟩
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>y : ℝ<VAR>hx : y • x₀ ∈ f.domain<GOAL>↑f ⟨y • x₀, hx⟩ ≤ gauge s ↑⟨y • x₀, hx⟩
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>y : ℝ<VAR>hx : y • x₀ ∈ f.domain<GOAL>y • 1 ≤ gauge s ↑⟨y • x₀, hx⟩
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>y : ℝ<VAR>hx : y • x₀ ∈ f.domain<GOAL>y ≤ gauge s (y • x₀)
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>y : ℝ<VAR>hx : y • x₀ ∈ f.domain<VAR>h : y ≤ 0<GOAL>y ≤ gauge s (y • x₀)
<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 : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<VAR>f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯<VAR>y : ℝ<VAR>hx : y • x₀ ∈ f.domain<VAR>h : 0 < y<GOAL>y ≤ gauge s (y • x₀)
<VAR>p q r : ℕ+<VAR>hpq : p ≤ q<VAR>hqr : q ≤ r<VAR>H : 1 < sumInv {p, q, r}<VAR>h3 : 0 < 3<GOAL>p < 3
<VAR>p q r : ℕ+<VAR>hpq : p ≤ q<VAR>hqr : q ≤ r<VAR>h3 : 0 < 3<VAR>H : 3 ≤ p<GOAL>sumInv {p, q, r} ≤ 1
<VAR>p q r : ℕ+<VAR>hpq : p ≤ q<VAR>hqr : q ≤ r<VAR>h3 : 0 < 3<VAR>H : 3 ≤ p<GOAL>(↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
<VAR>p q r : ℕ+<VAR>hpq : p ≤ q<VAR>hqr : q ≤ r<VAR>h3 : 0 < 3<VAR>H : 3 ≤ p<VAR>h3q : 3 ≤ q<VAR>h3r : 3 ≤ r<VAR>hp : (↑↑p)⁻¹ ≤ 3⁻¹<VAR>hq : (↑↑q)⁻¹ ≤ 3⁻¹<VAR>hr : (↑↑r)⁻¹ ≤ 3⁻¹<GOAL>(↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>init n (m • x) = init n (m • init n x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>f : R →+* S<VAR>s : Subring R<GOAL>comap f (map f s) = s ⊔ closure (⇑f ⁻¹' {0})
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>f : R →+* S<VAR>s : Subring R<GOAL>comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>f : R →+* S<VAR>s : Subring R<GOAL>s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (map f s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : GroupWithZero α<VAR>s t : Set α<VAR>hs : s.Nonempty<GOAL>0 ⊆ s / 0
<VAR>J : Type u'<VAR>inst✝¹ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<VAR>U : (Opens ↑↑(F.obj j₃))ᵒᵖ<GOAL>(F.map (f ≫ g)).c.app U = (F.map g).c.app U ≫ ((pushforward C (F.map g).base).map (F.map f).c).app U ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>↑f ⊔ ↑g ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>2⁻¹ • (↑f + ↑g + |↑g - ↑f|) ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>|↑g - ↑f| ∈ A.topologicalClosure
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Add α<VAR>inst✝² : Add α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : AddHomClass F α α₂<VAR>f : F<VAR>x y : β[α]<GOAL>mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Add α<VAR>inst✝² : Add α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : AddHomClass F α α₂<VAR>f : F<VAR>x y : β[α]<GOAL>(sum x fun a b => sum y fun a_1 b_1 => single (f a + f a_1) (b * b_1)) = sum (mapDomain (⇑f) x) fun a₁ b₁ => sum (mapDomain (⇑f) y) fun a₂ b₂ => single (a₁ + a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Add α<VAR>inst✝² : Add α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : AddHomClass F α α₂<VAR>f : F<VAR>x y : β[α]<GOAL>(sum x fun a b => sum y fun a_1 b_1 => single (f a + f a_1) (b * b_1)) = sum x fun a m => sum (mapDomain (⇑f) y) fun a₂ b₂ => single (f a + a₂) (m * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Add α<VAR>inst✝² : Add α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : AddHomClass F α α₂<VAR>f : F<VAR>x y : β[α]<GOAL>∀ (b : α₂), (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b + a₂) (0 * b₂)) = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Add α<VAR>inst✝² : Add α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : AddHomClass F α α₂<VAR>f : F<VAR>x y : β[α]<GOAL>∀ (b : α₂) (m₁ m₂ : β), (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b + a₂) ((m₁ + m₂) * b₂)) = (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b + a₂) (m₁ * b₂)) + sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b + a₂) (m₂ * b₂)
<GOAL>2 ^ 32 ≤ 2 ^ System.Platform.numBits
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>(o.oangle (-x) y).sign = -(o.oangle x y).sign
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<GOAL>((forget₂ C Ab).map (S.X₁.d j k)) x₁ = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<VAR>this : Mono S.f<GOAL>((forget₂ C Ab).map (S.X₁.d j k)) x₁ = 0