ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>inst✝¹² : Monoid R<VAR>inst✝¹¹ : Monoid S<VAR>inst✝¹⁰ : Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : DistribMulAction R A<VAR>inst✝⁷ : NonUnitalNonAssocSemiring B<VAR>inst✝⁶ : DistribMulAction S B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : DistribMulAction T C<VAR>φ' : S →* R<VAR>ψ : S →* T<VAR>χ : R →* T<VAR>B₁ : Type u_2<VAR>inst✝³ : NonUnitalNonAssocSemiring B₁<VAR>inst✝² : DistribMulAction R B₁<VAR>inst✝¹ : DistribMulAction R B<VAR>inst✝ : DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<VAR>c : R<VAR>x : A<GOAL>Pi.prod (⇑f) (⇑g) (c • x) = (MonoidHom.id R) c • Pi.prod (⇑f) (⇑g) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0<VAR>hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0<GOAL>f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0<VAR>hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0<GOAL>(∀ j ∈ filter (fun x => w x ≠ 0) t, p j = ∑ i ∈ filter (fun x => w x ≠ 0) t, w i • p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ x ∈ filter (fun x => w x ≠ 0) t, w x • p x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0<VAR>hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0<GOAL>∀ i ∈ filter (fun x => w x ≠ 0) t, 0 < w i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0<VAR>hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0<GOAL>∑ i ∈ filter (fun x => w x ≠ 0) t, w i = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0<VAR>hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0<GOAL>∀ i ∈ filter (fun x => w x ≠ 0) t, p i ∈ s
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>i : Fin n<GOAL>predAbove 0 i.succ = i
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ+<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F R R<VAR>inst✝ : RingHomClass F R R<VAR>σ : F<VAR>ζ : ↥(rootsOfUnity k R)<GOAL>∃ m, σ ↑↑ζ = ↑↑ζ ^ m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ+<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F R R<VAR>inst✝ : RingHomClass F R R<VAR>σ : F<VAR>ζ : ↥(rootsOfUnity k R)<VAR>m : ℤ<VAR>hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m<GOAL>∃ m, σ ↑↑ζ = ↑↑ζ ^ m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ+<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F R R<VAR>inst✝ : RingHomClass F R R<VAR>σ : F<VAR>ζ : ↥(rootsOfUnity k R)<VAR>m : ℤ<VAR>hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m<GOAL>∃ m_1, ↑↑ζ ^ (m % ↑(orderOf ζ)).toNat = ↑↑ζ ^ m_1
<VAR>R : Type u<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x y z : R<GOAL>SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Sort u_17<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h✝ : f =O[l] g'<VAR>hb : l.HasBasis p s<VAR>c : ℝ<VAR>h : c > 0 ∧ IsBigOWith c l f g'<GOAL>c > 0 ∧ ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<GOAL>H.FiniteIndex
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ<GOAL>H.FiniteIndex
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ<VAR>this : Finite (G ⧸ H)<GOAL>H.FiniteIndex
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>h : H<VAR>w : NormalWord d<GOAL>(h • w).prod = (base φ) h * w.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t : Set β<VAR>f✝ : α → β<VAR>inst✝ : Nonempty α<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>invFunOn f s (f x) ∈ s
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Involutive f<VAR>P : Prop<VAR>inst✝ : Decidable P<VAR>x : α<GOAL>f (if P then x else f x) = if ¬P then x else f x
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>X ^ n - C a ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>X ^ n + C (-a) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x : α × β × γ<VAR>ε : 𝕜<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>hx : x ∈ t<GOAL>(graph t).IsNClique 3 (toTriangle x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x : α × β × γ<VAR>ε : 𝕜<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>hx : x ∈ t<GOAL>(∃ c, (x.1, x.2.1, c) ∈ t) ∧ (∃ b, (x.1, b, x.2.2) ∈ t) ∧ ∃ a, (a, x.2.1, x.2.2) ∈ t
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<GOAL>(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id).card ≤ 2 ^ (P.parts.card - 1) * m
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<GOAL>(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id).card ≤ 2 ^ (P.parts.card - 1) * m
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<GOAL>(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id).card ≤ 2 ^ (P.parts.card - 1) * m
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<GOAL>∑ a ∈ filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts, (a \ (filter (fun x => x ⊆ a) (chunk hP G ε hU).parts).biUnion id).card ≤ 2 ^ (P.parts.card - 1) * m
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<GOAL>∑ _i ∈ filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts, m ≤ 2 ^ (P.parts.card - 1) * m
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<GOAL>(filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).card • m ≤ 2 ^ (P.parts.card - 1) * m
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<GOAL>(filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).card ≤ 2 ^ (P.parts.card - 1)
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<VAR>t : (filter (fun u => u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).card ≤ 2 ^ ((P.nonuniformWitnesses G ε U).card - 1)<GOAL>(filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).card ≤ 2 ^ (P.parts.card - 1)
<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>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<VAR>hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U<VAR>q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆ (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion fun B => B \ (filter (fun x => x ⊆ B) (chunk hP G ε hU).parts).biUnion id<VAR>t : (filter (fun u => u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts).card ≤ 2 ^ ((P.nonuniformWitnesses G ε U).card - 1)<GOAL>(P.nonuniformWitnesses G ε U).card ≤ P.parts.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p : α<VAR>hp✝ hp : Prime p<VAR>a : α<VAR>n : ℕ<VAR>ih : p ∣ a ^ n → p ∣ a<VAR>h : p ∣ a ^ (n + 1)<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p : α<VAR>hp✝ hp : Prime p<VAR>a : α<VAR>n : ℕ<VAR>ih : p ∣ a ^ n → p ∣ a<VAR>h : p ∣ a * a ^ n<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p : α<VAR>hp✝ hp : Prime p<VAR>a : α<VAR>n : ℕ<VAR>ih : p ∣ a ^ n → p ∣ a<VAR>h : p ∣ a * a ^ n<VAR>dvd_a : p ∣ a<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p : α<VAR>hp✝ hp : Prime p<VAR>a : α<VAR>n : ℕ<VAR>ih : p ∣ a ^ n → p ∣ a<VAR>h : p ∣ a * a ^ n<VAR>dvd_pow : p ∣ a ^ n<GOAL>p ∣ a
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁵ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝ : DecidableEq M<VAR>α : Type u_9<VAR>s : Finset α<VAR>f : { x // x ∈ s } → Finset M<GOAL>span R ↑(s.attach.biUnion f) = ⨆ x, span R ↑(f x)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.leftOp<VAR>j : Jᵒᵖ<GOAL>((fun s => (hc.desc (coconeOfConeLeftOp s)).unop) s ≫ (coneLeftOpOfCocone c).π.app j).op = (s.π.app j).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.leftOp<VAR>m : s.pt ⟶ (coneLeftOpOfCocone c).pt<VAR>w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j<GOAL>m = (fun s => (hc.desc (coconeOfConeLeftOp s)).unop) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.leftOp<VAR>m : s.pt ⟶ (coneLeftOpOfCocone c).pt<VAR>w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j<VAR>j : J<GOAL>(c.ι.app j ≫ m.op).unop = (c.ι.app j ≫ ((fun s => (hc.desc (coconeOfConeLeftOp s)).unop) s).op).unop
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<VAR>x : α<VAR>xC : x ∈ C<VAR>hxy : x ≠ y<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<VAR>x : α<VAR>xC : x ∈ C<VAR>hxy : x ≠ y<VAR>U : Set α<VAR>xU : x ∈ U<VAR>Uop : IsOpen U<VAR>V : Set α<VAR>yV : y ∈ V<VAR>Vop : IsOpen V<VAR>hUV : Disjoint (closure U) (closure V)<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<VAR>x : α<VAR>xC : x ∈ C<VAR>hxy : x ≠ y<VAR>U : Set α<VAR>xU : x ∈ U<VAR>Uop : IsOpen U<VAR>V : Set α<VAR>yV : y ∈ V<VAR>Vop : IsOpen V<VAR>hUV : Disjoint (closure U) (closure V)<GOAL>(Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty ∧ closure (U ∩ C) ⊆ C) ∧ (Perfect (closure (V ∩ C)) ∧ (closure (V ∩ C)).Nonempty ∧ closure (V ∩ C) ⊆ C) ∧ Disjoint (closure (U ∩ C)) (closure (V ∩ C))
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<VAR>x : α<VAR>xC : x ∈ C<VAR>hxy : x ≠ y<VAR>U : Set α<VAR>xU : x ∈ U<VAR>Uop : IsOpen U<VAR>V : Set α<VAR>yV : y ∈ V<VAR>Vop : IsOpen V<VAR>hUV : Disjoint (closure U) (closure V)<GOAL>(Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty) ∧ closure (U ∩ C) ⊆ C
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<VAR>x : α<VAR>xC : x ∈ C<VAR>hxy : x ≠ y<VAR>U : Set α<VAR>xU : x ∈ U<VAR>Uop : IsOpen U<VAR>V : Set α<VAR>yV : y ∈ V<VAR>Vop : IsOpen V<VAR>hUV : Disjoint (closure U) (closure V)<GOAL>((Perfect (closure (V ∩ C)) ∧ (closure (V ∩ C)).Nonempty) ∧ closure (V ∩ C) ⊆ C) ∧ Disjoint (closure (U ∩ C)) (closure (V ∩ C))
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T25Space α<VAR>hC : Perfect C<VAR>y : α<VAR>yC : y ∈ C<VAR>x : α<VAR>xC : x ∈ C<VAR>hxy : x ≠ y<VAR>U : Set α<VAR>xU : x ∈ U<VAR>Uop : IsOpen U<VAR>V : Set α<VAR>yV : y ∈ V<VAR>Vop : IsOpen V<VAR>hUV : Disjoint (closure U) (closure V)<GOAL>Disjoint (closure (U ∩ C)) (closure (V ∩ C))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<GOAL>a :: l ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ b ∈ l.head?, a < b
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<GOAL>x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<GOAL>(if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasProjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<GOAL>P.iso.inv ≫ (projectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫ Q.iso.inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasProjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<GOAL>Homotopy (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y)) (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>ha : 1 < a<GOAL>a ^ m < a ^ m.succ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n✝ : ℕ<VAR>ha : 1 < a<VAR>n : ℕ<VAR>a✝ : m.succ.le n<VAR>ih : a ^ m < a ^ n<GOAL>a ^ m < a ^ n.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>fromRel ⋯ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>∀ (e : Sym2 α), e ∉ fromRel ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>∀ (x y : α), s(x, y) ∉ fromRel ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>h : IsProjectiveLimit μ P<VAR>I : Finset ι<VAR>s : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>hs : MeasurableSet s<GOAL>μ (cylinder I s) = (P I) s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>h : IsProjectiveLimit μ P<VAR>I : Finset ι<VAR>s : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>hs : MeasurableSet s<GOAL>Measurable fun f i => f ↑i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → Prop<VAR>h : ∃ᶠ (n : ℕ) in atTop, P n<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → Prop<VAR>h : ∀ (a : ℕ), ∃ b > a, P b<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)