awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
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
⊢ False
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
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 (ℕ × ℕ)))
⊢ False
have this₁ : IsCornerFree (↑(image (Prod.map Nat.cast Nat.cast) A) : Set (Fin (2 * n).succ × Fin (2 * n).succ))
Tactic: rw [← coe_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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) ≤ Fintype.card (Fin (2 * n + 1))
have simp : cornersTheoremBound (ε / 9) ≤ 2 * n + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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))
⊢ False
have 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)) : ℝ)
Tactic: refine corners_theorem (ε / 9) (by positivity) (by simp; lia) _ ?_ this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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 : ℝ) + 1) 2 ≤
    ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2
have hbc : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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))
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)
have hbc : 1 ≤ n
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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))
⊢ Eq (α := ℝ) (↑(#A) : ℝ)
    (↑(Finset.card (α := Fin (2 * n + 1) × Fin (2 * n + 1)) (image (Prod.map Nat.cast Nat.cast) A)) : ℝ)
have rw : Set.InjOn (β := Fin (2 * n + 1) × Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast) (↑A : Set (ℕ × ℕ))
Tactic: rw [card_image_of_injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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))
⊢ (↑(range n) : Set ℕ) ⊆ Set.Iio (2 * n).succ
have simp : n ≤ 2 * n + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
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 + 1) × Fin (2 * n + 1)) (Prod.map Nat.cast Nat.cast) (↑A : Set (ℕ × ℕ))
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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 ≤
    (↑(Finset.card (α := Fin (2 * n + 1) × Fin (2 * n + 1)) (image (Prod.map Nat.cast Nat.cast) A)) : ℝ)
have _ : ε / 9 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) 2 =
  ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) 2
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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 (α := ℝ) (β := ℕ) (↑(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)) : ℝ)
have _₁ : ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) 2 ≤
  ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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 (α := ℝ) (β := ℕ) (↑(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)) : ℝ)
have _₂ : ε / 9 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) 2 = ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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
⊢ ε / 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)) : ℝ)
have _₃ : Eq (α := ℝ) (↑(#A) : ℝ)
  (↑(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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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}
⊢ (↑(Fintype.card G) : ℝ) * (ε * (↑(Fintype.card G) : ℝ)) ≤ HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(#A) : ℝ)
have ha : LE.le (α := ℝ) 0 (↑(Fintype.card G) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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) : ℝ)
have _ : HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(#A) : ℝ) = (↑(#B) : ℝ)
Tactic: calc
      _ = card G * (ε * card G) := by ring
      _ ≤ card G * #A := by gcongr
      _ = #B := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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) : ℝ)
have norm_cast : Fintype.card G * #A = #B
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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}
⊢ Fintype.card G * #A = #B
have rw : #(SProd.sprod (α := Finset G) univ A) = #B
Tactic: rw [← card_univ, ← card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
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}
⊢ False
have this : ε * 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])
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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) : ℝ)
⊢ False
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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₁) = y₁ - x₁ + (y₁ - x₁)
have rw : y₁ + y₂ - (x₂ + 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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₁)
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)
have rw₁ : y₂ + y₁ - (x₂ + 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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₁)
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)
have rw₂ : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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₁)
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)
have rw₃ : 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]