awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
have pos : |(ξ * (↑m : ℝ) - (↑(⌊ξ * (↑m : ℝ)⌋ + 1) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: refine ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
⊢ |(ξ * (↑m : ℝ) - (↑(⌊ξ * (↑m : ℝ)⌋ + 1) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have pos : -1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ∧
  (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 1
Tactic: rw [cast_add, ← sub_sub, sub_mul, cast_one, one_mul, abs_le]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
have pos : -1 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ (ξ * (↑m : ℝ) - (↑⌊ξ * (↑m : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: refine
      ⟨le_sub_iff_add_le.mpr ?_, sub_le_iff_le_add.mpr <| le_of_lt <| (hfu m).trans <| lt_one_add _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
have rw : (HSub.hSub (α := ℤ) (↑n : ℤ) 0).toNat < (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 0).toNat
Tactic: rw [card_Icc, card_Ico]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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 : ℤ)
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
Tactic: have hD : #(Ico (0 : ℤ) n) < #D := by rw [card_Icc, card_Ico]; exact lt_add_one n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have hfu' : ∀ (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))
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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 : ℤ)
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have hwd : ∀ 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)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
have obtain : ∀ (x : ℤ) (hx : x ∈ D) (y : ℤ) (hy : y ∈ D) (x_ne_y : x ≠ y) (hxy : f x = f y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
Tactic: obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
have inl : ∀ (h : x < y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
Tactic: rcases lt_trichotomy x y with (h | h | h)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
inl : ∀ (h : x < y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
have inr : ∀ (h : x = y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
Tactic: rcases lt_trichotomy x y with (h | h | h)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
inl : ∀ (h : x < y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
inr : ∀ (h : x = y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
have inr₁ : ∀ (h : y < x), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
Tactic: rcases lt_trichotomy x y with (h | h | h)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have neg : ∀ (x : ℤ) (hx : x ∈ D) (y : ℤ) (hy : y ∈ D) (x_lt_y : x < y) (hxy : f x = f y),
  ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ : ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y := by
      obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd
      rcases lt_trichotomy x y with (h | h | h)
      exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have neg : |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: refine
      ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
        sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have h : |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| =
  |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1|
Tactic: convert_to |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
h :
  |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| =
    |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1|
⊢ |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have neg : |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: convert_to |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| =
    |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1|
have h : (ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
  fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h : (ξ * HSub.hSub (α := ℝ) (↑y : ℝ) (↑x : ℝ) - HSub.hSub (α := ℝ) (↑⌊ξ * (↑y : ℝ)⌋ : ℝ) (↑⌊ξ * (↑x : ℝ)⌋ : ℝ)) *
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
  fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have obtain : ∀ (j k : ℤ) (hk₀ : 0 < k) (hk₁ : k ≤ (↑n : ℤ)) (h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1),
  ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hk : (↑k.toNat : ℤ) = k
Tactic: have hk := toNat_of_nonneg hk₀.le
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk : (↑k.toNat : ℤ) = k
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hk₂ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
Tactic: rw [← hk] at hk₀ hk₁ h
Cleared hypotheses: hk₀, hk₁, h, hk
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk : (↑k.toNat : ℤ) = k
hk₂ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hk₃ : LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)
Tactic: rw [← hk] at hk₀ hk₁ h
Cleared hypotheses: hk₀, hk₁, h, hk
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk : (↑k.toNat : ℤ) = k
hk₂ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
hk₃ : LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h₁ : |(↑(↑k.toNat : ℤ) : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [← hk] at hk₀ hk₁ h
Cleared hypotheses: hk₀, hk₁, h, hk
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n
have obtain : ∀ (j k : ℤ) (hk₀ : 0 < k) (hk₁ : k ≤ (↑n : ℤ)) (h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1),
  ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n
Tactic: obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n
have hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
Tactic: have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
⊢ (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
have h₁ : HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ) = Rat.divInt j k
Tactic: convert! le_of_dvd hk₀ (Rat.den_dvd j k)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n
have hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
Tactic: have hden : ((j / k : ℚ).den : ℤ) ≤ k := by
    convert! le_of_dvd hk₀ (Rat.den_dvd j k)
    exact Rat.intCast_div_eq_divInt _ _
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n
have refine : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| ≤
  1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ))
Tactic: refine ⟨j / k, ?_, Nat.cast_le.mp (hden.trans hk₁)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| ≤
    1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ))
have rw : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ) ≤
  1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [← div_div, le_div_iff₀ (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ) ≤
    1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have refine : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: refine (mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa₁ : |ξ - HDiv.hDiv (α := ℝ) (↑(↑j : ℚ) : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₁ : |ξ - HDiv.hDiv (α := ℝ) (↑(↑j : ℚ) : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa₂ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]