-- 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
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ ε / 9 * ↑(Fintype.card (Fin (2 * n + 1))) ^ 2 ≤ ↑(#(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; omega
  _ = ε * 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; omega)
    exact (this.prodMap this).mono hAn

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
⊢ Prod.map Nat.cast Nat.cast '' ↑A ⊆ Set.Iio ↑n ×ˢ Set.Iio ↑n

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

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
x : ℕ × ℕ
hx : x ∈ ↑(range n) ×ˢ ↑(range n)
⊢ x ∈ Prod.map Nat.cast Nat.cast ⁻¹' Set.Iio ↑n ×ˢ Set.Iio ↑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 ∈ ↑(range n) ×ˢ ↑(range n)
⊢ x ∈ Prod.map Nat.cast Nat.cast ⁻¹' Set.Iio ↑n ×ˢ Set.Iio ↑n

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

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
x : ℕ × ℕ
hx : x.1 < n ∧ x.2 < n
⊢ x ∈ Prod.map Nat.cast Nat.cast ⁻¹' Set.Iio ↑n ×ˢ Set.Iio ↑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)
⊢ False

Tactic:
have := Fin.isAddFreimanIso_Iio two_ne_zero (le_refl (2 * n))

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
⊢ 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)
⊢ ε / 9 * (2 * ↑n + ↑n) ^ 2 = ε * ↑n ^ 2

Tactic:
ring

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 : ℕ), (a, b) ∈ A → a < 2 * n + 1 ∧ b < 2 * n + 1

Tactic:
rintro a b hab

Result:
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
⊢ a < 2 * n + 1 ∧ b < 2 * n + 1

Proof state:
case h.hab.bc
n : ℕ
ε : ℝ
hε : 0 < ε
hn : ⌊(triangleRemovalBound (ε / 9 / 9) * 27)⁻¹⌋₊ + 1 ≤ 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:
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
⊢ False

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 omega) hx.1, Fin.natCast_strictMono (by omega) hx.2⟩

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 (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 ↑A
⊢ False

Tactic:
have : A = Prod.map Fin.val Fin.val ''
    (Prod.map Nat.cast Nat.cast '' A : Set (Fin (2 * n).succ × Fin (2 * n).succ)) := by
  rw [Set.image_image, Set.image_congr, Set.image_id]
  simp only [mem_coe, Nat.succ_eq_add_one, Prod.map_apply, Fin.val_natCast, id_eq, Prod.forall,
    Prod.mk.injEq, Nat.mod_succ_eq_iff_lt]
  rintro a b hab
  have := hAn hab
  simp at this
  omega

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ↑A = Prod.map Fin.val Fin.val '' (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 ↑A
a b : ℕ
hab : (a, b) ∈ A
this : (a, b) ∈ ↑(range n) ×ˢ ↑(range n)
⊢ a < 2 * n + 1 ∧ b < 2 * n + 1

Tactic:
simp at this

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