awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Dioph
Goal:
this :
  Dioph (α := Fin2 4)
    {v : Vector3 ℕ 4 |
      1 < v &0 ∧
        v &1 ≤ v &3 ∧
          (v &2 = 1 ∧ v &3 = 0 ∨
            ∃ (u : ℕ) (w : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
              v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
                u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                  s * s - (b * b - 1) * t * t = 1 ∧
                    1 < b ∧
                      b ≡ 1 [MOD 4 * v &3] ∧
                        b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}
⊢ Dioph (α := Fin2 4) {v : Vector3 ℕ 4 | ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3}

Tactic:
Dioph.ext this fun v => matiyasevic.symm

Premises used: Dioph.ext, Pell.matiyasevic, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
this :
  Dioph (α := Fin2 4)
    {v : Vector3 ℕ 4 |
      1 < v &0 ∧
        v &1 ≤ v &3 ∧
          (v &2 = 1 ∧ v &3 = 0 ∨
            ∃ (u : ℕ) (w : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
              v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
                u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                  s * s - (b * b - 1) * t * t = 1 ∧
                    1 < b ∧
                      b ≡ 1 [MOD 4 * v &3] ∧
                        b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}
⊢ Dioph (α := Fin2 4) {v : Vector3 ℕ 4 | ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3}

Tactic:
exact Dioph.ext this fun v => matiyasevic.symm

Premises used: Dioph.ext, Pell.matiyasevic, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
⊢ DiophPFun (α := Fin2 2) fun (v : Vector3 ℕ 2) ↦ { Dom := 1 < v &0, get := fun (h : 1 < v &0) ↦ xn h (v &1) }

Tactic:
have : Dioph {v : Vector3 ℕ 3 | ∃ y, ∃ h : 1 < v &1, xn h (v &2) = v &0 ∧ yn h (v &2) = y} :=
    let D_pell := pell_dioph.reindex_dioph (Fin2 4) [&2, &3, &1, &0]
    (D∃) 3 D_pell
  (diophPFun_vec _).2 <|
    Dioph.ext this fun _ => ⟨fun ⟨_, h, xe, _⟩ => ⟨h, xe⟩, fun ⟨h, xe⟩ => ⟨_, h, xe, rfl⟩⟩

Premises used: Iff.mpr, _private.0.Dioph.xn_dioph.match_2, _private.0.Dioph.xn_dioph.match_1, Part.mk, Dioph.ext, Pell.xn, PFun.graph, setOf, Dioph.vec_ex1_dioph, Fin2.fz, Fin2.ofNat', Function.comp, Membership.mem, Exists, Prod.mk, Dioph.diophPFun_vec, Dioph.reindex_dioph, Vector3.nil, Fin2.fs, Vector3.cons, And, Pell.yn, And.intro, LT.lt, Iff.intro, Exists.intro, Dioph.pell_dioph, OfNat.ofNat, Eq, rfl, Fin2
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ Dioph (α := Fin2 3)
    {v : Vector3 ℕ 3 |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (x : ℕ) (y : ℕ),
                (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}

Tactic:
have : Dioph {v : Vector3 ℕ 3 |
    v &2 = 0 ∧ v &0 = 1 ∨ 0 < v &2 ∧
    (v &1 = 0 ∧ v &0 = 0 ∨ 0 < v &1 ∧
    ∃ w a t z x y : ℕ,
      (∃ a1 : 1 < a, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
      x ≡ y * (a - v &1) + v &0 [MOD t] ∧
      2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧
      a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)} :=
  (D&2 D= D.0 D∧ D&0 D= D.1) D∨ (D.0 D< D&2 D∧
    ((D&1 D= D.0 D∧ D&0 D= D.0) D∨ (D.0 D< D&1 D∧
    ((D∃) 3 <| (D∃) 4 <| (D∃) 5 <| (D∃) 6 <| (D∃) 7 <| (D∃) 8 <|
    pell_dioph.reindex_dioph (Fin2 9) [&4, &8, &1, &0] D∧
    (D≡ (D&1) (D&0 D* (D&4 D- D&7) D+ D&6) (D&3)) D∧
    D.2 D* D&4 D* D&7 D= D&3 D+ (D&7 D* D&7 D+ D.1) D∧
    D&6 D< D&3 D∧ D&7 D≤ D&5 D∧ D&8 D≤ D&5 D∧
    D&4 D* D&4 D- ((D&5 D+ D.1) D* (D&5 D+ D.1) D- D.1) D* (D&5 D* D&2) D* (D&5 D* D&2) D= D.1))) :)
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this :
  Dioph (α := Fin2 3)
    {v : Vector3 ℕ 3 |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (x : ℕ) (y : ℕ),
                (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}
⊢ DiophFn (α := α) fun (v : α → ℕ) ↦ f v ^ g v

Tactic:
diophFn_comp2 df dg <| (diophFn_vec _).2 <| Dioph.ext this fun v => Iff.symm <|
    eq_pow_of_pell.trans <| or_congr Iff.rfl <| and_congr Iff.rfl <| or_congr Iff.rfl <|
       and_congr Iff.rfl <|
        ⟨fun ⟨w, a, t, z, a1, h⟩ => ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
        fun ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩ => ⟨w, a, t, z, a1, h⟩⟩

Premises used: Iff.mpr, or_congr, Dioph.diophFn_vec, Dioph.ext, HMul.hMul, Pell.xn, Iff.rfl, HSub.hSub, Fin2.fz, Fin2.ofNat', _private.0.Dioph.pow_dioph.match_1, Function.comp, Exists, _private.0.Dioph.pow_dioph.match_2, LE.le, Fin2.fs, And, Nat.ModEq, HAdd.hAdd, Pell.yn, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.trans, OfNat.ofNat, Eq, Iff.symm, Pell.eq_pow_of_pell, Dioph.diophFn_comp2, rfl, and_congr
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this :
  Dioph (α := Fin2 3)
    {v : Vector3 ℕ 3 |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (x : ℕ) (y : ℕ),
                (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}
⊢ DiophFn (α := α) fun (v : α → ℕ) ↦ f v ^ g v

Tactic:
exact diophFn_comp2 df dg <| (diophFn_vec _).2 <| Dioph.ext this fun v => Iff.symm <|
    eq_pow_of_pell.trans <| or_congr Iff.rfl <| and_congr Iff.rfl <| or_congr Iff.rfl <|
       and_congr Iff.rfl <|
        ⟨fun ⟨w, a, t, z, a1, h⟩ => ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
        fun ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩ => ⟨w, a, t, z, a1, h⟩⟩

Premises used: Iff.mpr, or_congr, Dioph.diophFn_vec, Dioph.ext, HMul.hMul, Pell.xn, Iff.rfl, HSub.hSub, Fin2.ofNat', Exists, LE.le, _private.0.match_1, And, Nat.ModEq, HAdd.hAdd, Pell.yn, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.trans, _private.0.match_2, OfNat.ofNat, Eq, Iff.symm, Pell.eq_pow_of_pell, Dioph.diophFn_comp2, rfl, and_congr
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
have hn : 0 < (n : ℝ) + 1 := mod_cast Nat.succ_pos _
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
have hfu := fun m : ℤ => mul_lt_of_lt_one_left hn <| fract_lt_one (ξ * ↑m)
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
j k : ℤ
rw : |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
| |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [mul_comm, le_div_iff₀ hn, ← abs_of_pos hn, ← abs_mul]

Premises used: abs_mul, mul_comm, abs_of_pos, le_div_iff₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
conv : ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
conv in |_| ≤ _ => rw [mul_comm, le_div_iff₀ hn, ← abs_of_pos hn, ← abs_mul]

Premises used: abs_mul, mul_comm, abs_of_pos, le_div_iff₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
pos :
  ∀ (H : ∃ m ∈ D, f m = (↑n : ℤ)),
    ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
neg :
  ∀ (H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)),
    ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
by_cases! H : ∃ m ∈ D, f m = n
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∃ m ∈ D, f m = (↑n : ℤ)
pos :
  ∀ (m : ℤ) (hm : m ∈ D) (hf : f m = (↑n : ℤ)),
    ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
obtain ⟨m, hm, hf⟩ := H
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
⊢ (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
have hf' : ((n : ℤ) : ℝ) ≤ fract (ξ * m) * (n + 1) := hf ▸ floor_le (fract (ξ * m) * (n + 1))
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ f 0 = 0

Tactic:
simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]

Premises used: Int.cast_zero, MulZeroClass.zero_mul, Int.floor_zero, MulZeroClass.mul_zero, Int.fract_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ f 0 = 0

Tactic:
have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hf₀ : f 0 = 0
⊢ 0 < m

Tactic:
Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1

Premises used: Finset.mem_Icc, And.left, Iff.mp, Ne.lt_of_le, LT.lt.ne
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hf₀ : f 0 = 0
refine : ∀ (h : 0 = m), 0 = n
⊢ 0 < m

Tactic:
refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1

Premises used: Finset.mem_Icc, And.left, Iff.mp, Ne.lt_of_le, LT.lt.ne
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hf₀ : f 0 = 0
h : 0 = m
⊢ 0 = n

Tactic:
mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)

Premises used: congrArg, cast, Eq.rec, Nat.cast, Nat.cast_inj._simp_1, congrFun', Nat.cast_zero, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hf₀ : f 0 = 0
h : 0 = m
⊢ 0 = n

Tactic:
exact mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)

Premises used: Eq.rec, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ 0 < m

Tactic:
have hm₀ : 0 < m := by
      have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
      refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1
      exact mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hm₀ : 0 < m
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, ?_⟩

Premises used: Int.cast, HMul.hMul, Int.floor, Finset.mem_Icc, And.right, HAdd.hAdd, And.intro, Exists.intro, Iff.mp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hm₀ : 0 < m
pos : |(ξ * (↑m : ℝ) - (↑(⌊ξ * (↑m : ℝ)⌋ + 1) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
refine ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, ?_⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hm₀ : 0 < m
pos :
  -1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ∧
    (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 1
⊢ |(ξ * (↑m : ℝ) - (↑(⌊ξ * (↑m : ℝ)⌋ + 1) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
rw [cast_add, ← sub_sub, sub_mul, cast_one, one_mul, abs_le]

Premises used: abs_le, Int.cast_add, sub_mul, sub_sub, one_mul, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hm₀ : 0 < m
⊢ -1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ∧
    (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 1

Tactic:
⟨le_sub_iff_add_le.mpr ?_, sub_le_iff_le_add.mpr <| le_of_lt <| (hfu m).trans <| lt_one_add _⟩

Premises used: Iff.mpr, le_of_lt, sub_le_iff_le_add, And.intro, LT.lt.trans, le_sub_iff_add_le, lt_one_add
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hm₀ : 0 < m
pos : -1 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ -1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ∧
    (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 1

Tactic:
refine
      ⟨le_sub_iff_add_le.mpr ?_, sub_le_iff_le_add.mpr <| le_of_lt <| (hfu m).trans <| lt_one_add _⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hm₀ : 0 < m
⊢ -1 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simpa only [neg_add_cancel_comm_assoc] using hf'

Premises used: neg_add_cancel_comm_assoc
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
rw : (HSub.hSub (α := ℤ) (↑n : ℤ) 0).toNat < (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 0).toNat
⊢ card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D

Tactic:
rw [card_Icc, card_Ico]

Premises used: Int.card_Ico, Int.card_Icc
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
⊢ (HSub.hSub (α := ℤ) (↑n : ℤ) 0).toNat < (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 0).toNat

Tactic:
lt_add_one n

Premises used: lt_add_one, Int.toNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
⊢ (HSub.hSub (α := ℤ) (↑n : ℤ) 0).toNat < (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 0).toNat

Tactic:
exact lt_add_one n

Premises used: lt_add_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
⊢ card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D

Tactic:
have hD : #(Ico (0 : ℤ) n) < #D := by rw [card_Icc, card_Ico]; exact lt_add_one n
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
⊢ ∀ (m : ℤ), f m ≤ (↑n : ℤ)

Tactic:
have hfu' : ∀ m, f m ≤ n := fun m => lt_add_one_iff.mp (floor_lt.mpr (mod_cast hfu m))
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
⊢ ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)

Tactic:
have hwd : ∀ m : ℤ, m ∈ D → f m ∈ Ico (0 : ℤ) n := fun x hx =>
      mem_Ico.mpr
        ⟨floor_nonneg.mpr (mul_nonneg (fract_nonneg (ξ * x)) hn.le), Ne.lt_of_le (H x hx) (hfu' x)⟩