awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
h : (↑u : ℝ) - HSub.hSub (α := ℝ) 1 2⁻¹ = (↑u : ℝ) + -(1 / 2)
⊢ (↑u : ℝ) - HSub.hSub (α := ℝ) 1 2⁻¹ < ξ

Tactic:
convert! h₁ using 1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ (↑u : ℝ) + -HSub.hSub (α := ℝ) 1 2⁻¹ = (↑u : ℝ) + -(1 / 2)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ ⌊(fract ξ)⁻¹⌋ = 1

Tactic:
have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 := by
          rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
          refine ⟨(fract_lt_one ξ).le, ?_⟩
          rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
          convert! h₁ using 1
          rw [sub_eq_add_neg]
          norm_num
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1
h : (↑u : ℚ) = ξ.convergent 1
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n

Tactic:
use 1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1
⊢ (↑u : ℚ) = ξ.convergent 1

Tactic:
simp [convergent, hξ₁, hξ₂, cast_sub, cast_one]

Premises used: Int.cast_sub, Real.convergent, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
⊢ 0 < u - ⌊ξ⌋ * (↑v : ℤ)

Tactic:
obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h

Premises used: Iff.mpr, _private.0.Real.aux₂, Nat.cast_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
⊢ u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)

Tactic:
obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h

Premises used: Iff.mpr, _private.0.Real.aux₂, Nat.cast_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
⊢ Ne (α := ℚ) (↑v : ℚ) 0

Tactic:
have Hv : (v : ℚ) ≠ 0 := (Nat.cast_pos.mpr (zero_lt_one.trans ht)).ne'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
zify : LT.lt (α := ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ) (↑v : ℤ)
⊢ (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v

Tactic:
zify
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
rwa rwa₁ rwa₂ rwa₃ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
⊢ LT.lt (α := ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ) (↑v : ℤ)

Tactic:
rwa [toNat_of_nonneg huv₀.le]

Premises used: Int.toNat_of_nonneg, LT.lt.le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
⊢ (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v

Tactic:
have huv₁' : (u - ⌊ξ⌋ * v).toNat < v := by zify; rwa [toNat_of_nonneg huv₀.le]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
⊢ ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)

Tactic:
have inv : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * ↑v).toNat :=
      (toNat_of_nonneg huv₀.le).symm ▸ invariant (Nat.cast_le.mpr ht) h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
h₁ :
  ∀ (n : ℕ) (hn : HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ) = (fract ξ)⁻¹.convergent n),
    ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
obtain ⟨n, hn⟩ := ih (u - ⌊ξ⌋ * v).toNat huv₁' inv

Premises used: HMul.hMul, Int.floor, HSub.hSub, Nat.cast, Int.toNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
n : ℕ
hn : HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ) = (fract ξ)⁻¹.convergent n
h₁ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
use n + 1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
n : ℕ
hn : HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ) = (fract ξ)⁻¹.convergent n
h₁ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹
h₂ :
  HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) =
    (↑⌊ξ⌋ : ℚ) + (HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ))⁻¹
h₃ :
  HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) =
    (↑⌊ξ⌋ : ℚ) + ((↑(↑v : ℤ) : ℚ) / ((↑u : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ)))⁻¹
h₄ :
  HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + ((↑v : ℚ) / ((↑u : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ)))⁻¹
h₅ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + ((↑u : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ)) / (↑v : ℚ)
h₆ :
  HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) =
    (↑⌊ξ⌋ : ℚ) + (HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ) / (↑v : ℚ))
h₇ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + (HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) - (↑⌊ξ⌋ : ℚ))
h₈ h₉ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)

Tactic:
rw [convergent_succ, ← hn,
      (mod_cast toNat_of_nonneg huv₀.le : ((u - ⌊ξ⌋ * v).toNat : ℚ) = u - ⌊ξ⌋ * v),
      cast_natCast, inv_div, sub_div, mul_div_cancel_right₀ _ Hv, add_sub_cancel]

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, Int.floor, congrArg, Int.toNat_of_nonneg, HSub.hSub, cast, Real.convergent_succ, LT.lt.le, sub_div, Nat.cast, mul_div_cancel_right₀, Int.cast_inj._simp_1, Int.cast_mul._simp_1, add_sub_cancel, inv_div, Int.toNat, Eq.symm, Eq, Eq.trans, Int.cast_sub._simp_1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ ∃ (n : ℕ), q = ξ.convergent n

Tactic:
q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩

Premises used: Rat.num_div_den, Eq.rec, And.intro, Real.exists_rat_eq_convergent'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
refine_1 : IsCoprime q.num (↑q.den : ℤ)
refine_2 : ∀ (hd : Eq (α := ℤ) (↑q.den : ℤ) 1), -(1 / 2) < ξ - (↑q.num : ℝ)
refine_3 :
  |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
⊢ ∃ (n : ℕ), q = ξ.convergent n

Tactic:
refine q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ IsCoprime q.num (↑q.den : ℤ)

Tactic:
isCoprime_iff_nat_coprime.mpr (natAbs_natCast q.den ▸ q.reduced)

Premises used: Iff.mpr, Rat.reduced, Int.isCoprime_iff_nat_coprime, Rat.den, Eq.rec, Int.natAbs_natCast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ IsCoprime q.num (↑q.den : ℤ)

Tactic:
exact isCoprime_iff_nat_coprime.mpr (natAbs_natCast q.den ▸ q.reduced)

Premises used: Iff.mpr, Int.isCoprime_iff_nat_coprime
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hd : Eq (α := ℤ) (↑q.den : ℤ) 1
⊢ |ξ - (↑(↑q.num : ℚ) : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Rat.den (↑q.num : ℚ)) : ℝ) 2)

Tactic:
rw [← q.den_eq_one_iff.mp (Nat.cast_eq_one.mp hd)] at h

Premises used: Nat.cast_eq_one, Iff.mp, Rat.den_eq_one_iff
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hd : Eq (α := ℤ) (↑q.den : ℤ) 1
h₁ : |ξ - (↑(↑q.num : ℚ) : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Rat.den (↑q.num : ℚ)) : ℝ) 2)
⊢ Eq (α := ℤ) (↑q.den : ℤ) 1

Tactic:
rw [← q.den_eq_one_iff.mp (Nat.cast_eq_one.mp hd)] at h

Premises used: Nat.cast_eq_one, Iff.mp, Rat.den_eq_one_iff
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑(↑q.num : ℚ) : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Rat.den (↑q.num : ℚ)) : ℝ) 2)
hd : Eq (α := ℤ) (↑q.den : ℤ) 1
⊢ -(1 / 2) < ξ - (↑q.num : ℝ)

Tactic:
simpa only [Rat.den_intCast, Nat.cast_one, one_pow, mul_one] using (abs_lt.mp h).1

Premises used: one_pow, Rat.den_intCast, And.left, Iff.mp, abs_lt, mul_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)

Tactic:
obtain ⟨hq₀, hq₁⟩ := aux₀ (Nat.cast_pos.mpr q.pos)

Premises used: Iff.mpr, Nat.cast_pos, Rat.pos, _private.0.Real.aux₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1

Tactic:
obtain ⟨hq₀, hq₁⟩ := aux₀ (Nat.cast_pos.mpr q.pos)

Premises used: Iff.mpr, Nat.cast_pos, Rat.pos, _private.0.Real.aux₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
hq₁ : 0 < HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1
⊢ 0 < (↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1)

Tactic:
replace hq₁ := mul_pos hq₀ hq₁
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
hq₁ : 0 < (↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1)
⊢ 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)

Tactic:
have hq₂ : (0 : ℝ) < 2 * (q.den * q.den) := mul_pos zero_lt_two (mul_pos hq₀ hq₀)
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
hq₁ : 0 < (↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑q.den : ℝ)

Tactic:
rw [cast_natCast] at *

Premises used: Int.cast_natCast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
hq₁ : 0 < (↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
hq₃ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
⊢ 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)

Tactic:
rw [cast_natCast] at *

Premises used: Int.cast_natCast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
hq₁ : 0 < (↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
hq₃ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₄ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
⊢ 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)

Tactic:
rw [cast_natCast] at *

Premises used: Int.cast_natCast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Rat.divInt q.num (↑q.den : ℤ) = Rat.divInt q.num (↑q.den : ℤ)
⊢ HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
refine_3 : |ξ - (↑q : ℝ)| < ((↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1))⁻¹
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)| < ((↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1))⁻¹

Tactic:
rw [(by norm_cast : (q.num / q.den : ℝ) = (q.num / q.den : ℚ)), Rat.num_div_den]

Premises used: Rat.num_div_den
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
rw : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
⊢ 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2) < ((↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1))⁻¹

Tactic:
rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]

Premises used: sub_pos, sq, one_div, one_div_lt_one_div
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
ring_nf : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
⊢ 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑q.den : ℝ)

Tactic:
hq₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑q.den : ℝ)

Tactic:
exact hq₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
hq₁ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
hq₂ : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ)
⊢ |ξ - (↑q : ℝ)| < ((↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1))⁻¹

Tactic:
exact h.trans (by rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]; ring_nf; exact hq₀)

Premises used: LT.lt.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
ξ : ℝ
⊢ (GenContFract.of ξ).convs 0 = (↑(ξ.convergent 0) : ℝ)

Tactic:
simp only [zeroth_conv_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_intCast]

Premises used: Rat.cast_intCast, Real.convergent_zero, GenContFract.of_h_eq_floor, GenContFract.zeroth_conv_eq_h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)
ξ : ℝ
succ :
  HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑((fract ξ)⁻¹.convergent n) : ℝ)⁻¹ = (↑((↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹) : ℝ)
⊢ (GenContFract.of ξ).convs (n + 1) = (↑(ξ.convergent (n + 1)) : ℝ)

Tactic:
rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]

Premises used: Int.fract, Real.convergent_succ, GenContFract.convs_succ, Inv.inv, one_div
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)
ξ : ℝ
succ succ₁ succ₂ succ₃ : (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹ = (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹
⊢ HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑((fract ξ)⁻¹.convergent n) : ℝ)⁻¹ = (↑((↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
ξ : ℝ
n : ℕ
zero : ∀ (ξ : ℝ), (GenContFract.of ξ).convs 0 = (↑(ξ.convergent 0) : ℝ)
succ :
  ∀ (n : ℕ) (ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)) (ξ : ℝ),
    (GenContFract.of ξ).convs (n + 1) = (↑(ξ.convergent (n + 1)) : ℝ)
⊢ (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)

Tactic:
induction n generalizing ξ with
  | zero => simp only [zeroth_conv_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_intCast]
  | succ n ih => rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]; norm_cast

Premises used: Rat.cast_intCast, Real.convergent_succ, Real.convergent_zero, GenContFract.convs_succ, one_div, Int.succ, GenContFract.of_h_eq_floor, GenContFract.zeroth_conv_eq_h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
obtain : ∀ (n : ℕ) (hn : q = ξ.convergent n), ∃ (n : ℕ), (GenContFract.of ξ).convs n = (↑q : ℝ)
⊢ ∃ (n : ℕ), (GenContFract.of ξ).convs n = (↑q : ℝ)

Tactic:
obtain ⟨n, hn⟩ := exists_rat_eq_convergent h

Premises used: Real.exists_rat_eq_convergent
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
n : ℕ
hn : q = ξ.convergent n
⊢ ∃ (n : ℕ), (GenContFract.of ξ).convs n = (↑q : ℝ)

Tactic:
⟨n, hn.symm ▸ convs_eq_convergent ξ n⟩

Premises used: Eq.rec, Real.convs_eq_convergent, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
n : ℕ
hn : q = ξ.convergent n
⊢ ∃ (n : ℕ), (GenContFract.of ξ).convs n = (↑q : ℝ)

Tactic:
exact ⟨n, hn.symm ▸ convs_eq_convergent ξ n⟩
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
a : ZMod n
ha : IsUnit a
⊢ Eq (α := R) ((χ : (a : ZMod n) → R) a : R) ((↑((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ) ha.unit) : R) : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ toUnitHom χ = toUnitHom ψ ↔ χ = ψ

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x : ZMod n
⊢ Eq (α := R) ((χ : (a : ZMod n) → R) ((↑n : ZMod n) - x) : R) ((χ : (a : ZMod n) → R) (-x) : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.DirichletCharacter.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n_1 : ℕ
χ : DirichletCharacter R n_1
n m : ℕ
hm : n ∣ m
h :
  ∀ (a : (ZMod m)ˣ),
    Eq.{u_1 + 1} (α := R)
      ((ofUnitHom (MonoidHom.comp (toUnitHom 1) (ZMod.unitsMap hm)) : (a : ZMod m) → R) (↑a : ZMod m) : R)
      ((1 : (a : ZMod m) → R) (↑a : ZMod m) : R)
⊢ Eq.{u_1 + 1} (α := DirichletCharacter R m) (ofUnitHom (MonoidHom.comp (toUnitHom 1) (ZMod.unitsMap hm))) 1

Tactic:
ext