mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
⊢ ∀ (i : G × G), i ∈ univ ×ˢ A ↔ ((Equiv.refl G).prodShear fun a ↦ Equiv.addLeft a) i ∈ B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ δₘ[A, B] ≤ A.dens⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑σₘ[A, B] = ↑(#(A * B)) / ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
⊢ ∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ x₁ ≠ x₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑δₘ[A, B] = ↑(#(A / B)) / ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ Eₘ[s₁, t₁] ≤ Eₘ[s₂, t₂]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ Set.MapsTo (fun x ↦ ((x.1, x.1), x.2, x.2)) ↑(s ×ˢ t) ↑({x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2})

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ Set.InjOn (fun x ↦ ((x.1, x.1), x.2, x.2)) ↑(s ×ˢ t)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s * #t ≤ Eₘ[s, t]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
t : Finset α
⊢ Eₘ[∅, t] = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ Eₘ[s, ∅] = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ 0 < Eₘ[s] ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * ↑σₘ[A, B] = ↑(#(A * B))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ Eₘ[s] = 0 ↔ s = ∅

Tactic:
rw [mulEnergy_eq_zero_iff, or_self_iff]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ Eₘ[s] = 0 ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ 0 < ε

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * ↑δₘ[A, B] = ↑(#(A / B))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ (i : (α × α) × α × α),
    i ∈ {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2} ↔
      (Equiv.prodProdProdComm α α α α) i ∈ {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < ↑(#A) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this✝ : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
this : y₁ - x₂ = y₁ - x₁
⊢ x₁ = x₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) * ↑(#A)) = ↑(#(A / A)) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ 4 / 5 * ε

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#A) ≤ ↑(#(A * A)) * ↑(#(A * A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#A) ≤ ↑(#(A * A)) * ↑(#(A * A))

Tactic:
by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
⊢ ¬ThreeAPFree ↑A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#(A * A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A] ≤ σₘ[A] ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A⁻¹, B] = δₘ[A, B]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ Eₘ[s, t] = ∑ a ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A⁻¹, B] = σₘ[A, B]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ ∀ (i : α), #({xy ∈ s ×ˢ t | xy.1 * xy.2 = i}) ^ 2 ≠ 0 → i ∈ s * t

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ Eₘ[s, t] = ∑ a, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < ↑(#A) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}) ^ 2 = (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ↑A = Fin.val '' Nat.cast '' ↑A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2 ≤ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * (↑(#A) * ↑(#A)) = ↑(#(A * A)) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 ≤ #u * ∑ c ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#A) ≤ ↑(#(A / A)) * ↑(#(A / A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 = #u * Eₘ[s, t]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}) ^ 2 ≤ #u * Eₘ[s, t]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#(A / A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝ : ↑A = Fin.val '' Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ n ≤ 2 * n

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
⊢ σₘ[A] ≤ δₘ[A] ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s ^ 2 * #t ^ 2 = #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ s * t}) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝ : ↑A = Fin.val '' Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ x < n

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ Eₘ[s, t] = Eₘ[t, s]

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ 0 < ε / 3

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ Set.InjOn f ↑(univ ×ˢ t ×ˢ t)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ cornersTheoremBound (ε / 3) ≤ Fintype.card (Fin (2 * n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∑ x, (eval x) f = ∑ x, ∑ d ∈ f.support, coeff d f * ∏ i, x i ^ d i

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ε / 3 * ↑(Fintype.card (Fin (2 * n + 1))) = ε / 3 * (2 * ↑n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
h : (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
⊢ f (a.1.1 * a.2.2⁻¹, a.2.1, a.2.2) = a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
⊢ Eₘ[univ, t] = Fintype.card α * #t ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s : Finset α
⊢ Eₘ[s, univ] = Fintype.card α * #s ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ε / 3 * (2 * ↑n + 1) ≤ ε / 3 * (2 * ↑n + ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ a, (∏ j, x₀ j ^ d ↑j) * a ^ d i = (∏ j, x₀ j ^ d ↑j) * ∑ a, a ^ d i

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ε / 3 * (2 * ↑n + ↑n) = ε * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ (∏ j, x₀ j ^ d ↑j) * ∑ a, a ^ d i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
    ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
⊢ 0 ≤ ε

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ Set.Iio n ⊆ Set.Iio (2 * n).succ

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ∏ j, ↑(e a) j ^ d j = ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j = a ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ↑(#A) = ↑(#(image (fun x ↦ ↑x) A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * ↑n ≤ ↑(#A)
⊢ ¬ThreeAPFree ↑A

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
⊢ ∑ x, (eval x) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
⊢ 0 < q - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: ⊢ (fun N ↦ ↑(rothNumberNat N)) =o[atTop] fun N ↦ ↑N

Tactic:
by

Goal state after: