-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
theorem roth_3ap_theorem (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ card G)
    (A : Finset G) (hAε : ε * card G ≤ #A) : ¬ ThreeAPFree (A : Set G)

Proof state:
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
⊢ False

Tactic:
let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A

Result:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ False

Proof state:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
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:
simpa using this.symm

Result:
no goals

Proof state:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ ↑(Fintype.card G) * ↑(#A) = ↑(#B)

Tactic:
norm_cast

Result:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ Fintype.card G * #A = #B

Proof state:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ Fintype.card G * #A = #B

Tactic:
rw [← card_univ, ← card_product]

Result:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ #(univ ×ˢ A) = #B

Proof state:
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) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ #(univ ×ˢ A) = #B

Tactic:
exact card_equiv ((Equiv.refl _).prodShear fun a ↦ Equiv.addLeft a) (by simp [B])

Result:
no goals

Proof state:
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
⊢ False

Tactic:
classical
let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A
have : ε * card G ^ 2 ≤ #B := by
  calc
    _ = card G * (ε * card G) := by ring
    _ ≤ card G * #A := by gcongr
    _ = #B := ?_
  norm_cast
  rw [← card_univ, ← card_product]
  exact card_equiv ((Equiv.refl _).prodShear fun a ↦ Equiv.addLeft a) (by simp [B])
obtain ⟨x₁, y₁, x₂, y₂, hx₁y₁, hx₁y₂, hx₂y₁, hxy, hx₁x₂⟩ :
    ∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ x₁ ≠ x₂ := by
  simpa [IsCornerFree, isCorner_iff, B, -exists_and_left, -exists_and_right]
    using corners_theorem ε hε hG B this
have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by rw [sub_add_sub_comm, add_comm, add_sub_add_comm, add_right_cancel_iff,
    sub_eq_sub_iff_add_eq_add, add_comm, hxy, add_comm]
exact hx₁x₂ <| by simpa using this.symm

Result:
no goals