-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
theorem corners_theorem_nat (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n)
    (A : Finset (ℕ × ℕ)) (hAn : A ⊆ range n ×ˢ range n) (hAε : ε * n ^ 2 ≤ #A) :
    ¬ IsCornerFree (A : Set (ℕ × ℕ))

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ × ℕ
hx : x.1 < n ∧ x.2 < n
⊢ n ≤ 2 * n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : A ⊆ range n ×ˢ range n
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Tactic:
rw [← coe_subset, coe_product] at hAn

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ Set.InjOn (Prod.map Nat.cast Nat.cast) ↑A

Tactic:
have : Set.InjOn Nat.cast (range n) :=
  (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; omega)

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝² : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝¹ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this✝ : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
this : Set.InjOn Nat.cast ↑(range n)
⊢ Set.InjOn (Prod.map Nat.cast Nat.cast) ↑A

Proof state:
case h.hab.bc
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ 1 ≤ ↑n

Tactic:
simp

Result:
case h.hab.bc
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ 1 ≤ n

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ × ℕ
hx : x.1 < n ∧ x.2 < n
⊢ x ∈ Prod.map Nat.cast Nat.cast ⁻¹' Set.Iio ↑n ×ˢ Set.Iio ↑n

Tactic:
exact ⟨Fin.natCast_strictMono (by omega) hx.1, Fin.natCast_strictMono (by omega) hx.2⟩

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ 0 < ε / 9

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
a b : ℕ
hab : (a, b) ∈ A
this : a < n ∧ b < n
⊢ a < 2 * n + 1 ∧ b < 2 * n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ cornersTheoremBound (ε / 9) ≤ Fintype.card (Fin (2 * n + 1))

Tactic:
simp

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ cornersTheoremBound (ε / 9) ≤ 2 * n + 1

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree (Prod.map Nat.cast Nat.cast '' ↑A)
⊢ False

Tactic:
rw [← coe_image] at this

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ False

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ n ≤ 2 * n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝² : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝¹ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this✝ : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
this : Set.InjOn Nat.cast ↑(range n)
⊢ Set.InjOn (Prod.map Nat.cast Nat.cast) ↑A

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

Result:
no goals