ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<VAR>Vl : 4 / 5 * ε ≤ ↑(star hP G ε hV U).card / 4 ^ P.parts.card<VAR>this : 0 < ε<VAR>UVl : 4 / 5 * ε * (4 / 5 * ε) ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card * (↑(star hP G ε hV U).card / 4 ^ P.parts.card)<GOAL>ε ^ 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / 4 ^ 2 * ε ^ 2)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<VAR>Vl : 4 / 5 * ε ≤ ↑(star hP G ε hV U).card / 4 ^ P.parts.card<VAR>this : 0 < ε<VAR>UVl : 4 / 5 * ε * (4 / 5 * ε) ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card * (↑(star hP G ε hV U).card / 4 ^ P.parts.card)<GOAL>0 ≤ 9 / 4 ^ 2 * ε ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts<VAR>hε : 0 ≤ ε<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts<VAR>hε : 0 ≤ ε<VAR>sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts<VAR>hε : 0 ≤ ε<VAR>sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b<VAR>this : ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑((star hP G ε hU V).product (star hP G ε hV U)).card / ↑((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts).card * (3 / 4 * ε) ^ 2 ≤ (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (fun x => ↑(G.edgeDensity x.1 x.2)) i ^ 2) / ↑((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts).card<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts<VAR>hε : 0 ≤ ε<VAR>sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b<GOAL>3 / 4 * ε ≤ |(∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U), (fun x => ↑(G.edgeDensity x.1 x.2)) i) / ↑((star hP G ε hU V).product (star hP G ε hV U)).card - (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (fun x => ↑(G.edgeDensity x.1 x.2)) i) / ↑((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts).card|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts<VAR>hε : 0 ≤ ε<VAR>sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ ((∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (fun x => ↑(G.edgeDensity x.1 x.2)) i) / ↑((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts).card) ^ 2
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate n).reverse.rotate n = l.reverse
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<GOAL>𝓤 (α × β) = comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((𝓤 α).prod (𝓤 β))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<GOAL>comap (fun p => (p.1.1, p.2.1)) (𝓤 α) ⊓ comap (fun p => (p.1.2, p.2.2)) (𝓤 β) = comap (Prod.fst ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α) ⊓ comap (Prod.snd ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>h'u : range u ⊆ s<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>h'u : range u ⊆ s<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>h'u : range u ⊆ s<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>∀ (n : ℕ), 0 ≤ (fun n => ↑K * b n) n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>h'u : range u ⊆ s<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>h'u : range u ⊆ s<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>Tendsto (fun n => ↑K * b n) atTop (𝓝 0)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : T<VAR>p : T[X]<VAR>ha : a ≠ 0<GOAL>(a • p).aroots S = p.aroots S
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f✝ : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>f : ContDiffBump 0<VAR>x : E<GOAL>↑f (-x) = ↑f x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed (polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed (⋂ i ∈ s, {x | ‖x i‖ ≤ 1})
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<GOAL>powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<GOAL>powersetCard n.succ s ∪ filter (fun x => x.card = n.succ) (image (insert x) s.powerset) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<GOAL>filter (fun x => x.card = n.succ) (image (insert x) s.powerset) = image (insert x) (powersetCard n s)
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<GOAL>image (insert x) (filter (fun a => (insert x a).card = n.succ) s.powerset) = image (insert x) (filter (fun x => x.card = n) s.powerset)
<VAR>α : Type u_1<VAR>s✝¹ t✝¹ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<VAR>t : Finset α<GOAL>t ∈ filter (fun a => (insert x a).card = n.succ) s.powerset ↔ t ∈ filter (fun x => x.card = n) s.powerset
<VAR>α : Type u_1<VAR>s✝¹ t✝¹ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<VAR>t : Finset α<GOAL>t ⊆ s → ((insert x t).card = n.succ ↔ t.card = n)
<VAR>α : Type u_1<VAR>s✝¹ t✝¹ : Finset α<VAR>n✝ : ?m.21546<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<VAR>t : Finset α<VAR>ht : t ⊆ s<VAR>this : x ∉ t<GOAL>(insert x t).card = n.succ ↔ t.card = n
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : ModP K v O hv p<VAR>hvx : preVal K v O hv p x = 0<VAR>hx0 : x ≠ 0<GOAL>False
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : ModP K v O hv p<VAR>hvx : preVal K v O hv p x = 0<VAR>hx0 : v ↑p < 0<GOAL>False
<VAR>x y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>(norm x).natAbs ≤ (norm (x * y)).natAbs
<VAR>x y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>(norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>IndepFun f g μ ↔ Measure.map (fun ω => (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>(∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)) ↔ Measure.map (fun ω => (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>h₀ : ∀ {s : Set β} {t : Set β'}, MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧ μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω => (f ω, g ω)) μ) (s ×ˢ t)<GOAL>(∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)) ↔ Measure.map (fun ω => (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w w₁ w₂ : ι → k<VAR>p : ι → V<VAR>hp : AffineIndependent k p<VAR>hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i<VAR>hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i<GOAL>∀ i ∈ s, w₁ i = w₂ i
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>IsClosedImmersion f ↔ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => ClosedEmbedding) ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f) f
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>(ClosedEmbedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(Scheme.Hom.stalkMap f x)) ↔ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => ClosedEmbedding) ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f) f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ x y : E<GOAL>dist (f x) (f y) ≤ ‖f‖ * dist x y
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R✝ : Type u_3<VAR>inst✝¹ : CommSemiring R✝<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : M → ι<VAR>m : M<VAR>r : R<VAR>x : M<VAR>hx : x ∈ (Finsupp.single m r).support<GOAL>f x = f m
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>Integrable (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>Continuous fun x => -b * ↑x ^ 2
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>HasFiniteIntegral (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>this : HasFiniteIntegral (fun x => x * rexp (-b.re * x ^ 2)) volume<GOAL>HasFiniteIntegral (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>this : HasFiniteIntegral (fun a => ‖a * rexp (-b.re * a ^ 2)‖) volume<GOAL>HasFiniteIntegral (fun a => ‖↑a * cexp (-b * ↑a ^ 2)‖) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>this : HasFiniteIntegral (fun a => ‖a * rexp (-b.re * a ^ 2)‖) volume<VAR>x✝ : ℝ<GOAL>‖↑x✝ * cexp (-b * ↑x✝ ^ 2)‖ = ‖x✝ * rexp (-b.re * x✝ ^ 2)‖
<VAR>n a b : ℕ<VAR>h : n = a + b<GOAL>n.choose a = n.choose b
<VAR>n a b : ℕ<VAR>h : n = a + b<GOAL>n.choose (n - b) = n.choose b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>min a b ≤ a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<GOAL>P.toPoly.natDegree ≤ 2
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n✝ : ℕ<VAR>a : M<VAR>n : ℕ<GOAL>a ^ n * a = a * a ^ n
<VAR>n : ℕ<VAR>h : 0 < n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i
<VAR>n : ℕ<VAR>h : 0 < n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
<VAR>x : ℝ<VAR>hx0 : x < 0<VAR>hpx : -(π / 2) < x<GOAL>-x < π / 2
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖f‖ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a✝ a : α<VAR>ha : a ≠ 0<VAR>x✝¹ x✝ : α<GOAL>dist x✝¹ x✝ ≤ ↑‖a‖₊⁻¹ * dist (x✝¹ * a) (x✝ * a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K U V : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection U<VAR>h : (orthogonalProjection U).comp V.subtypeL = 0<VAR>u : E<VAR>hu : u ∈ U<VAR>v : E<VAR>hv : v ∈ V<GOAL>⟪v, u⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K U V : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection U<VAR>h : (orthogonalProjection U).comp V.subtypeL = 0<VAR>u : E<VAR>hu : u ∈ U<VAR>v : E<VAR>hv : v ∈ V<GOAL>v = v - ↑((orthogonalProjection U) v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K U V : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection U<VAR>h : (orthogonalProjection U).comp V.subtypeL = 0<VAR>u : E<VAR>hu : u ∈ U<VAR>v : E<VAR>hv : v ∈ V<VAR>this : (orthogonalProjection U) v = 0<GOAL>v = v - ↑((orthogonalProjection U) v)
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁹ : SMul M X<VAR>inst✝⁸ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝⁷ : SMul N Y<VAR>inst✝⁶ : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝⁵ : SMul P Z<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F X Y<VAR>inst✝³ : MulOneClass X<VAR>inst✝² : SMul X Y<VAR>inst✝¹ : IsScalarTower M' X Y<VAR>inst✝ : MulActionHomClass F X X Y<VAR>f : F<VAR>m : M'<VAR>x : X<GOAL>f (m • x) = id m • f x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>chainLength (-α) β = chainLength α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>IsOpen (Ico 0 b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>IsOpen (Iio b)
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F f : J → C<VAR>t : Bicone f<VAR>ht : IsLimit t.toCone<VAR>j : J<VAR>j' : Discrete J<GOAL>t.ι j ≫ t.toCone.π.app j' = ht.lift (Fan.mk (f j) fun j' => if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'