awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁)
rw₃ : 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]
-- 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₁)
rw₃ : y₂ - x₂ = y₁ - x₁
rw₄ : y₂ + x₁ = y₁ + x₂
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)
have rw₅ : x₁ + y₂ = 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₁)
rw₃ : y₂ - x₂ = y₁ - x₁
rw₄ : y₂ + x₁ = y₁ + x₂
rw₅ : x₁ + y₂ = y₁ + x₂
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)
have rw₆ : x₂ + y₁ = 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₁)
rw₃ : y₂ - x₂ = y₁ - x₁
rw₄ : y₂ + x₁ = y₁ + x₂
rw₅ : x₁ + y₂ = y₁ + x₂
rw₆ : x₂ + y₁ = 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]
-- 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}
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₂
⊢ False
have this₁ : y₁ - x₂ = y₁ - x₁
Tactic: have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
    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)
let let₁ let₂ : False
⊢ False
have let₃ : let 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
Tactic: classical
  let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A
  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])
  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
  have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
    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]
  exact hx₁x₂ <| by simpa using this.symm
-- 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)
let let₁ let₂ : False
let₃ :
  let 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
⊢ False
have let₄ : let 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₂), False
Tactic: classical
  let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A
  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])
  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
  have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
    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]
  exact hx₁x₂ <| by simpa using this.symm
-- 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)
let let₁ let₂ : False
let₃ :
  let 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
let₄ :
  let 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₂), False
⊢ False
have let₅ : let 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₂)
  (this : y₁ - x₂ = y₁ - x₁), False
Tactic: classical
  let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A
  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])
  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
  have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
    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]
  exact hx₁x₂ <| by simpa using this.symm
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
⊢ False
have hAn₁ : (↑A : Set ℕ) ⊆ Set.Iio n
Tactic: rw [← coe_subset, coe_range] at hAn
Cleared hypotheses: hAn, hAε, hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
⊢ (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
have rw : ∀ a ∈ (↑A : Set ℕ), (↑(↑a : Fin (2 * n).succ) : ℕ) = 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 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
⊢ ∀ a ∈ (↑A : Set ℕ), (↑(↑a : Fin (2 * n).succ) : ℕ) = id a
have simp : ∀ a ∈ A, a < 2 * n + 1
Tactic: simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
a : ℕ
ha : a ∈ A
⊢ a < 2 * n + 1
have this : a ∈ Set.Iio n
Tactic: have := hAn ha
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
a : ℕ
ha : a ∈ A
this : a ∈ Set.Iio n
⊢ a < 2 * n + 1
have this₁ : a < n
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
⊢ False
have this : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
Tactic: have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
    rintro a ha
    have := hAn ha
    simp at this
    lia
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (↑A : Set ℕ)
this : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
⊢ False
have hA₁ : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (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 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (α := Fin (2 * n + 1)) ((fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) '' (↑A : Set ℕ))
⊢ False
have this₁ : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
Tactic: rw [← coe_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ cornersTheoremBound (ε / 3) ≤ Fintype.card (Fin (2 * n + 1))
have simp : cornersTheoremBound (ε / 3) ≤ 2 * n + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ False
have refine : ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
  (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
Tactic: refine roth_3ap_theorem (ε / 3) (by positivity) (by simp; lia) _ ?_ this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) ≤ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ))
have hbc : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ 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 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ Eq (α := ℝ) (↑(#A) : ℝ) (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
have rw : Set.InjOn (β := Fin (2 * n + 1)) (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) (↑A : Set ℕ)
Tactic: rw [card_image_of_injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ Set.Iio n ⊆ Set.Iio (2 * n).succ
have simp : n ≤ 2 * n + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
    (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
have _ : ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) = ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
Tactic: calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
_ : ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) = ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
⊢ ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
    (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
have _₁ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) ≤ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ))
Tactic: calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (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 : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
_ : ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) = ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
_₁ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) ≤ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ))
⊢ ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
    (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
have _₂ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) = ε * (↑n : ℝ)
Tactic: calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia