awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
hs : IsCornerFree (↑A : Set (G × G))
a a' b b' c c' : G
ha : (a', b, c) ∈ triangleIndices A
hb : (a, b', c) ∈ triangleIndices A
hc : (a, b, c') ∈ triangleIndices A
ha₁ : (a', b) ∈ A ∧ c = a' + b
⊢ a = a' ∨ b = b' ∨ c = c'
have hb₁ : (a, b') ∈ A ∧ c = a + b'
Tactic: simp only [mk_mem_triangleIndices] at ha hb hc
Cleared hypotheses: ha, hb, hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
hs : IsCornerFree (↑A : Set (G × G))
a a' b b' c c' : G
ha : (a', b, c) ∈ triangleIndices A
hb : (a, b', c) ∈ triangleIndices A
hc : (a, b, c') ∈ triangleIndices A
ha₁ : (a', b) ∈ A ∧ c = a' + b
hb₁ : (a, b') ∈ A ∧ c = a + b'
⊢ a = a' ∨ b = b' ∨ c = c'
have hc₁ : (a, b) ∈ A ∧ c' = a + b
Tactic: simp only [mk_mem_triangleIndices] at ha hb hc
Cleared hypotheses: ha, hb, hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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) : ℝ)
⊢ (graph (triangleIndices A)).FarFromTriangleFree (ε / 9)
have refine : ε / 9 * (↑(HPow.hPow (β := ℕ) (Fintype.card G + Fintype.card G + Fintype.card G) 2) : ℝ) ≤ (↑(#(triangleIndices A)) : ℝ)
Tactic: refine farFromTriangleFree _ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
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) : ℝ)
⊢ ε / 9 * (↑(HPow.hPow (β := ℕ) (Fintype.card G + Fintype.card G + Fintype.card G) 2) : ℝ) ≤
    (↑(#(triangleIndices A)) : ℝ)
have simp_rw : ε *
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ) + (↑(Fintype.card G) : ℝ))
        2 /
      9) ≤
  (↑(#A) : ℝ)
Tactic: simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]
-- 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 × G)
hAε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
hA : IsCornerFree (↑A : Set (G × G))
⊢ False
have 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
Tactic: rw [cornersTheoremBound, Nat.add_one_le_iff] at hG
Cleared hypotheses: hG, A, hAε, hA
-- 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 : ⌊(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
have this : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(Fintype.card.{u_1} (G × G)) : ℝ)
Tactic: have := hAε.trans (Nat.cast_le.2 A.card_le_univ)
-- 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 : ⌊(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)) : ℝ)
⊢ ε ≤ 1
have this₁ : ε * 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
Cleared hypotheses: 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 : ⌊(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) : ℝ)
⊢ ε ≤ 1
have rwa : 0 < HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)
Tactic: rwa [mul_le_iff_le_one_left] at this
-- 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 : ⌊(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
have hε₁ : ε ≤ 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
-- 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 : ⌊(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
⊢ False
have this : NoAccidental (triangleIndices A)
Tactic: have := noAccidental hA
-- 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 : ⌊(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
have 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
Tactic: rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀' (by positivity)] at hG
Cleared hypotheses: hG, A, hAε, hA, hε₁, 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 : 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
have refine : triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
  1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
Tactic: refine hG.not_ge (le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < card G ^ 2))
-- 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 : 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) * 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 ≤
  (↑(#((graph (triangleIndices A)).cliqueFinset 3)) : ℝ)
Tactic: have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset
-- 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 : 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) * 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) : ℝ)
Tactic: rw [card_triangles, card_triangleIndices] at h₁
Cleared hypotheses: h₁
-- 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 : 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 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
have 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
Tactic: convert! h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1
-- 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 : 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
⊢ triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
have h₂ : 1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 = (↑(Fintype.card.{u_1} (G × G)) : ℝ)
Tactic: convert! h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1
-- 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 : 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.{u_1} (G ⊕ G ⊕ G)) : ℝ) 3
have 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
Tactic: simp
-- 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 : 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) : ℝ)
⊢ 1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 = (↑(Fintype.card.{u_1} (G × G)) : ℝ)
have h : HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 =
  HMul.hMul (α := ℝ) (↑(Fintype.card G) : ℝ) (↑(Fintype.card G) : ℝ)
Tactic: simp
-- 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 : 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) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
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
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
-- 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 : 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
⊢ triangleRemovalBound (ε / 9) * 27 * (↑(Fintype.card G) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
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 (ℕ × ℕ))
⊢ False
have hAn₁ : (↑A : Set (ℕ × ℕ)) ⊆ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
Tactic: rw [← coe_subset, coe_product] at hAn
Cleared hypotheses: hAn, hAε, hA
-- 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 (↑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 (ℕ × ℕ)))
have 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
Tactic: rw [Set.image_image, Set.image_congr, Set.image_id]
-- 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 (↑A : Set (ℕ × ℕ))
⊢ ∀ 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
have simp : ∀ (a b : ℕ), (a, b) ∈ A → a < 2 * n + 1 ∧ b < 2 * n + 1
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]
-- 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 (↑A : Set (ℕ × ℕ))
a b : ℕ
hab : (a, b) ∈ A
⊢ a < 2 * n + 1 ∧ b < 2 * n + 1
have this : (a, b) ∈ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
Tactic: have := hAn hab
-- 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 (↑A : Set (ℕ × ℕ))
a b : ℕ
hab : (a, b) ∈ A
this : (a, b) ∈ (↑(range n) : Set ℕ) ×ˢ (↑(range n) : Set ℕ)
⊢ a < 2 * n + 1 ∧ b < 2 * n + 1
have this₁ : a < n ∧ b < n
Tactic: simp at this
Cleared hypotheses: this
-- 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 (↑A : Set (ℕ × ℕ))
⊢ False
have 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 (ℕ × ℕ)))
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
-- 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 (↑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 (ℕ × ℕ)))
⊢ False
have 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 (ℕ × ℕ))))
Tactic: rw [this] at hA
Cleared hypotheses: hA, this
-- 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 :
  (↑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 (ℕ × ℕ)))
⊢ False
have this₁ : 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))
-- 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 : 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)))
have 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)))
Tactic: refine Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_
-- 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
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)))
have hx₁ : x.1 < n ∧ x.2 < n
Tactic: simp only [coe_range, Set.mem_prod, Set.mem_Iio] at hx
Cleared hypotheses: hx