ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>hs : ThreeAPFree s<GOAL>ThreeAPFree t
<VAR>α : Type u_2<VAR>Monoid α<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>hs : ThreeGPFree s<GOAL>ThreeGPFree t
<VAR>α : Type u_2<VAR>Monoid α<GOAL>ThreeGPFree ∅
<VAR>α : Type u_2<VAR>AddMonoid α<GOAL>ThreeAPFree ∅
<VAR>α : Type u_2<VAR>Monoid α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>ThreeGPFree s
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>ThreeAPFree s
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>a : α<GOAL>ThreeAPFree {a}
<VAR>α : Type u_2<VAR>Monoid α<VAR>a : α<GOAL>ThreeGPFree {a}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddMonoid α<VAR>AddMonoid β<VAR>s : Set α<VAR>t : Set β<VAR>hs : ThreeAPFree s<VAR>ht : ThreeAPFree t<GOAL>ThreeAPFree (s ×ˢ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid α<VAR>Monoid β<VAR>s : Set α<VAR>t : Set β<VAR>hs : ThreeGPFree s<VAR>ht : ThreeGPFree t<GOAL>ThreeGPFree (s ×ˢ t)
<VAR>ι : Type u_6<VAR>α : ι → Type u_7<VAR>(i : ι) → AddMonoid (α i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : ∀ (i : ι), ThreeAPFree (s i)<GOAL>ThreeAPFree (Set.univ.pi s)
<VAR>ι : Type u_6<VAR>α : ι → Type u_7<VAR>(i : ι) → Monoid (α i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : ∀ (i : ι), ThreeGPFree (s i)<GOAL>ThreeGPFree (Set.univ.pi s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s A : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsAddFreimanHom 2 s t f<VAR>hf' : Set.InjOn f s<VAR>hAs : A ⊆ s<VAR>hA : ThreeAPFree (f '' A)<GOAL>ThreeAPFree A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s A : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 s t f<VAR>hf' : Set.InjOn f s<VAR>hAs : A ⊆ s<VAR>hA : ThreeGPFree (f '' A)<GOAL>ThreeGPFree A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s A : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s<GOAL>ThreeAPFree (f '' A) ↔ ThreeAPFree A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s A : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hAs : A ⊆ s<GOAL>ThreeGPFree (f '' A) ↔ ThreeGPFree A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 s t f<VAR>hf' : Set.InjOn f s<VAR>ht : ThreeGPFree t<GOAL>ThreeGPFree s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsAddFreimanHom 2 s t f<VAR>hf' : Set.InjOn f s<VAR>ht : ThreeAPFree t<GOAL>ThreeAPFree s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsAddFreimanIso 2 s t f<GOAL>ThreeAPFree s ↔ ThreeAPFree t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 s t f<GOAL>ThreeGPFree s ↔ ThreeGPFree t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Set α<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>f : F<VAR>hf : Set.InjOn (⇑f) (s * s)<VAR>h : ThreeGPFree s<GOAL>ThreeGPFree (⇑f '' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Set α<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>f : F<VAR>hf : Set.InjOn (⇑f) (s + s)<VAR>h : ThreeAPFree s<GOAL>ThreeAPFree (⇑f '' s)
<VAR>α : Type u_2<VAR>CancelCommMonoid α<VAR>s : Set α<VAR>hs : ThreeGPFree s<VAR>a : α<GOAL>a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → b = c
<VAR>α : Type u_2<VAR>AddCancelCommMonoid α<VAR>s : Set α<VAR>a : α<GOAL>ThreeAPFree (insert a s) ↔ ThreeAPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b + c = a + a → b = a
<VAR>α : Type u_2<VAR>CancelCommMonoid α<VAR>s : Set α<VAR>a : α<GOAL>ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
<VAR>α : Type u_2<VAR>CancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ThreeGPFree s<GOAL>ThreeGPFree (a • s)
<VAR>α : Type u_2<VAR>AddCancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ThreeAPFree s<GOAL>ThreeAPFree (a +ᵥ s)
<VAR>α : Type u_2<VAR>AddCancelCommMonoid α<VAR>s : Set α<VAR>a : α<GOAL>ThreeAPFree (a +ᵥ s) ↔ ThreeAPFree s
<VAR>α : Type u_2<VAR>CancelCommMonoid α<VAR>s : Set α<VAR>a : α<GOAL>ThreeGPFree (a • s) ↔ ThreeGPFree s
<VAR>α : Type u_2<VAR>OrderedCancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ∀ i ∈ s, i < a<GOAL>ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ∀ i ∈ s, i < a<GOAL>ThreeAPFree (insert a s) ↔ ThreeAPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → a = b
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>NoZeroDivisors α<VAR>s : Set α<VAR>a : α<VAR>hs : ThreeGPFree s<VAR>ha : a ≠ 0<GOAL>ThreeGPFree (a • s)
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>NoZeroDivisors α<VAR>s : Set α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>ThreeGPFree (a • s) ↔ ThreeGPFree s
<VAR>s : Set ℕ<GOAL>ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<GOAL>addRothNumber s ≤ s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<GOAL>mulRothNumber s ≤ s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<GOAL>∃ t ⊆ s, t.card = addRothNumber s ∧ ThreeAPFree ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<GOAL>∃ t ⊆ s, t.card = mulRothNumber s ∧ ThreeGPFree ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s t : Finset α<VAR>hs : ThreeAPFree ↑s<VAR>h : s ⊆ t<GOAL>s.card ≤ addRothNumber t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s t : Finset α<VAR>hs : ThreeGPFree ↑s<VAR>h : s ⊆ t<GOAL>s.card ≤ mulRothNumber t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>hs : ThreeAPFree ↑s<GOAL>addRothNumber s = s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>hs : ThreeGPFree ↑s<GOAL>mulRothNumber s = s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<GOAL>addRothNumber ∅ = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<GOAL>mulRothNumber ∅ = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>a : α<GOAL>addRothNumber {a} = 1
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>a : α<GOAL>mulRothNumber {a} = 1
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s t : Finset α<GOAL>mulRothNumber (s ∪ t) ≤ mulRothNumber s + mulRothNumber t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s t : Finset α<GOAL>addRothNumber (s ∪ t) ≤ addRothNumber s + addRothNumber t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>AddMonoid α<VAR>DecidableEq β<VAR>AddMonoid β<VAR>s : Finset α<VAR>t : Finset β<GOAL>addRothNumber s * addRothNumber t ≤ addRothNumber (s ×ˢ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Monoid α<VAR>DecidableEq β<VAR>Monoid β<VAR>s : Finset α<VAR>t : Finset β<GOAL>mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>n : ℕ<VAR>h : ∀ t ∈ Finset.powersetCard n s, ¬ThreeGPFree ↑t<GOAL>mulRothNumber s < n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>n : ℕ<VAR>h : ∀ t ∈ Finset.powersetCard n s, ¬ThreeAPFree ↑t<GOAL>addRothNumber s < n
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>CommMonoid β<VAR>DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<GOAL>mulRothNumber B ≤ mulRothNumber A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsAddFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<GOAL>addRothNumber B ≤ addRothNumber A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>CommMonoid β<VAR>DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<GOAL>mulRothNumber A = mulRothNumber B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsAddFreimanIso 2 (↑A) (↑B) f<GOAL>addRothNumber A = addRothNumber B
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddCancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>addRothNumber (Finset.map (addLeftEmbedding a) s) = addRothNumber s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>CancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>mulRothNumber (Finset.map (mulLeftEmbedding a) s) = mulRothNumber s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddCancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>addRothNumber (Finset.map (addRightEmbedding a) s) = addRothNumber s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>CancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>mulRothNumber (Finset.map (mulRightEmbedding a) s) = mulRothNumber s
<VAR>n : ℕ<GOAL>rothNumberNat n = addRothNumber (Finset.range n)
<VAR>N : ℕ<GOAL>rothNumberNat N ≤ N
<VAR>n : ℕ<GOAL>∃ t ⊆ Finset.range n, t.card = rothNumberNat n ∧ ThreeAPFree ↑t
<VAR>k n : ℕ<VAR>s : Finset ℕ<VAR>hs : ThreeAPFree ↑s<VAR>hsn : ∀ x ∈ s, x < n<VAR>hsk : s.card = k<GOAL>k ≤ rothNumberNat n
<VAR>M N : ℕ<GOAL>rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N
<VAR>a b : ℕ<GOAL>addRothNumber (Finset.Ico a b) = rothNumberNat (b - a)
<VAR>k n : ℕ<VAR>hkn : 2 * k ≤ n<GOAL>addRothNumber (Finset.Iio ↑k) = rothNumberNat k
<VAR>k n : ℕ<VAR>hkn : k ≤ n<GOAL>addRothNumber (Finset.Iio ↑k) ≤ rothNumberNat k
<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>a b : ℚ<GOAL>a ≠ b ↔ ↑a ≠ ↑b
<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>↑(OfNat.ofNat a) = OfNat.ofNat a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Finset α<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<GOAL>s₁.mulEnergy t₁ ≤ s₂.mulEnergy t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Finset α<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<GOAL>s₁.addEnergy t₁ ≤ s₂.addEnergy t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t : Finset α<VAR>hs : s₁ ⊆ s₂<GOAL>s₁.addEnergy t ≤ s₂.addEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t : Finset α<VAR>hs : s₁ ⊆ s₂<GOAL>s₁.mulEnergy t ≤ s₂.mulEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t₁ t₂ : Finset α<VAR>ht : t₁ ⊆ t₂<GOAL>s.addEnergy t₁ ≤ s.addEnergy t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t₁ t₂ : Finset α<VAR>ht : t₁ ⊆ t₂<GOAL>s.mulEnergy t₁ ≤ s.mulEnergy t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s.card * t.card ≤ s.mulEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s.card * t.card ≤ s.addEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>0 < s.addEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>0 < s.mulEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>t : Finset α<GOAL>∅.addEnergy t = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>t : Finset α<GOAL>∅.mulEnergy t = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s : Finset α<GOAL>s.mulEnergy ∅ = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s : Finset α<GOAL>s.addEnergy ∅ = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>0 < s.mulEnergy t ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>0 < s.addEnergy t ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s.addEnergy t = 0 ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s.mulEnergy t = 0 ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s.addEnergy t = (Finset.filter (fun x => Finset.addEnergy_eq_card_filter.match_1 (fun x => Prop) x fun a b c d => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s.mulEnergy t = (Finset.filter (fun x => match x with | ((a, b), c, d) => a * b = c * d) ((s ×ˢ t) ×ˢ s ×ˢ t)).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s.addEnergy t = ∑ a ∈ s + t, (Finset.filter (fun x => Finset.addEnergy_eq_sum_sq'.match_1 (fun x => Prop) x fun x y => x + y = a) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s.mulEnergy t = ∑ a ∈ s * t, (Finset.filter (fun x => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>Fintype α<VAR>s t : Finset α<GOAL>s.mulEnergy t = ∑ a : α, (Finset.filter (fun x => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>Fintype α<VAR>s t : Finset α<GOAL>s.addEnergy t = ∑ a : α, (Finset.filter (fun x => Finset.addEnergy_eq_sum_sq'.match_1 (fun x => Prop) x fun x y => x + y = a) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t u : Finset α<GOAL>(Finset.filter (fun x => match x with | (a, b) => a * b ∈ u) (s ×ˢ t)).card ^ 2 ≤ u.card * s.mulEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t u : Finset α<GOAL>(Finset.filter (fun x => Finset.addEnergy_eq_sum_sq'.match_1 (fun x => Prop) x fun a b => a + b ∈ u) (s ×ˢ t)).card ^ 2 ≤ u.card * s.addEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s.card ^ 2 * t.card ^ 2 ≤ (s + t).card * s.addEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s.card ^ 2 * t.card ^ 2 ≤ (s * t).card * s.mulEnergy t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommMonoid α<VAR>s t : Finset α<GOAL>s.mulEnergy t = t.mulEnergy s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>s t : Finset α<GOAL>s.addEnergy t = t.addEnergy s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>Fintype α<VAR>t : Finset α<GOAL>Finset.univ.mulEnergy t = Fintype.card α * t.card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>Fintype α<VAR>t : Finset α<GOAL>Finset.univ.addEnergy t = Fintype.card α * t.card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>Fintype α<VAR>s : Finset α<GOAL>s.addEnergy Finset.univ = Fintype.card α * s.card ^ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>Fintype α<VAR>s : Finset α<GOAL>s.mulEnergy Finset.univ = Fintype.card α * s.card ^ 2
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A - C).card * B.card ≤ (A - B).card * (B - C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A / B).card * (B / C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A - C).card * B.card ≤ (A + B).card * (B + C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A + C).card * B.card ≤ (A - B).card * (B + C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A / B).card * (B * C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A + C).card * B.card ≤ (A + B).card * (B - C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A * B).card * (B / C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B : Finset α<VAR>C : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<GOAL>(A * B * C).card * A.card ≤ (A * B).card * (A * C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B : Finset α<VAR>C : Finset α<VAR>hA : ∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card<GOAL>(A + B + C).card * A.card ≤ (A + B).card * (A + C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A + C).card / ↑A.card ≤ ↑(A' + C).card / ↑A'.card<VAR>A' : Finset α<GOAL>A' ⊆ A → (A + C).card * A'.card ≤ (A' + C).card * A.card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card<VAR>A' : Finset α<GOAL>A' ⊆ A → (A * C).card * A'.card ≤ (A' * C).card * A.card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A + C).card * B.card ≤ (A + B).card * (B + C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A + C).card * B.card ≤ (A - B).card * (B - C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A / B).card * (B / C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A * B).card * (B / C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A - C).card * B.card ≤ (A + B).card * (B - C).card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A - C).card * B.card ≤ (A - B).card * (B + C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A / B).card * (B * C).card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A B : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>n : ℕ<GOAL>↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A B : Finset α<VAR>hAB : ∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card<VAR>n : ℕ<GOAL>↑(A + n • B).card ≤ (↑(A + B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(m • B - n • B).card ≤ (↑(A + B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(m • B - n • B).card ≤ (↑(A - B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>n : ℕ<GOAL>↑(B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>n : ℕ<GOAL>↑(n • B).card ≤ (↑(A + B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>n : ℕ<GOAL>↑(B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>A : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>n : ℕ<GOAL>↑(n • B).card ≤ (↑(A - B).card / ↑A.card) ^ n * ↑A.card
<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε₁ : ε ≤ 1<GOAL>0 < SimpleGraph.triangleRemovalBound ε
<VAR>ε : ℝ<VAR>hε : ε ≤ 0<GOAL>SimpleGraph.triangleRemovalBound ε ≤ 0
<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>SimpleGraph.triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1
<VAR>n k : ℕ<VAR>hk : 0 < k<VAR>hn : k ≤ n<GOAL>n < 2 * k * (n / k)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊<VAR>hX : s ∈ P.parts<GOAL>↑(Fintype.card α) / (2 * ↑(SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>t : Finset α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊<VAR>ht : t ∈ (SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3<GOAL>SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>Nonempty α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hPε : P.IsUniform G (ε / 8)<VAR>hP' : 4 / ε ≤ ↑P.parts.card<GOAL>2 * (↑G.edgeFinset.card - ↑(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card) < 2 * ε * ↑(Fintype.card α ^ 2)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<GOAL>SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>hG : ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3<GOAL>∃ G' ≤ G, ∃ x, ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>n : ℕ∞<GOAL>ContDiff K n fun x => x
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>x : E<VAR>n : ℕ∞<GOAL>ContDiffAt K n (fun x => x) x
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>s : Set E<VAR>n : ℕ∞<GOAL>ContDiffOn K n (fun x => x) s
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace K G<VAR>f : E → F<VAR>n : ℕ∞<VAR>g : F → G<VAR>hg : ContDiff K n g<VAR>hf : ContDiff K n f<GOAL>ContDiff K n fun x => g (f x)
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace K G<VAR>x : E<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : F → G<VAR>hg : ContDiffAt K n g (f x)<VAR>hf : ContDiffAt K n f x<GOAL>ContDiffAt K n (fun x => g (f x)) x
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>n : ℕ∞<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_8<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace K (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hΦ : ∀ (i : ι), ContDiff K n fun x => Φ x i<GOAL>ContDiff K n Φ
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>s : Set E<VAR>n : ℕ∞<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_8<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace K (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hΦ : ∀ (i : ι), ContDiffOn K n (fun x => Φ x i) s<GOAL>ContDiffOn K n Φ s
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>x : E<VAR>n : ℕ∞<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_8<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace K (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hΦ : ∀ (i : ι), ContDiffAt K n (fun x => Φ x i) x<GOAL>ContDiffAt K n Φ x
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>s : Set E<VAR>CompleteSpace K<VAR>f g : E → K<VAR>n : ℕ∞<VAR>hf : ContDiffOn K n f s<VAR>hg : ContDiffOn K n g s<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<GOAL>ContDiffOn K n (fun x => f x / g x) s