-- 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
B : Finset (G × G) :=
  filter
    (fun x =>
      match x with
      | (x, y) => y - x ∈ A)
    univ
⊢ ∀ (i : G × G), i ∈ univ ×ˢ A ↔ ((Equiv.refl G).prodShear fun a => Equiv.addLeft a) i ∈ B

Tactic:
simp [B]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
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₂
⊢ False

Tactic:
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]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
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₁
⊢ 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
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)

Tactic:
calc
  _ = card G * (ε * card G) := by ring
  _ ≤ card G * #A := by gcongr
  _ = #B := ?_

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)
⊢ ¬ThreeAPFree ↑A

Tactic:
rintro hA

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
⊢ 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
⊢ False

Tactic:
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])

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
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
⊢ 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)
⊢ False

Tactic:
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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
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₂
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
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₁
⊢ False

Tactic:
exact hx₁x₂ <| by 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) ^ 2 = ↑(Fintype.card G) * (ε * ↑(Fintype.card G))

Tactic:
ring

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
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:
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]

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) * (ε * ↑(Fintype.card G)) ≤ ↑(Fintype.card G) * ↑(#A)

Tactic:
gcongr

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
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:
simpa [IsCornerFree, isCorner_iff, B, -exists_and_left, -exists_and_right]
  using corners_theorem ε hε hG B this

Result:
no goals