ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>r : R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n * r = n • r
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>r : R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>r * OfNat.ofNat n = n • r
<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt n n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<GOAL>Mathlib.Meta.NormNum.IsNat Zero.zero 0
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<GOAL>Mathlib.Meta.NormNum.IsNat One.one 1
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>a : α<VAR>n : ℕ<VAR>h : ↑n = a<GOAL>Mathlib.Meta.NormNum.IsNat a n
<VAR>n n' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.IsNat (Int.ofNat n) n'
<VAR>n : ℤ<VAR>a : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n a → Mathlib.Meta.NormNum.IsNat n.natAbs a
<VAR>n : ℤ<VAR>a : ℕ<GOAL>Mathlib.Meta.NormNum.IsInt n (Int.negOfNat a) → Mathlib.Meta.NormNum.IsNat n.natAbs a
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n m : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℤ<VAR>m : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m
<VAR>R : Type u_1<VAR>Ring R<VAR>n m : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt n m → Mathlib.Meta.NormNum.IsInt (↑n) m
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>f : α → α → α<VAR>a b : α<VAR>a' b' c : ℕ<GOAL>f = HAdd.hAdd → Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.add b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>a' b' c : ℤ<GOAL>f = HAdd.hAdd → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → a'.add b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<GOAL>f = HAdd.hAdd → Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsRat (f a b) nc dc
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α<VAR>a : α<VAR>a' b : ℤ<GOAL>f = Neg.neg → Mathlib.Meta.NormNum.IsInt a a' → a'.neg = b → Mathlib.Meta.NormNum.IsInt (-a) b
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α<VAR>a : α<VAR>n n' : ℤ<VAR>d : ℕ<GOAL>f = Neg.neg → Mathlib.Meta.NormNum.IsRat a n d → n.neg = n' → Mathlib.Meta.NormNum.IsRat (-a) n' d
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>a' b' c : ℤ<GOAL>f = HSub.hSub → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → a'.sub b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>hf : f = HSub.hSub<VAR>ra : Mathlib.Meta.NormNum.IsRat a na da<VAR>rb : Mathlib.Meta.NormNum.IsRat b nb db<VAR>h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc<VAR>h₂ : da.mul db = k.mul dc<GOAL>Mathlib.Meta.NormNum.IsRat (f a b) nc dc
<VAR>α : Type u_1<VAR>Semiring α<VAR>f : α → α → α<VAR>a b : α<VAR>a' b' c : ℕ<GOAL>f = HMul.hMul → Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.mul b' = c → Mathlib.Meta.NormNum.IsNat (a * b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>a' b' c : ℤ<GOAL>f = HMul.hMul → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → a'.mul b' = c → Mathlib.Meta.NormNum.IsInt (a * b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<GOAL>f = HMul.hMul → Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → na.mul nb = (↑k).mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsRat (f a b) nc dc
<VAR>α : Type u<VAR>DivisionRing α<VAR>a b : α<VAR>cn : ℤ<VAR>cd : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat (a * b⁻¹) cn cd → Mathlib.Meta.NormNum.IsRat (a / b) cn cd
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>a b : α<VAR>c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a c → Mathlib.Meta.NormNum.IsNat b c → a = b
<VAR>x y : ℕ<GOAL>x.ble y = false ↔ y < x
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>z : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a z → Mathlib.Meta.NormNum.IsInt b z → a = b
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>n : ℤ<VAR>d : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a n d → Mathlib.Meta.NormNum.IsRat b n d → a = b
<VAR>a b : Prop<VAR>ha : a<VAR>hb : b<GOAL>a = b
<VAR>a b : Prop<VAR>ha : ¬a<VAR>hb : b<GOAL>a ≠ b
<VAR>a b : Prop<VAR>ha : a<VAR>hb : ¬b<GOAL>a ≠ b
<VAR>a b : Prop<VAR>ha : ¬a<VAR>hb : ¬b<GOAL>a = b
<VAR>a a' c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → a'.succ = c → Mathlib.Meta.NormNum.IsNat a.succ c
<VAR>a b a' b' c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.sub b' = c → Mathlib.Meta.NormNum.IsNat (a - b) c
<VAR>a b a' b' c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.mod b' = c → Mathlib.Meta.NormNum.IsNat (a % b) c
<VAR>a b a' b' c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.div b' = c → Mathlib.Meta.NormNum.IsNat (a / b) c
<VAR>a b a' b' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.mod a' = 0 → a ∣ b
<VAR>a b a' b' c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.mod a' = c.succ → ¬a ∣ b
<VAR>n : ℕ<VAR>pn : Mathlib.Meta.NormNum.IsNat n 0<GOAL>List.range n = []
<VAR>n nn n' : ℕ<VAR>pn : Mathlib.Meta.NormNum.IsNat n nn<VAR>pn' : nn = n'.succ<GOAL>List.range n = 0 :: List.map Nat.succ (List.range n')
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>insert a s = a ::ₘ s
<VAR>n : ℕ<VAR>pn : Mathlib.Meta.NormNum.IsNat n 0<GOAL>Multiset.range n = 0
<VAR>n nn n' : ℕ<VAR>pn : Mathlib.Meta.NormNum.IsNat n nn<VAR>pn' : nn = n'.succ<GOAL>Multiset.range n = n' ::ₘ Multiset.range n'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>insert a s = Finset.cons a s h
<VAR>n : ℕ<VAR>pn : Mathlib.Meta.NormNum.IsNat n 0<GOAL>Finset.range n = ∅
<VAR>n nn n' : ℕ<VAR>pn : Mathlib.Meta.NormNum.IsNat n nn<VAR>pn' : nn = n'.succ<GOAL>Finset.range n = Finset.cons n' (Finset.range n') ⋯
<VAR>α : Type u_1<VAR>Fintype α<VAR>elems : Finset α<VAR>complete : ∀ (x : α), x ∈ elems<GOAL>Finset.univ = elems
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>CommSemiring β<VAR>f : α → β<GOAL>Mathlib.Meta.NormNum.IsNat (∅.sum f) 0
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>CommSemiring β<VAR>f : α → β<GOAL>Mathlib.Meta.NormNum.IsNat (∅.prod f) 1
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>n m : ℤ<GOAL>a * b ^ n * b ^ m = a * b ^ (n + m)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>n m : ℤ<GOAL>a + n • b + m • b = a + (n + m) • b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>m : ℤ<GOAL>a * b * b ^ m = a * b ^ (m + 1)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>m : ℤ<GOAL>a + b + m • b = a + (m + 1) • b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>n : ℤ<GOAL>a + n • b + b = a + (n + 1) • b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>n : ℤ<GOAL>a * b ^ n * b = a * b ^ (n + 1)
<VAR>p q : Prop<GOAL>(¬q → ¬p) → p → q
<VAR>α α' : Sort u<VAR>β β' : Sort v<VAR>h : α = α'<VAR>h' : α' → β = β'<GOAL>(α → β) = (α' → β')
<VAR>α β : Sort u<VAR>Lean.Meta.FastSubsingleton α<VAR>h₂ : α = β<VAR>a : α<VAR>b : β<GOAL>HEq a b
<VAR>α : Sort u_1<VAR>x y : α<VAR>p : HEq x y → Prop<VAR>h : ∀ (he : x = y), p ⋯<VAR>he : HEq x y<GOAL>p he
<VAR>x y : Prop<VAR>p : x = y → Prop<VAR>h : ∀ (he : x ↔ y), p ⋯<VAR>he : x = y<GOAL>p he
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : f = g<VAR>Z : C<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<GOAL>(SzemerediRegularity.star hP G ε hU V).biUnion id ⊆ G.nonuniformWitness ε U V
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<GOAL>SzemerediRegularity.star hP G ε hU V ⊆ (SzemerediRegularity.chunk hP G ε hU).parts
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>h₂ : ¬G.IsUniform ε U V<GOAL>(G.nonuniformWitness ε U V \ (SzemerediRegularity.star hP G ε hU V).biUnion id).card ≤ 2 ^ (P.parts.card - 1) * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<GOAL>(1 - ε / 10) * ↑(G.nonuniformWitness ε U V).card ≤ ↑((SzemerediRegularity.star hP G ε hU V).biUnion id).card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>hm : Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≠ 0<GOAL>(SzemerediRegularity.chunk hP G ε hU).parts.card = 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>s : Finset α<VAR>hs : s ∈ (SzemerediRegularity.chunk hP G ε hU).parts<GOAL>s.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card ∨ s.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>s : Finset α<VAR>hs : s ∈ (SzemerediRegularity.chunk hP G ε hU).parts<GOAL>Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≤ s.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>s : Finset α<VAR>hs : s ∈ (SzemerediRegularity.chunk hP G ε hU).parts<GOAL>s.card ≤ Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<GOAL>↑((SzemerediRegularity.star hP G ε hU V).biUnion id).card ≤ ↑(SzemerediRegularity.star hP G ε hU V).card * (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>h𝒜 : 𝒜 ⊆ (SzemerediRegularity.chunk hP G ε hU).parts<VAR>hs : s ∈ 𝒜<GOAL>↑𝒜.card * ↑s.card * (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) / (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)) ≤ ↑(𝒜.sup id).card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>m_pos : 0 < ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card)<VAR>h𝒜 : 𝒜 ⊆ (SzemerediRegularity.chunk hP G ε hU).parts<VAR>hs : s ∈ 𝒜<GOAL>↑(𝒜.sup id).card ≤ ↑𝒜.card * ↑s.card * ((↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1) / ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card))
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>1 - ε ^ 5 / 50 ≤ (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) / (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)) ^ 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<GOAL>((↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1) / ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card)) ^ 2 ≤ 1 + ε ^ 5 / 49
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (SzemerediRegularity.chunk hP G ε hU).parts<VAR>hB : B ⊆ (SzemerediRegularity.chunk hP G ε hV).parts<GOAL>↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>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>A B : Finset (Finset α)<VAR>hA : A ⊆ (SzemerediRegularity.chunk hP G ε hU).parts<VAR>hB : B ⊆ (SzemerediRegularity.chunk hP G ε hV).parts<GOAL>(∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) ≤ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>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>A B : Finset (Finset α)<VAR>hA : A ⊆ (SzemerediRegularity.chunk hP G ε hU).parts<VAR>hB : B ⊆ (SzemerediRegularity.chunk hP G ε hV).parts<GOAL>|(∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) - ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))| ≤ ε ^ 5 / 49
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ ((∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV' : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>|↑(G.edgeDensity ((SzemerediRegularity.star hP G ε hU V).biUnion id) ((SzemerediRegularity.star hP G ε hV U).biUnion id)) - ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))| ≤ ε / 5
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>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>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<GOAL>4 / 5 * ε ≤ ↑(SzemerediRegularity.star hP G ε hU V).card / 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>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>3 / 4 * ε ≤ |(∑ ab ∈ (SzemerediRegularity.star hP G ε hU V).product (SzemerediRegularity.star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(SzemerediRegularity.star hP G ε hU V).card * ↑(SzemerediRegularity.star hP G ε hV U).card) - (∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card|
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>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 + ε ^ 4 / 3 ≤ (∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>U V : Finset α<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ (∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>a b : ℤ<GOAL>a = b ↔ ↑a = ↑b
<VAR>a b : ℤ<GOAL>a ≤ b ↔ ↑a ≤ ↑b
<VAR>a b : ℤ<GOAL>a < b ↔ ↑a < ↑b
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g h i : a ⟶ b<VAR>Mathlib.Tactic.BicategoryCoherence.LiftHom f<VAR>Mathlib.Tactic.BicategoryCoherence.LiftHom g<VAR>Mathlib.Tactic.BicategoryCoherence.LiftHom h<VAR>η : f ⟶ g<VAR>θ : g ⟶ h<VAR>ι : h ⟶ i<VAR>Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η<VAR>Mathlib.Tactic.BicategoryCoherence.LiftHom₂ θ<GOAL>η ≫ θ ≫ ι = (η ≫ θ) ≫ ι
<VAR>α : Type u<VAR>p : α → Prop<GOAL>(∀ (x : (CategoryTheory.forget (Type u)).obj α), p x) ↔ ∀ (x : α), p x
<VAR>α β : Type u<VAR>f : α ⟶ β<GOAL>⇑f = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h : f = g<VAR>x : (CategoryTheory.forget C).obj X<GOAL>f x = g x
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>self : CategoryTheory.BicategoricalCoherence f g<GOAL>CategoryTheory.IsIso ⊗𝟙
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<GOAL> ⊗𝟙 = 𝟙 f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>CategoryTheory.BicategoricalCoherence g h<GOAL> ⊗𝟙 = f ◁ ⊗𝟙
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>h : b ⟶ c<VAR>CategoryTheory.BicategoricalCoherence f g<GOAL> ⊗𝟙 = ⊗𝟙 ▷ h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ b<VAR>CategoryTheory.BicategoricalCoherence (𝟙 b) g<GOAL> ⊗𝟙 = (ρ_ f).inv ≫ f ◁ ⊗𝟙
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<VAR>g : b ⟶ b<VAR>CategoryTheory.BicategoricalCoherence g (𝟙 b)<GOAL> ⊗𝟙 = f ◁ ⊗𝟙 ≫ (ρ_ f).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>CategoryTheory.BicategoricalCoherence f g<GOAL> ⊗𝟙 = (λ_ f).hom ≫ ⊗𝟙
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>CategoryTheory.BicategoricalCoherence f g<GOAL> ⊗𝟙 = ⊗𝟙 ≫ (λ_ g).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>CategoryTheory.BicategoricalCoherence f g<GOAL> ⊗𝟙 = (ρ_ f).hom ≫ ⊗𝟙
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>CategoryTheory.BicategoricalCoherence f g<GOAL> ⊗𝟙 = ⊗𝟙 ≫ (ρ_ g).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : a ⟶ d<VAR>CategoryTheory.BicategoricalCoherence (f ≫ g ≫ h) i<GOAL> ⊗𝟙 = (α_ f g h).hom ≫ ⊗𝟙
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : a ⟶ d<VAR>CategoryTheory.BicategoricalCoherence i (f ≫ g ≫ h)<GOAL> ⊗𝟙 = ⊗𝟙 ≫ (α_ f g h).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g h : a ⟶ b<VAR>η : f ⟶ g<VAR>θ : g ⟶ h<GOAL>η ⊗≫ θ = η ≫ θ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>self : CategoryTheory.MonoidalCoherence X Y<GOAL>CategoryTheory.IsIso ⊗𝟙
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL> ⊗𝟙 = 𝟙 X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>CategoryTheory.MonoidalCoherence Y Z<GOAL> ⊗𝟙 = X ◁ ⊗𝟙
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>CategoryTheory.MonoidalCoherence X Y<GOAL> ⊗𝟙 = ⊗𝟙 ▷ Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.MonoidalCoherence (𝟙_ C) Y<GOAL> ⊗𝟙 = (ρ_ X).inv ≫ X ◁ ⊗𝟙
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.MonoidalCoherence Y (𝟙_ C)<GOAL> ⊗𝟙 = X ◁ ⊗𝟙 ≫ (ρ_ X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.MonoidalCoherence X Y<GOAL> ⊗𝟙 = (λ_ X).hom ≫ ⊗𝟙
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.MonoidalCoherence X Y<GOAL> ⊗𝟙 = ⊗𝟙 ≫ (λ_ Y).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.MonoidalCoherence X Y<GOAL> ⊗𝟙 = (ρ_ X).hom ≫ ⊗𝟙
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.MonoidalCoherence X Y<GOAL> ⊗𝟙 = ⊗𝟙 ≫ (ρ_ Y).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z W : C<VAR>CategoryTheory.MonoidalCoherence (X ⊗ Y ⊗ Z) W<GOAL> ⊗𝟙 = (α_ X Y Z).hom ≫ ⊗𝟙
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>CategoryTheory.MonoidalCoherence W (X ⊗ Y ⊗ Z)<GOAL> ⊗𝟙 = ⊗𝟙 ≫ (α_ X Y Z).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>f ⊗≫ g = f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>Mathlib.Tactic.Coherence.LiftObj W<VAR>Mathlib.Tactic.Coherence.LiftObj X<VAR>Mathlib.Tactic.Coherence.LiftObj Y<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>Mathlib.Tactic.Coherence.LiftHom f<VAR>Mathlib.Tactic.Coherence.LiftHom g<GOAL>f ≫ g ≫ h = (f ≫ g) ≫ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : f ≫ 𝟙 Y = g<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : f = g ≫ 𝟙 Y<GOAL>f = g
<VAR>x y : SetTheory.Game<GOAL>¬x ≤ y ↔ y.LF x
<VAR>x y : SetTheory.Game<GOAL>¬x.LF y ↔ y ≤ x
<VAR>x y : SetTheory.PGame<GOAL>x ≤ y ↔ ⟦x⟧ ≤ ⟦y⟧
<VAR>x y : SetTheory.PGame<GOAL>x.LF y ↔ SetTheory.Game.LF ⟦x⟧ ⟦y⟧
<VAR>x y : SetTheory.PGame<GOAL>x < y ↔ ⟦x⟧ < ⟦y⟧
<VAR>x y : SetTheory.PGame<GOAL>x ≈ y ↔ ⟦x⟧ = ⟦y⟧
<VAR>x y : SetTheory.PGame<GOAL>x.Fuzzy y ↔ SetTheory.Game.Fuzzy ⟦x⟧ ⟦y⟧
<VAR>b c : SetTheory.Game<GOAL>b.LF c → ∀ (a : SetTheory.Game), (b + a).LF (c + a)
<VAR>b c : SetTheory.Game<GOAL>b.LF c → ∀ (a : SetTheory.Game), (a + b).LF (a + c)
<VAR>ι : Type u_1<VAR>Small.{u, u_1} ι<VAR>f : ι → SetTheory.Game<GOAL>BddAbove (Set.range f)
<VAR>s : Set SetTheory.Game<VAR>Small.{u, u + 1} ↑s<GOAL>BddAbove s