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 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
⊢ Prod.map Nat.cast Nat.cast '' (↑A : Set (ℕ × ℕ)) ⊆
    SProd.sprod (α := Set (Fin (2 * n + 1))) (β := Set (Fin (2 * n + 1))) (Set.Iio (↑n : Fin (2 * n + 1)))
      (Set.Iio (↑n : Fin (2 * n + 1)))

Tactic:
Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.image_subset_iff
-- 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 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
refine :
  ∀ (x : ℕ × ℕ) (hx : x ∈ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)),
    x ∈
      Prod.map Nat.cast Nat.cast ⁻¹'
        SProd.sprod (α := Set (Fin (2 * n + 1))) (β := Set (Fin (2 * n + 1))) (Set.Iio (↑n : Fin (2 * n + 1)))
          (Set.Iio (↑n : Fin (2 * n + 1)))
⊢ Prod.map Nat.cast Nat.cast '' (↑A : Set (ℕ × ℕ)) ⊆
    SProd.sprod (α := Set (Fin (2 * n + 1))) (β := Set (Fin (2 * n + 1))) (Set.Iio (↑n : Fin (2 * n + 1)))
      (Set.Iio (↑n : Fin (2 * n + 1)))

Tactic:
refine Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.image_subset_iff
-- 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 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
x : ℕ × ℕ
hx : x ∈ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
⊢ x.1 < n ∧ x.2 < n

Tactic:
simp only [coe_range, Set.mem_prod, Set.mem_Iio] at hx

Premises used: Set.mem_Iio, Finset.coe_range, Set.mem_prod
-- 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 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
x : ℕ × ℕ
hx : x.1 < n ∧ x.2 < n
⊢ n ≤ 2 * n

Tactic:
lia
-- 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 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
x : ℕ × ℕ
hx : x.1 < n ∧ x.2 < n
⊢ x ∈
    Prod.map Nat.cast Nat.cast ⁻¹'
      SProd.sprod (α := Set (Fin (2 * n + 1))) (β := Set (Fin (2 * n + 1))) (Set.Iio (↑n : Fin (2 * n + 1)))
        (Set.Iio (↑n : Fin (2 * n + 1)))

Tactic:
exact ⟨Fin.natCast_strictMono (by lia) hx.1, Fin.natCast_strictMono (by lia) hx.2⟩
-- 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 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
⊢ IsCornerFree (G := Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast '' (↑A : Set (ℕ × ℕ)))

Tactic:
have := hA.of_image this.isAddFreimanHom Fin.val_injective.injOn <| by
    refine Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_
    simp only [coe_range, Set.mem_prod, Set.mem_Iio] at hx
    exact ⟨Fin.natCast_strictMono (by lia) hx.1, Fin.natCast_strictMono (by lia) hx.2⟩
-- 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 (G := Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast '' (↑A : Set (ℕ × ℕ)))
⊢ IsCornerFree (↑(image (Prod.map Nat.cast Nat.cast) A) : Set (Fin (2 * n).succ × Fin (2 * n).succ))

Tactic:
rw [← coe_image] at this

Premises used: Finset.coe_image
-- 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))
⊢ 0 < ε / 9

Tactic:
positivity
-- 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))
simp : cornersTheoremBound (ε / 9) ≤ 2 * n + 1
⊢ cornersTheoremBound (ε / 9) ≤ Fintype.card (Fin (2 * n + 1))

Tactic:
simp
-- 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))
⊢ cornersTheoremBound (ε / 9) ≤ 2 * n + 1

Tactic:
lia
-- 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))
refine :
  ε / 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)) : ℝ)
⊢ False

Tactic:
refine corners_theorem (ε / 9) (by positivity) (by simp; lia) _ ?_ this

Premises used: corners_theorem, HDiv.hDiv, OfNat.ofNat
-- 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

Tactic:
simp
-- 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))
hbc : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) 2 ≤
    ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2

Tactic:
gcongr
-- 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))
hbc : 1 ≤ n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : ⌊(triangleRemovalBound (ε / 9 / 9) * 27)⁻¹⌋₊ + 1 ≤ 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))
⊢ 1 ≤ n

Tactic:
lia
-- 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 (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2 = ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2

Tactic:
ring
-- 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))
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)

Tactic:
hAε
-- 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))
rw : Set.InjOn (β := Fin (2 * n + 1) × Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast) (↑A : Set (ℕ × ℕ))
⊢ Eq (α := ℝ) (↑(#A) : ℝ)
    (↑(Finset.card (α := Fin (2 * n + 1) × Fin (2 * n + 1)) (image (Prod.map Nat.cast Nat.cast) A)) : ℝ)

Tactic:
rw [card_image_of_injOn]

Premises used: Finset.card_image_of_injOn
-- 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))
simp : n ≤ 2 * n + 1
⊢ (↑(range n) : Set ℕ) ⊆ Set.Iio (2 * n).succ

Tactic:
simp
-- 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))
⊢ n ≤ 2 * n + 1

Tactic:
lia
-- 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))
⊢ Set.InjOn (β := Fin (2 * n).succ) Nat.cast (↑(range n) : Set ℕ)

Tactic:
have : Set.InjOn Nat.cast (range n) :=
        (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; lia)
-- 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_3 : IsCornerFree (↑(image (Prod.map Nat.cast Nat.cast) A) : Set (Fin (2 * n).succ × Fin (2 * n).succ))
this : Set.InjOn (β := Fin (2 * n).succ) Nat.cast (↑(range n) : Set ℕ)
⊢ Set.InjOn (β := Fin (2 * n + 1) × Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast) (↑A : Set (ℕ × ℕ))

Tactic:
(this.prodMap this).mono hAn

Premises used: Set.InjOn.prodMap, Set.InjOn.mono
-- 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_3 : IsCornerFree (↑(image (Prod.map Nat.cast Nat.cast) A) : Set (Fin (2 * n).succ × Fin (2 * n).succ))
this : Set.InjOn (β := Fin (2 * n).succ) Nat.cast (↑(range n) : Set ℕ)
⊢ Set.InjOn (β := Fin (2 * n + 1) × Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast) (↑A : Set (ℕ × ℕ))

Tactic:
exact (this.prodMap this).mono hAn

Premises used: Set.InjOn.prodMap, Set.InjOn.mono