awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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)⁻¹
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₂ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) =
  (↑⌊ξ⌋ : ℚ) + (HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ))⁻¹
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℚ))⁻¹
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₃ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) =
  (↑⌊ξ⌋ : ℚ) + ((↑(↑v : ℤ) : ℚ) / ((↑u : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ)))⁻¹
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℚ)))⁻¹
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₄ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + ((↑v : ℚ) / ((↑u : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ)))⁻¹
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℚ)))⁻¹
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₅ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + ((↑u : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ)) / (↑v : ℚ)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₆ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) =
  (↑⌊ξ⌋ : ℚ) + (HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) - HMul.hMul (α := ℚ) (↑⌊ξ⌋ : ℚ) (↑v : ℚ) / (↑v : ℚ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℚ))
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₇ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + (HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) - (↑⌊ξ⌋ : ℚ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℚ) - (↑⌊ξ⌋ : ℚ))
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₈ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ ∃ (n : ℕ), q = ξ.convergent n
have refine_1 : IsCoprime q.num (↑q.den : ℤ)
Tactic: refine q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
refine_1 : IsCoprime q.num (↑q.den : ℤ)
⊢ ∃ (n : ℕ), q = ξ.convergent n
have refine_2 : ∀ (hd : Eq (α := ℤ) (↑q.den : ℤ) 1), -(1 / 2) < ξ - (↑q.num : ℝ)
Tactic: refine q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℝ)
⊢ ∃ (n : ℕ), q = ξ.convergent n
have refine_3 : |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
  ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
Tactic: refine q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hd : Eq (α := ℤ) (↑q.den : ℤ) 1
⊢ -(1 / 2) < ξ - (↑q.num : ℝ)
have h₁ : |ξ - (↑(↑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
Cleared hypotheses: h, hd
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
have hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
Tactic: obtain ⟨hq₀, hq₁⟩ := aux₀ (Nat.cast_pos.mpr q.pos)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
hq₀ : LT.lt (α := ℝ) 0 (↑(↑q.den : ℤ) : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
have hq₁ : 0 < HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1
Tactic: obtain ⟨hq₀, hq₁⟩ := aux₀ (Nat.cast_pos.mpr q.pos)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
have hq₂ : 0 < (↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1)
Tactic: replace hq₁ := mul_pos hq₀ hq₁
Cleared hypotheses: hq₁
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
have hq₂ : 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₀)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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 : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
have hq₃ : LT.lt (α := ℝ) 0 (↑q.den : ℝ)
Tactic: rw [cast_natCast] at *
Cleared hypotheses: hq₀, hq₁, hq₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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 : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑(↑q.den : ℤ) : ℝ)| <
    ((↑(↑q.den : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑q.den : ℤ) : ℝ) - 1))⁻¹
have hq₄ : 0 < (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
Tactic: rw [cast_natCast] at *
Cleared hypotheses: hq₀, hq₁, hq₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℝ)
have norm_cast : Rat.divInt q.num (↑q.den : ℤ) = Rat.divInt q.num (↑q.den : ℤ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)| < ((↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1))⁻¹
have refine_3 : |ξ - (↑q : ℝ)| < ((↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℝ)
⊢ 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2) < ((↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1))⁻¹
have rw : 0 < 2 * HMul.hMul (α := ℝ) (↑q.den : ℝ) (↑q.den : ℝ) - (↑q.den : ℝ) * (HMul.hMul (α := ℝ) 2 (↑q.den : ℝ) - 1)
Tactic: rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions (goal)
Goal:
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)
ξ : ℝ
⊢ (GenContFract.of ξ).convs (n + 1) = (↑(ξ.convergent (n + 1)) : ℝ)
have succ : HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑((fract ξ)⁻¹.convergent n) : ℝ)⁻¹ = (↑((↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹) : ℝ)
Tactic: rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions (goal)
Goal:
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)
ξ : ℝ
⊢ HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑((fract ξ)⁻¹.convergent n) : ℝ)⁻¹ = (↑((↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹) : ℝ)
have succ : (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹ = (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions (goal)
Goal:
ξ : ℝ
n : ℕ
⊢ (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)
have zero : ∀ (ξ : ℝ), (GenContFract.of ξ).convs 0 = (↑(ξ.convergent 0) : ℝ)
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
Cleared hypotheses: ξ, n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions (goal)
Goal:
ξ : ℝ
n : ℕ
zero : ∀ (ξ : ℝ), (GenContFract.of ξ).convs 0 = (↑(ξ.convergent 0) : ℝ)
⊢ (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)
have succ : ∀ (n : ℕ) (ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = (↑(ξ.convergent n) : ℝ)) (ξ : ℝ),
  (GenContFract.of ξ).convs (n + 1) = (↑(ξ.convergent (n + 1)) : ℝ)
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
Cleared hypotheses: ξ, n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions (goal)
Goal:
ξ : ℝ
q : ℚ
h : |ξ - (↑q : ℝ)| < 1 / (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ ∃ (n : ℕ), (GenContFract.of ξ).convs n = (↑q : ℝ)
have obtain : ∀ (n : ℕ) (hn : q = ξ.convergent n), ∃ (n : ℕ), (GenContFract.of ξ).convs n = (↑q : ℝ)
Tactic: obtain ⟨n, hn⟩ := exists_rat_eq_convergent h
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n_1 : ℕ
χ : DirichletCharacter R n_1
n m : ℕ
hm : n ∣ m
⊢ Eq.{u_1 + 1} (α := DirichletCharacter R m) (ofUnitHom (MonoidHom.comp (toUnitHom 1) (ZMod.unitsMap hm))) 1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n_1 : ℕ
χ : DirichletCharacter R n_1
n m : ℕ
hm : n ∣ m
ψ₁ ψ₂ : DirichletCharacter R n
⊢ ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm)) =
    ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm))
have h : ∀ (a : (ZMod m)ˣ),
  Eq (α := R) ((ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm)) : (a : ZMod m) → R) (↑a : ZMod m) : R)
    ((ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm)) :
          (a : ZMod m) → R)
        (↑a : ZMod m) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  Eq (α := DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m)
⊢ a₁ = a₂
have h₁ : ∀ (y : (ZMod n)ˣ), Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑y : ZMod n) : R) ((a₂ : (a : ZMod n) → R) (↑y : ZMod n) : R)
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  Eq (α := DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m)
y : (ZMod n)ˣ
⊢ Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑y : ZMod n) : R) ((a₂ : (a : ZMod n) → R) (↑y : ZMod n) : R)
have h₁ : ∀ (z : (ZMod m)ˣ),
  Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
    ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
Tactic: obtain ⟨z, rfl⟩ := ZMod.unitsMap_surjective hm y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n m : ℕ
inst_1 : NeZero m
hm : n ∣ m
a₁ a₂ : DirichletCharacter R n
h :
  Eq (α := DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m)
    ((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m)
z : (ZMod m)ˣ
⊢ Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
    ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
have h₁ : ∀
  (h :
    ∀ (a : (ZMod m)ˣ),
      Eq (α := R)
        ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₁ : DirichletCharacter R m) :
              (a : ZMod m) → R)
            (↑a : ZMod m) :
          R)
        ((((changeLevel hm : (a : DirichletCharacter R n) → DirichletCharacter R m) a₂ : DirichletCharacter R m) :
              (a : ZMod m) → R)
            (↑a : ZMod m) :
          R))
  (z : (ZMod m)ˣ),
  Eq (α := R) ((a₁ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
    ((a₂ : (a : ZMod n) → R) (↑((ZMod.unitsMap hm : (a : (ZMod m)ˣ) → (ZMod n)ˣ) z) : ZMod n) : R)
Tactic: rw [MulChar.ext_iff] at h
Cleared hypotheses: h, z
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ toUnitHom ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R n) χ) = toUnitHom χ
have rw : toUnitHom χ = toUnitHom χ
Tactic: rw [changeLevel_self]