awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : (↑A : Set (ℕ × ℕ)) ⊆ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)
hA :
  IsCornerFree
    (Set.image (α := Fin (2 * n).succ × Fin (2 * n).succ) (Prod.map Fin.val Fin.val)
      (Prod.map Nat.cast Nat.cast '' (↑A : Set (ℕ × ℕ))))
this_1 :
  (↑A : Set (ℕ × ℕ)) =
    Set.image (α := Fin (2 * n).succ × Fin (2 * n).succ) (Prod.map Fin.val Fin.val)
      (Prod.map Nat.cast Nat.cast '' (↑A : Set (ℕ × ℕ)))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : IsCornerFree (↑(image (Prod.map Nat.cast Nat.cast) A) : Set (Fin (2 * n).succ × Fin (2 * n).succ))
_ :
  ε / 9 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) 2 =
    ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) 2
_₁ :
  ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) 2 ≤
    ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2
_₂ :
  ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2 = ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
_₃ :
  Eq (α := ℝ) (↑(#A) : ℝ)
    (↑(Finset.card (α := Fin (2 * n + 1) × Fin (2 * n + 1)) (image (Prod.map Nat.cast Nat.cast) A)) : ℝ)
⊢ ε / 9 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) 2 ≤
    (↑(Finset.card (α := Fin (2 * n + 1) × Fin (2 * n + 1)) (image (Prod.map Nat.cast Nat.cast) A)) : ℝ)

Tactic:
calc
    _ = ε / 9 * (2 * n + 1) ^ 2 := by simp
    _ ≤ ε / 9 * (2 * n + n) ^ 2 := by gcongr; simp; unfold cornersTheoremBound at hn; lia
    _ = ε * n ^ 2 := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      have : Set.InjOn Nat.cast (range n) :=
        (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; lia)
      exact (this.prodMap this).mono hAn

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 = (↑(Fintype.card G) : ℝ) * (ε * (↑(Fintype.card G) : ℝ))

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
ha : LE.le (α := ℝ) 0 (↑(Fintype.card G) : ℝ)
⊢ (↑(Fintype.card G) : ℝ) * (ε * (↑(Fintype.card G) : ℝ)) ≤ HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(#A) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
⊢ HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(#A) : ℝ) = (↑(#B) : ℝ)

Tactic:
?_
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
_ : HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(#A) : ℝ) = (↑(#B) : ℝ)
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#B) : ℝ)

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

Premises used: HMul.hMul, Fintype.card, Nat.cast
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
norm_cast : Fintype.card G * #A = #B
⊢ HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(#A) : ℝ) = (↑(#B) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
rw : #(SProd.sprod (α := Finset G) univ A) = #B
⊢ Fintype.card G * #A = #B

Tactic:
rw [← card_univ, ← card_product]

Premises used: Finset.card_univ, Finset.card_product
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
⊢ ∀ (i : G × G),
    i ∈ SProd.sprod (α := Finset G) univ A ↔
      Membership.mem (α := G × G) B
        (((Equiv.refl G).prodShear fun (a : G) ↦ Equiv.addLeft a : (a : G × G) → G × G) i : G × G)

Tactic:
simp [B]
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
⊢ #(SProd.sprod (α := Finset G) univ A) = #B

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

Premises used: Finset.card_equiv, Equiv.addLeft, Equiv.refl, Equiv.prodShear
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#B) : ℝ)

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])
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#B) : ℝ)
⊢ ∃ (x₁ : G) (y₁ : G) (x₂ : G) (y₂ : G), 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

Premises used: isCorner_iff, corners_theorem, exists_and_left, exists_and_right, IsCornerFree
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#B) : ℝ)
obtain :
  ∀ (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
⊢ 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
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(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₂
rw : y₁ + y₂ - (x₂ + x₁) = y₁ - x₁ + (y₁ - x₁)
rw₁ : y₂ + y₁ - (x₂ + x₁) = y₁ - x₁ + (y₁ - x₁)
rw₂ : y₂ - x₂ + (y₁ - x₁) = y₁ - x₁ + (y₁ - x₁)
rw₃ : y₂ - x₂ = y₁ - x₁
rw₄ : y₂ + x₁ = y₁ + x₂
rw₅ : x₁ + y₂ = y₁ + x₂
rw₆ : x₂ + y₁ = y₁ + x₂
rw₇ rw₈ : y₁ + x₂ = y₁ + 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]

Premises used: sub_eq_sub_iff_add_eq_add, sub_add_sub_comm, add_comm, add_right_cancel_iff, add_sub_add_comm
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(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₁

Tactic:
have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
    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]
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
this_1 : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(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

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
B : Finset (G × G) :=
  {x : G × G |
    match (motive := G × G → Prop) x with
    | (x, y) => y - x ∈ A}
this_1 : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(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
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * (↑(Fintype.card G) : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set G)
let let₁ let₂ : False
let₃ :
  let B : Finset (G × G) :=
    {x : G × G |
      match (motive := G × G → Prop) x with
      | (x, y) => y - x ∈ A};
  ∀ (this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#B) : ℝ)), False
let₄ :
  let B : Finset (G × G) :=
    {x : G × G |
      match (motive := G × G → Prop) x with
      | (x, y) => y - x ∈ A};
  ∀ (this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(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
let₅ :
  let B : Finset (G × G) :=
    {x : G × G |
      match (motive := G × G → Prop) x with
      | (x, y) => y - x ∈ A};
  ∀ (this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(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
⊢ 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 -- TODO: This really ought to just be `by linear_combination h`
    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
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
⊢ (↑A : Set ℕ) ⊆ Set.Iio n

Tactic:
rw [← coe_subset, coe_range] at hAn

Premises used: Finset.coe_range, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
hAn₁ : (↑A : Set ℕ) ⊆ Set.Iio n
⊢ ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)

Tactic:
rw [← coe_subset, coe_range] at hAn

Premises used: Finset.coe_range, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
hAn₁ : (↑A : Set ℕ) ⊆ Set.Iio n
hAε₁ : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
⊢ ThreeAPFree (↑A : Set ℕ)

Tactic:
rw [← coe_subset, coe_range] at hAn

Premises used: Finset.coe_range, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
rw : ∀ a ∈ (↑A : Set ℕ), (↑(↑a : Fin (2 * n).succ) : ℕ) = id a
⊢ (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))

Tactic:
rw [Set.image_image, Set.image_congr, Set.image_id]

Premises used: Set.image_image, Set.image_congr, Set.image_id
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
simp : ∀ a ∈ A, a < 2 * n + 1
⊢ ∀ a ∈ (↑A : Set ℕ), (↑(↑a : Fin (2 * n).succ) : ℕ) = id a

Tactic:
simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]

Premises used: Fin.val_natCast, Nat.succ_eq_add_one, Nat.mod_succ_eq_iff_lt, Finset.mem_coe, id_eq
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
a : ℕ
ha : a ∈ A
⊢ a ∈ Set.Iio n

Tactic:
have := hAn ha
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
a : ℕ
ha : a ∈ A
this : a ∈ Set.Iio n
⊢ a < n

Tactic:
simp at this
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
a : ℕ
ha : a ∈ A
this : a < n
⊢ a < 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
⊢ (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))

Tactic:
have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
    rintro a ha
    have := hAn ha
    simp at this
    lia
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
this : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
⊢ ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))

Tactic:
rw [this] at hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
this : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
hA₁ : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
⊢ (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))

Tactic:
rw [this] at hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
⊢ IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val

Tactic:
have := Fin.isAddFreimanIso_Iio two_ne_zero (le_refl (2 * n))
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ n ≤ 2 * n

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ x < n

Tactic:
simpa only [coe_range, Set.mem_Iio] using hx

Premises used: Set.mem_Iio, Finset.coe_range
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (α := Fin (2 * n + 1)) ((fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) '' (↑A : Set ℕ))
⊢ ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))

Tactic:
rw [← coe_image] at this

Premises used: Finset.coe_image
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ 0 < ε / 3

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
simp : cornersTheoremBound (ε / 3) ≤ 2 * n + 1
⊢ cornersTheoremBound (ε / 3) ≤ Fintype.card (Fin (2 * n + 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ cornersTheoremBound (ε / 3) ≤ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
refine :
  ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
    (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
⊢ False

Tactic:
refine roth_3ap_theorem (ε / 3) (by positivity) (by simp; lia) _ ?_ this

Premises used: roth_3ap_theorem, HDiv.hDiv, OfNat.ofNat