awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst_1 : Fintype G
inst_2 : DecidableEq G
hε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
simp_rw :
  ε *
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ) + (↑(Fintype.card G) : ℝ))
          2 /
        9) ≤
    (↑(#A) : ℝ)
⊢ ε / 9 * (↑(HPow.hPow (β := ℕ) (Fintype.card G + Fintype.card G + Fintype.card G) 2) : ℝ) ≤
    (↑(#(triangleIndices A)) : ℝ)

Tactic:
simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]

Premises used: Nat.cast_add, _private.0.Corners.card_triangleIndices, mul_comm_div, Nat.cast_pow
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst_1 : Fintype G
inst_2 : DecidableEq G
hε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
ring_nf : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
⊢ ε *
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ) + (↑(Fintype.card G) : ℝ))
          2 /
        9) ≤
    (↑(#A) : ℝ)

Tactic:
ring_nf
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst_1 : Fintype G
inst_2 : DecidableEq G
hε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)

Tactic:
simpa only [mul_comm] using hε

Premises used: mul_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 × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
rw :
  ∀ (hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G) (A : Finset (G × G))
    (hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ))
    (hA : IsCornerFree (↑A : Set (G × G))), False
⊢ False

Tactic:
rw [cornersTheoremBound, Nat.add_one_le_iff] at hG

Premises used: cornersTheoremBound, Nat.add_one_le_iff
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(Fintype.card.{u_1} (G × G)) : ℝ)

Tactic:
have := hAε.trans (Nat.cast_le.2 A.card_le_univ)
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(Fintype.card.{u_1} (G × G)) : ℝ)
⊢ ε * HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)

Tactic:
simp only [sq, Nat.cast_mul, Fintype.card_prod] at this

Premises used: sq, Fintype.card_prod, Nat.cast_mul
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
this :
  ε * HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)
rwa : 0 < HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)
⊢ ε ≤ 1

Tactic:
rwa [mul_le_iff_le_one_left] at this

Premises used: mul_le_iff_le_one_left
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
this :
  ε * HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
⊢ ε ≤ 1

Tactic:
have hε₁ : ε ≤ 1 := by
    have := hAε.trans (Nat.cast_le.2 A.card_le_univ)
    simp only [sq, Nat.cast_mul, Fintype.card_prod] at this
    rwa [mul_le_iff_le_one_left] at this
    positivity
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
⊢ NoAccidental (triangleIndices A)

Tactic:
have := noAccidental hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ Fintype.card G ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : (triangleRemovalBound (ε / 9) * 27)⁻¹ < (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ 0 < triangleRemovalBound (ε / 9) * 27

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
rw :
  ∀ (hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)) (A : Finset (G × G))
    (hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ))
    (hA : IsCornerFree (↑A : Set (G × G))) (hε₁ : ε ≤ 1) (this : NoAccidental (triangleIndices A)), False
⊢ False

Tactic:
rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀' (by positivity)] at hG

Premises used: Nat.floor_lt', inv_lt_iff_one_lt_mul₀'
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
refine :
  triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
⊢ False

Tactic:
refine hG.not_ge (le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < card G ^ 2))

Premises used: le_of_mul_le_mul_right, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤
    (↑(#((graph (triangleIndices A)).cliqueFinset 3)) : ℝ)

Tactic:
have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ :
  triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤
    (↑(#((graph (triangleIndices A)).cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)

Tactic:
rw [card_triangles, card_triangleIndices] at h₁

Premises used: _private.0.Corners.card_triangleIndices, SimpleGraph.TripartiteFromTriangles.card_triangles
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)
⊢ triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤
    (↑(Fintype.card.{u_1} (G × G)) : ℝ)

Tactic:
h₁.trans (Nat.cast_le.2 <| card_le_univ _)

Premises used: Iff.mpr, Finset.card_le_univ, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)
h :
  triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
    triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3
h₂ : 1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 = (↑(Fintype.card.{u_1} (G × G)) : ℝ)
⊢ triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2

Tactic:
convert! h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1

Premises used: Iff.mpr, Finset.card_le_univ, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)
h :
  triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
    triangleRemovalBound (ε / 9) *
      HPow.hPow (β := ℕ) ((↑(Fintype.card G) : ℝ) + HAdd.hAdd (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ))
        3
⊢ triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
    triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)
h :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
    HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)
⊢ 1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 = (↑(Fintype.card.{u_1} (G × G)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)
⊢ triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
    triangleRemovalBound (ε / 9) *
      HPow.hPow (β := ℕ) ((↑(Fintype.card G) : ℝ) + HAdd.hAdd (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ))
        3

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤ (↑(#A) : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
    HMul.hMul (α := ℝ) (↑(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 : 1 < triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ)
A : Finset (G × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
have have₁ have₂ :
  ∀
    (h₁ :
      triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤
        (↑(#((graph (triangleIndices A)).cliqueFinset 3)) : ℝ)),
    triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) *
        HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
      1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
have₃ :
  ∀
    (h₁ :
      triangleRemovalBound (ε / 9) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3 ≤
        (↑(#A) : ℝ)),
    triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) *
        HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
      1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
⊢ triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2

Tactic:
classical
  have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset
  rw [card_triangles, card_triangleIndices] at h₁
  convert! h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1 <;> simp <;> ring

Premises used: _private.0.Corners.card_triangleIndices, SimpleGraph.TripartiteFromTriangles.card_triangles
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : A ⊆ range n ×ˢ range n
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (ℕ × ℕ))
⊢ (↑A : Set (ℕ × ℕ)) ⊆ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)

Tactic:
rw [← coe_subset, coe_product] at hAn

Premises used: Finset.coe_product, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : A ⊆ range n ×ˢ range n
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (ℕ × ℕ))
hAn₁ : (↑A : Set (ℕ × ℕ)) ⊆ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
⊢ ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)

Tactic:
rw [← coe_subset, coe_product] at hAn

Premises used: Finset.coe_product, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : A ⊆ range n ×ˢ range n
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (ℕ × ℕ))
hAn₁ : (↑A : Set (ℕ × ℕ)) ⊆ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
hAε₁ : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)
⊢ IsCornerFree (↑A : Set (ℕ × ℕ))

Tactic:
rw [← coe_subset, coe_product] at hAn

Premises used: Finset.coe_product, Finset.coe_subset
-- 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 (↑A : Set (ℕ × ℕ))
rw :
  ∀ a ∈ (↑A : Set (ℕ × ℕ)),
    Prod.map (α₁ := Fin (2 * n).succ) (β₁ := Fin (2 * n).succ) Fin.val Fin.val (Prod.map Nat.cast Nat.cast a) = id a
⊢ (↑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 (ℕ × ℕ)))

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 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : (↑A : Set (ℕ × ℕ)) ⊆ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (ℕ × ℕ))
simp : ∀ (a b : ℕ), (a, b) ∈ A → a < 2 * n + 1 ∧ b < 2 * n + 1
⊢ ∀ a ∈ (↑A : Set (ℕ × ℕ)),
    Prod.map (α₁ := Fin (2 * n).succ) (β₁ := Fin (2 * n).succ) Fin.val Fin.val (Prod.map Nat.cast Nat.cast a) = id a

Tactic:
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]

Premises used: Fin.val_natCast, Nat.succ_eq_add_one, Prod.mk.injEq, Nat.mod_succ_eq_iff_lt, Prod.map_apply, Prod.forall, Finset.mem_coe, id_eq
-- 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 (↑A : Set (ℕ × ℕ))
a b : ℕ
hab : (a, b) ∈ A
⊢ (a, b) ∈ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)

Tactic:
have := hAn hab
-- 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 (↑A : Set (ℕ × ℕ))
a b : ℕ
hab : (a, b) ∈ A
this : (a, b) ∈ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
⊢ a < n ∧ b < n

Tactic:
simp at this
-- 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 (↑A : Set (ℕ × ℕ))
a b : ℕ
hab : (a, b) ∈ A
this : a < n ∧ b < n
⊢ a < 2 * n + 1 ∧ b < 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 (↑A : Set (ℕ × ℕ))
⊢ (↑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 (ℕ × ℕ)))

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
    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 (↑A : Set (ℕ × ℕ))
this :
  (↑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 (ℕ × ℕ)))
⊢ 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 (ℕ × ℕ))))

Tactic:
rw [this] at 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 (↑A : Set (ℕ × ℕ))
this :
  (↑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 (ℕ × ℕ)))
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 (ℕ × ℕ))))
⊢ (↑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 (ℕ × ℕ)))

Tactic:
rw [this] at 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 :
  (↑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 (ℕ × ℕ)))
⊢ 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))